I am currently trying to work through this double induction proof used to prove Hales Jewett. I understand most of it, everything apart from the part that I highlighted in bold. I was hoping somebody could explain to me why this colouring exists, that is why because there are $k^{m^n}$ ways of colouring $[m]^{(n)}$ and $n'=HJ(m-1, k^{m^n})$ do we have the colouring $c(a,b)=c(a,b')$ for all $a \in [m]^{(n)}$ and $b,b' \in [m]^{(n')}$.
Many thanks in advance. The Theorem is: For any $m,k \in \mathbb{N}$, there exists an $n \in \mathbb{N}$ such that any $k$-colouring of $[m]^{(n)}$ contains a monochromatic line.
The full proof goes as follows:
We begin by inducting on $m$. Base case $1$: For $m=1$, take $n=1$. Induction Hypothesis $1$: We assume that for all $m-1 \geq 1$ there exists an $n \in \mathbb{N}$ that satisfies the Theorem for all $k \in \mathbb{N}$, set $n=HJ(m-1, k)$.
We now make the claim: $(\dagger)$ For all $r \leq k$ there is an $n \in \mathbb{N}$ such that for any $k$-colouring of $[m]^{(n)}$ there is either a monochromatic combinatorial line in $[m]^{(n)}$ or $r$ colour focussed combinatorial lines. To prove this claim, we induct on $r$: Base case $2$: For $r=1$, let $n=HJ(m-1, k)$ which exists due to Induction Hypothesis $1$. Induction Hypothesis $2$: Assume that for any $r \geq 1$ there exists an $n \in \mathbb{N}$ that holds for $(\dagger)$, we proceed in seeing that $n+HJ(m-1,k^{m^n})$ is sufficient for $r+1$, let $n'=HJ(m-1,k^{m^n})$ . Assume that all $k$-colourings of $[m]^{(n+n')}(=[m]^{n}\times[m]^{n'})$ do not yield a monochromatic combinatorial line, so we need to show that a $k$-colouring gives us $r+1$ colour focussed combinatorial lines. There is a combinatorial line $L \subset [m]^{(n')}$ with active coordinate set $I \subset [n']$ such that for all $a \in [m]^{(n)}$ and all $b,b' \in L-L^+$, $c((a,b))=c((a,b'))$ this is due to there being $k^{m^n}$ ways of colouring $[m]^{(n)}$ and the choice of $n'=HJ(m-1,k^{m^n})$. Furthermore, as $n=HJ(m-1,k)$ and there being no monochromatic combinatorial line in the $k$-colouring of $[m]^{(n+n')}$ by our induction hypothesis, there are $r$ colour focussed combinatorial lines for c, say $L_1, L_2,...,L_r$ with the respective active coordinate sets $I_1,I_2,...,I_r$ and focus $f$. From these $r$ colour focussed combinatorial lines in $[m]^n$ we are now going to identify $r+1$ colour focussed combinatorial lines in $[m]^{n}\times[m]^{n'}(=[m]^{(n+n')})$: Define $L^{'}_{i}$ to be the line through the point $(L_{i}^{-}, L^-)$ with active coordinate set $I = I_i \cup I$ for $1 \leq i \leq r$. $$\implies L_{1}^{'},L_{2}^{'},...,L_{r}^{'} \text{ are colour focused at } (f, L^+)$$So together with the line going through $(f,L^-)$ which is focused at $(f,L^+)$ gives us $r+1$ colour focussed lines. So the claim $(\dagger)$ holds, which in turn implies our Induction Hypothesis $1$ is true.
To complete the proof, note that inserting $r=k$ in our proved claim $(\dagger)$ gives us either a monochromatic combinatorial line in in $[m]^{(n)}$ or $k$ colour focussed combinatorial lines. If the first case is not true then by looking at the focus of the $k$ coloured combinatorial lines gives us a line which is monochromatic.
For a specific $b\in [m]^{(n')}$, there are $m^n$ points $(a,b)$. Those points can be coloured in $k^{m^n}$ different ways. Let $K=k^{m^n}$, then think of the collection of $m^n$ colours as a single COLOUR. So each $b\in [m]^{(n')}$ has one of $K$ different COLOURs.
Consider just those $b$ with no coordinate $1$. So they might be $(2,4,4,3,5,2)$, but exclude $(3,4,1,4,2,3)$. The point is that set has $m-1$ instead of $m$. So they have a monoCOLOUR line $\hat L$, with active set $I$ in the theorem. All $b,b'$ in the line have the same COLOUR, which means $(a,b)$ has the same colour as $(a,b')$ for all $a$.
Note that $\hat L= L-L^+$.