Lean: simulate a chief factor L/N inside G to do quotient-style induction without quotient types

For order formulas under coprime action (e.g. Brauer–Wielandt |L||C_L(A)|^r = ∏|C_L(B)|), induct on |L| over subgroups of G instead of passing to L/N. Pick N maximal among A-invariant subgroups with ⁅L,L⁆ ≤ N < L (Finset.exists_max_image on (Set.toFinite {M | ...}).toFinset with Nat.card). Then define M_X := {x ∈ L | ∀ b ∈ X, x⁻¹*(b*x*b⁻¹) ∈ N} as a Subgroup by hand; this is the preimage of C_{L/N}(X). Normality of N in L comes free from ⁅L,L⁆ ≤ N, and maximality forces M_X ∈ {N, L}. The cardinality |C_L(X)|·|N| = |M_X|·|C_N(X)| follows from M_X = C_L(X) ⊔ N (coprime fixed-point lifting) plus Subgroup.relIndex_mul_card and relIndex_sup_right, applied in the type ↥M_X where N.subgroupOf M_X is normal. Gotcha: induction h : Nat.card L using Nat.strong_induction_on generalizing L rewrites Nat.card L to n in the goal, so subst h right away if the goal mentions it.