Deducing finitary Hales-Jewett from infinitary Hales-Jewett I have at my disposal the infinitary Hales-Jewett theorem. Denote by $\operatorname{Seq}(n)$ the set of all nonempty finite words generated by an $n$-letter alphabet.

If $\operatorname{Seq}(n)$ is finitely partitioned into $k$ parts, then for some $i \in \{1, \ldots, k\}$ part $i$ contains a combinatorial line.

I want to deduce the following finitary version of the theorem.

For any $n, k \in \mathbb{N}$ there exists $N \in \mathbb{N}$ such that for any $d > N$, if $n^d$ is partitioned into $k$ parts, then at least one of the parts contains a combinatorial line.

I'm approaching this by contradiction. Hence for any $N \in \mathbb{N}$, there is some $d > N$ such that $\{1,\ldots,n\}^d$ can be partitioned into $k$ parts but none of the parts contain a combinatorial line. Hence, for each $N \in \mathbb{N}$, we have some $d_N$ so that $\{1,\ldots,n\}^d$ can be made into a "bad partition".
I'm unsure how to proceed exactly. I think the idea is to extend the bad partition of $\{1, \ldots, n\}^d$ to a partition of $\operatorname{Seq}(n)$, but doing so is not obvious. I can of course extend every word in every part "upwards" by considering all its extensions, but this only gets me halfway to a partition of $\operatorname{Seq}(n)$; I also need to extend downwards. Doing so is tricky because words coming from different parts of the bad partition might have common prefixes. Instead, I thought perhaps I can bin all the words of length less than $d$ into a new part to form a partition of $\operatorname{Seq}(n)$. But then if I apply the infinitary Hales-Jewett, it could be that the combinatorial line is in this new part, and I'm unsure how to handle that. In fact, even if the combinatorial line that the infinitary Hales-Jewett theorem gives me is in one of the parts corresponding to a piece of the original bad partition, it's unclear to me how exactly I can use it to obtain a combinatorial line.
We saw this material in the context of ultrafilters (we used nonprincipal ultrafilters in the Stone-Cech compactification of $\operatorname{Seq}(n)$ to prove the infinitary Hales-Jewett theorem) so I believe I should use an argument involving an ultrafilter. 
 A: First, to prove that there exists some $N$ such that $n^N$ can be finitely partitioned into $m$ pieces in any way and have a combinatorial line in one of the pieces, suppose to the contrary that there is no such $N$. Then for every $N$ we have a bad partition into $m$ pieces, such that no piece contains a combinatorial line. For each stage $N$, enumerate the pieces of the bad partition by $P_{i,N}$ for $i \in [m]$. Define the family of sets
$$
P_i = \bigcup_{j < \omega} P_{i,j}
$$
for every $i \in [m]$. Note that this family of sets is a partition of $\operatorname{Seq}(n)$.
By the infinitary Hales-Jewett theorem, there exists a piece, say $P_i$, in this partition that contains a combinatorial line, say $L$ generated by the variable word $w$ of length $l$. But then this combinatorial line is contained in $P_{i,l}$, which contradicts that the family of $P_{j,l}$ over $j < \omega$ is a bad partition.
Hence, no matter how $n^N$ is finitely partitioned into $m$ pieces, one of the pieces contains a combinatorial line. 
Now we want to show that for any $d \geq N$, $n^d$ can be finitely partitioned in any way and have a piece with a combinatorial line.
We proceed by induction on $d$. The base case $d = N$ is covered by the above argument. Now for the step case suppose that $n^{d+1}$ is partitioned into $m$ pieces. We want to find a combinatorial line in one of the pieces. This induces a partition on the set of all words in $n^{d+1}$ that end in 1, which we can identify with words in $n^d$. Hence, this induces a partition on $n^d$, which by the induction hypothesis can be finitely partitioned in any way and have a piece with a combinatorial line, say $L$ generated by the variable word $w$ of length $d$. We can extend $w$ to $w^\prime \in n^{d+1}$ by appending the letter $1$. But then this generates a combinatorial line in the partition piece of $n^{d+1}$ corresponding to piece $i$ in $n^d$. Hence one of the pieces of $n^{d+1}$ contains a combinatorial line.
