@Magma gives a beautiful self-contained answer — 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: 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!

@Magma gives a beautiful self-contained answer — 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: 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.)

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.