Sperner's theorem
Sperner's theorem: Any line-free subset of [math]\displaystyle{ [2]^n }[/math] has cardinality at most [math]\displaystyle{ \binom{n}{\lfloor n/2\rfloor} }[/math].
It implies the k=2 version of the density Hales-Jewett theorem.
A stronger version of Sperner's theorem is
LYM inequality: Any line-free subset of [math]\displaystyle{ [2]^n }[/math] has equal-slices measure at most 1.
The k=3 generalisation of this inequality is the hyper-optimistic conjecture.
The LYM inequality can be proven as follows. Randomly shuffle the n indices and then consider the intersection of A with the strings [math]\displaystyle{ 0^i 1^{n-i} }[/math] for [math]\displaystyle{ i=0,\ldots,n }[/math]. As A is line-free, at most one of these strings lie in A. Averaging over all choice of shuffles we obtain the claim.