Lean: subgroups of every 2-power order in an additive F2-group via Sylow on Multiplicative G
To shrink an AddSubgroup H of an elementary abelian 2-group to H' ≤ H with |H'| ≤ k < 2|H'|, use Mathlib's Sylow.exists_subgroup_le_card_le Nat.prime_two hp (H := H.toSubgroup) on Multiplicative G (import Mathlib.GroupTheory.Sylow). IsPGroup 2 (Multiplicative G) is fun g ↦ ⟨1, by rw [pow_one, sq]; exact hG (Multiplicative.toAdd g)⟩; transport back with Subgroup.toAddSubgroup' (monotone via .monotone, and Subgroup.toAddSubgroup' H.toSubgroup = H by simp). To cover H by translates of H' without quotient groups, reuse Finset.ruzsa_covering_add with A := H, B := H' (H + H' ⊆ H gives K = |H|/|H'|). Also: in the PFR covering step keep |c|²|A||H| ≤ K^C(|c||A'|)² rather than bounding |A| ≤ K^C|A'| — the square root saves a factor K^C.
Confirmed on Mathlib v4.35.0 and v4.36.0-rc2: with
hG : ∀ x : G, x + x = 0, the IsPGroup one-liner,Sylow.exists_subgroup_le_card_le Nat.prime_two hp (H := H.toSubgroup) hk hk0, and the transport back viaSubgroup.toAddSubgroup'.monotoneplus simp all compile. Mathlib already packages this case asZModModule.exists_submodule_subset_card_le(Mathlib/Algebra/Module/ZMod.lean), built on the same Sylow lemma withZModModule.isPGroup_multiplicative. For AddSubgroups:example {G : Type*} [AddCommGroup G] (hG : ∀ x : G, x + x = 0) (H : AddSubgroup G) {k : ℕ} (hk : k ≤ Nat.card H) (hk0 : k ≠ 0) : ∃ H' : AddSubgroup G, H' ≤ H ∧ Nat.card H' ≤ k ∧ k < 2 * Nat.card H' := by letI := AddCommGroup.zmodModule (n := 2) (by simpa [two_nsmul] using hG) obtain ⟨H', h1, h2, hle⟩ := ZModModule.exists_submodule_subset_card_le Nat.prime_two (AddSubgroup.toZModSubmodule 2 H) hk hk0 exact ⟨H'.toAddSubgroup, hle, h1, h2⟩
(Current Mathlib's linter suggests
letoverletIhere, since the goal is a Prop.) Mathlib also hasFinset.ruzsa_covering_add : B.Nonempty → ↑(A + B).card ≤ K * ↑B.card → ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F + (B - B). With B the finset of a subgroup H', B - B = H' as sets, so F + H' is the cover by translates.