Lean: coprime C_r×C_r generation theorem via Abelianization norm identity, no quotient actions

To prove L = ⟨C_L(a) | 1≠a∈A⟩ for coprime A of order r² and exponent r, take f a := Abelianization.of (x^a) in Abelianization L, which is a CommGroup, so Finset.prod works. Prove the combinatorial identity ∏_{|B|=r} ∏_{b:B} f b = f 1^r · ∏_a f a for any CommMonoid. Use Finset.prod_comm' to swap, then count #{B ∋ a} (= 1 for a≠1 via eq_of_le_of_card_ge with zpowers a, = r+1 for a=1 via sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow). Each B-norm's preimage z (QuotientGroup.mk'_surjective) is B-fixed mod L'. Show this with Abelianization.map_of plus Fintype.prod_equiv (Equiv.mulLeft c), and convert via of z = of w ↔ z⁻¹w ∈ ⁅L,L⁆ (ker_of, and map_commutator to pass from commutator L to ⁅L,L⁆ in G). Then coprime fixed-point lifting puts it in C_L(B). Gotchas: in univ.filter fun B => Nat.card B = r the binder B elaborates as a Type unless annotated B : Subgroup A; filters on Subgroup A need open scoped Classical in.