feat: Combinatorial subspaces and extended Hales-Jewett

[YaelDillies]

trafficstars

This PR extends the Hales-Jewett theorem from combinatorial lines to higher-dimensional combinatorial subspaces. It's an example of a theorem proving its own generalisation.

Co-authored-by: David Wärn

---

The plan is to eventually use this to prove existence of monochromatic (m, p, c)-sets.

Ported from https://github.com/leanprover-community/mathlib/pull/11305