Tiling $\mathbb{R}^2$ with polyomino Divide $\mathbb{R}^2$ into disjoint unit squares, let Q be a tile (a polyomino, a finite set of connected unit squares). If, for every finite set S of unit squares in $\mathbb{R}^2$, - I can find a finite set of disjoint Q-tiles (a tiling) such that S is a subset of this tiling, how to prove that I can tile entire $\mathbb{R}^2$ with Q-tiles, (without axiom of choice)?
 A: Consider a sequence $S_1, S_2, S_3, \ldots$ of finite regions that exhaust the plane, namely $\cup S_i = \mathbb{R}^2$. For instance, you may take $S_i$ to be the square of edge side $2i+1$ centered at the origin.
Each $S_i$ is coverable with copies of your tile $Q$. Define a tree as follows: The vertices at level $i$ are all the possible coverings of $S_i$, and a vertex at level $i$ is a connected with a vertex at level $i+1$ iff the latter is an extension of the former - namely, a covering of $S_{i+1}$ that contains the covering of $S_i$ and possibly adds a finite number of additional tiles. (to give our tree a root we can just add a vertex, representing "S_0", connected to all the ways to position a single tile $Q$ over $S_1$). 
It should be easy to prove that this is indeed an infinite tree. By Kőnig's lemma it contains an infinite branch which defines a tiling of the while plane. Kőnig's lemma is equivalent to a weak form of AC, probably countable-AC or something similar; I don't think you can avoid some form of choice or dependent choice for your proof. 
A: I know three different proofs of this.


*

*First, you can appeal to König's lemma. View the set
of tilings of increasingly large squares based at the
origin (that is, they minimally cover such a square) as a
tree under the subtiling relation. This is a finitely
branching tree, since any tiling of a square has only
finitely many extensions to cover the next larger square.
But your assumption says that this tree is infinite. Thus,
it has an infinite branch, by König's lemma. Such a
branch gives a tiling of the entire plane.

*Second, you can view the previous argument as a
compactness argument, if you consider the right topology.

*Third, one can argue from nonstandard analysis. Take a
nonstandard model of the natural numbers. By the transfer
principle, there must be a tiling of some nonstandard
size square using tiles from your tile set. But a nonstandard
(pseudo)finite square includes many actual copies of the
standard plane inside it, around the nonstandard numbers in the
very center of the nonstandard square. Thus, there is a
tiling of the actual standard plane.
