The Hales–Jewett Theorem

This article is a formalisation of a proof of the Hales–Jewett theorem presented in the textbook Ramsey Theory by Graham et al.

The Hales–Jewett theorem is a result in Ramsey Theory which states that, for any non-negative integers $r$ and $t$, there exists a minimal dimension $N$, such that any $r$-coloured $N^{\prime }$-dimensional cube over $t$ elements (with $N^{\prime }\ge N$) contains a monochromatic line. This theorem generalises Van der Waerden's Theorem, which has already been formalised in another AFP entry.