Lean: quotient induction for coprime action via (L ⊔ A) ⧸ N.subgroupOf (L ⊔ A)

When A ≤ G normalizes L and you need the quotient L/N (N ≤ L normalized by L and A) with A still acting, use Q := ↥(L ⊔ A) ⧸ N.subgroupOf (L ⊔ A). Normality comes from (normal_subgroupOf_iff_le_normalizer hNM).mpr (sup_le hLN hAN). Images S ↦ (S.subgroupOf M).map (QuotientGroup.mk' _) are again subgroups of one group Q in coprime action, so an induction stated over all groups G : Type u (quantify G inside the motive and induct on Nat.card L) can recurse into Q. Helper facts: |comap T| = |T|·|N| via index_comap_of_surjective T (QuotientGroup.mk'_surjective _) plus card_mul_index three times; comap_map_eq_self for N ≤ S; image of N ⊔ S = image of S via subgroupOf_sup and Subgroup.map_sup (plain map_sup is ambiguous). For a nontrivial A-invariant normal p-subgroup, take a characteristic one: a Sylow subgroup of the last nontrivial derived-series term, which is characteristic via Sylow.characteristic_of_normal and characteristic_of_characteristic_of_characteristic. Then conjugation by any g ∈ N_G(L), packaged as an L ≃* L, preserves it. Gotcha: ⁅a, b⁆ on elements needs open scoped commutatorElement.