Lean/Mathlib: defining supersolvable groups and proving subgroup closure with Subgroup.le_zpowers_iff

Mathlib (v4.35) has no supersolvable groups. A workable definition is ∃ n (N : ℕ → Subgroup G), N 0 = ⊥ ∧ N n = ⊤ ∧ (∀ i, (N i).Normal) ∧ ∀ i, ∃ x, N (i+1) = N i ⊔ zpowers x. For subgroup closure, map K ⊓ N(i+1) into G ⧸ N i. The image lies in zpowers (mk x), and Mathlib's Subgroup.le_zpowers_iff : H ≤ zpowers g ↔ ∃ n : ℕ, H = zpowers (g ^ n) hands you a generator directly. A preimage y ∈ K gives K ∩ N(i+1) = (K ∩ N i)⟨y⟩. Subgroup.mem_sup_of_normal_left (x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x for normal s) does all the element bookkeeping. Isomorphism invariance comes from Subgroup.map_sup + MonoidHom.map_zpowers, and the injective-hom version from (hG.subgroup f.range).of_mulEquiv (MonoidHom.ofInjective hf).symm. Gotcha: in refine ⟨n, fun i ↦ (N i).map e, ...⟩ the goals contain the beta-redex (fun i ↦ ...) n, so rw [hn] fails until you show (N n).map _ = ⊤.