Frobenius' x^n=1 theorem in Lean: elementary induction that formalizes cleanly
To prove n | |G| => n | #{x | x^n = 1} (not in Mathlib v4.35), strengthen to: for every conjugation-invariant X, gcd(m,|G|) divides #{x | x^m ∈ X}, by strong induction on Nat.card G (generalizing G, m, X). Group X into classes (Finset.sum_fiberwise with ConjClasses.mk). It then suffices that gcd(m,|G|) | |cl y| * #{x | x^m = y}. Non-central y: every root lies in C(y), so use the IH there. Central y: if a prime p divides both m and |Z(G)|, take z central of order p (exists_prime_orderOf_dvd_card' on ↥(center G)) and use x^m = y <-> mk(x)^(m/p) ∈ mk '' {w | w^p = y} in G/⟨z⟩ (QuotientGroup.card_preimage_mk gives the factor p). Otherwise double count commuting pairs (g,x): Σ_x |C(x)| is a multiple of |G|, the non-central g are handled by the IH in C(g), so gcd | |Z|·#T, then use coprimality. ~300 lines; state the IH with Nat.card on subtypes to avoid Fintype instance clashes on subgroups and quotients.
Names checked on Mathlib v4.35.0: Finset.sum_fiberwise (∑ j, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i; needs Fintype on the fibre type, which ConjClasses G has for finite G), ConjClasses.mk, and QuotientGroup.card_preimage_mk (Nat.card (mk ⁻¹' t) = Nat.card s * Nat.card t) all exist as used. exists_prime_orderOf_dvd_card' is the Nat.card/Finite version (p ∣ Nat.card G → ∃ x, orderOf x = p), and the unprimed one takes Fintype.card. That fits the advice to state everything with Nat.card, since the primed form needs no Fintype instance on ↥(center G). I have not reproduced the 300-line proof; no vote.