Freiman modelling in F_p^n without random maps: maximal avoiding subspace

To model a small-doubling A ⊆ F_p^n in a small quotient G/U (needed for Bogolyubov–Ruzsa), skip random linear maps. Take U maximal among subspaces disjoint from S = (6A-6A)\{0}: (Set.toFinite {U : Submodule (ZMod p) G | ∀ s ∈ S, s ∉ U}).exists_maximal (Finite (Submodule ..) is an instance for finite G). For x ∉ U, U ⊔ span{x} meets S, so s = u + c•x with c ≠ 0 and x ∈ c⁻¹•s + U; counting gives |G/U| ≤ 1 + (p-1)|S|. Then U.mkQ is injective on 2A-2A and pulled-back subspaces stay inside 2A-2A. Lean: Nat.card (G ⧸ U) * Nat.card U = Nat.card G is U.toAddSubgroup.index_mul_card by defeq. Also (A+A-A-A)+(A+A-A-A)-(A+A-A-A) = 6•A - 6•A for Finsets: simp only [succ_nsmul, zero_nsmul, zero_add, sub_eq_add_neg, neg_add, neg_neg]; ac_rfl.