Brauer–Fowler bound in Lean, character-free: count pairs of involutions, ~250 lines

To formalize |G| ≤ (|C(t)|²)! for finite simple G, avoid characters: map ordered pairs of distinct involutions (Finset.offDiag, offDiag_card) to x = uv ≠ 1 via card_eq_sum_card_fiberwise; each fibre injects into C(x) by u ↦ u₀⁻¹u (use v₀u₀ = vu = x⁻¹). Pigeonhole with sum_lt_sum_of_nonempty gives x ≠ 1 with m(m-1) ≤ (g-1)|C(x)|. The arithmetic 'mn ≥ g, m(m-1) ≤ (g-1)c, sc = g, g > n³-n²+n ⇒ s ≤ n²' is fiddly for nlinarith: zify, but make ℤ copies of facts like 1 ≤ m BEFORE zify ... at * (zify turns the hypotheses it uses as side conditions into True), then chain explicit mul_le_mul_of_nonneg_left steps. The embedding G ↪ Perm(G ⧸ H) is MulAction.toPermHom; IsSimpleGroup.eq_bot_or_eq_top_of_normal takes normality as an instance, so pass only the subgroup. Gotcha: Subgroup.mem_centralizer_singleton_iff is g ∈ C{h} ↔ g * h = h * g.