@Magma gives [a beautiful self-contained answer](https://mathoverflow.net/a/420104/2273) — but to put it into a bigger picture, it’s worth also mentioning the word **compactness**, the term for a lot of phenomena like this one, and which gives this as a consequence of various quite general theorems. As a logician, the first way that springs to mind for me is the [compactness theorem for first-order logic](https://en.wikipedia.org/wiki/Compactness_theorem): if every subset of some first-order theory has a model, then so does the whole theory. So: write down a first-order theory describing a suitable tiling of the plane; and note that “arbitrarily large squares can be tiled” implies that every finite subset is consistent. (There are lots of ways to write such a theory, but one approach is purely propositional: for each $i,j \in \mathbb{Z}$, take atomic propositions $H_{i,j}$ and $V_{i,j}$ in the language, read as saying that the square $(i,j)$ is in the same tile as its horizontal neighbour $(i+1,j)$ or its vertical neighbour $(i,j+1)$ respectively; and for each $(i,j)$, give an axiom $\alpha_{i,j}$ expressing that some copy of the polyomino is formed by tiles connected to $(i,j)$, and that these are not connected to any of their other neighbours.) But compactness can be also seen in other guises, e.g. topologically. Intuitively, @Magma’s argument can be seen as saying that the sequence of arbitrarily large finite tilings must have a convergent subsequence within some suitable compact topological space of tilings, which must converge to a tiling of the whole plane. I don’t immediately what space to use, that would make each of the above steps “easy” (either directly or from general theorems) — but I’m sure someone more familiar with writing in such terms can see how to write it this way. (Edit: Magma has now done that, in their [second answer](https://mathoverflow.net/a/420178/2273).) That said, the big payoff of this framework isn’t (in my opinion) invoking the big theorems for proofs — as in this case, the direct proofs are often very nice, and no harder than carefully encoding the problem to fit one of the general theorems. **The real advantage of this framework is helping us recognise such situations.** Familiarity with compactness theorems lets you look at a question like this one and immediately think “yes, this should be possible, by some kind of compactness argument” — and then guide you to a proof, either direct or via a general theorem.