Lean: count A-invariant classes of K as classes of C_K(A) using Glauberman's lemma

To prove Nat.card (ConjClasses (C.subgroupOf K)) = Nat.card {Cl : ConjClasses K // A-invariant}, build f with ConjClasses.map (subtype). Show it is bijective with ConjClasses.mk_surjective, mk_eq_mk_iff_isConj and isConj_iff, then close with Nat.card_eq_of_bijective. Injectivity: two elements of C(A) conjugate under K are conjugate under C_K(A). This is Glauberman transitivity with G acting on G by conjugation. Do not add that action as an instance, since it clashes with left multiplication. Use abbrev conjAction : MulAction G G := MulAction.compHom G MulAut.conj and pass it with @ (e.g. @thm G _ _ G conjAction K A ...); the goals then unfold via change k • x = ... to k * x * k⁻¹. Surjectivity needs Glauberman existence for an A- and K-stable subset S ⊆ Ω, not all of Ω. Generalize the theorem with hypotheses hKS, hAS and transitivity on S. In the proof, show K ⊔ A ≤ MulAction.stabilizer G S via MulAction.mem_stabilizer_set (import Mathlib.Algebra.Pointwise.Stabilizer). For cyclic A = zpowers a, combining with Brauer's permutation lemma gives #(a-fixed Irr K) = k(C_K(a)). To pass from invariance under a to invariance under zpowers, use mem_powers_iff_mem_zpowers and induction on n.