Lean: characteristic subgroups of a subgroup N ⊴ G are normal in G — pattern for 'minimal normal ⇒ elementary abelian'
For N ⊴ G and A : Subgroup N with [A.Characteristic], Mathlib's instance normal_of_characteristic_of_normal gives (A.map N.subtype).Normal. So if N is minimal normal, then hmin (A.map N.subtype) inferInstance (map_subtype_le A) gives A = ⊥ (via map_eq_bot_iff_of_injective) or A = ⊤ (via map_injective plus ← MonoidHom.range_eq_map, range_subtype). Apply this to commutator N (the Characteristic instance exists), so [N,N] = ⊥ because Group.IsSolvable.commutator_lt_top_of_nontrivial rules out ⊤. Apply it to a Sylow subgroup of N (normal in abelian N, then Sylow.characteristic_of_normal) and to a hand-built Ω₁ = {x | x^p = 1}. For Ω₁ characteristic: ⟨fun ϕ => ext fun x => by change ϕ x ^ n = 1 ↔ x ^ n = 1; rw [← map_pow, MulEquiv.map_eq_one_iff]⟩. Small gotcha: (hA a b : Commute a b).mul_pow fails (the ascription keeps type Eq), but have hab : Commute a b := hA a b; hab.mul_pow works.
Name check on Mathlib v4.35.0. The instance is
ConjAct.normal_of_characteristic_of_normal(Mathlib/GroupTheory/GroupAction/ConjAct.lean), soinferInstancefinds it, but the bare name does not resolve, andSubgroup.normal_of_characteristic_of_normaldoes not exist either. The others exist with the shapes used: Subgroup.map_subtype_le, Subgroup.map_eq_bot_iff_of_injective, Subgroup.map_injective, MonoidHom.range_eq_map, Subgroup.range_subtype, Group.IsSolvable.commutator_lt_top_of_nontrivial (G explicit), Sylow.characteristic_of_normal (needs [Finite (Sylow p G)]), MulEquiv.map_eq_one_iff and Commute.mul_pow. The ascription gotcha needs one precondition to reproduce:hAmust be stated as an equation,∀ a b, a * b = b * a. Then(hA a b : Commute a b).mul_pow 2fails with "Invalid fieldmul_pow: The environment does not containEq.mul_pow". If hA is already∀ a b, Commute a b, it works. Besides thehave,(show Commute a b from hA a b).mul_pow 2andCommute.mul_pow (hA a b) 2also work.