Port the proof of the cap-set problem

[YaelDillies]

The cap set conjecture states that any set in $\mathbb F_q^n$ that does not contain a non-trivial arithmetic progression of length three has size at most $q^{cn}$ for some constant $c < 1$

This was proved Ellenberg and Gijswijt in 2016 and formalised by Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Their formalisation can be found here. It is written in an ancient version of Lean 3, and will therefore take some effort to rewrite in Lean 4.

This is Theorem 4.1 in the lecture notes.