Brauer's permutation lemma and #real characters = #real classes in Lean without inverting the character table

The textbook proof of Brauer's permutation lemma writes PX = XQ with permutation matrices and an invertible character table X, then takes traces. In Lean, Matrix indexed by Fin n versus ConjClasses G is painful, and you don't need it. Let β : G → G respect conjugacy and permute the irreducible characters, i.e. each χ_i ∘ β is some χ_j. By the first orthogonality relation, |G|⁻¹ ∑_g χ_i(βg) χ_i(g⁻¹) is 1 or 0 according to whether χ_i ∘ β = χ_i. (If j ≠ i but χ_j = χ_i, orthogonality gives 0 = 1.) Sum over i and swap the sums (Finset.sum_comm). Column orthogonality turns ∑_i χ_i(g⁻¹) χ_i(βg) into [g ~ βg]·|C_G(g)|, and |C_G(g)|/|G| = 1/|g^G|. A 'sum of a class function divided by class size over G = sum over ConjClasses' lemma finishes, via Finset.sum_fiberwise with ConjClasses.mk. Instances: β = α for an automorphism, where ρ_i ∘ α has norm 1 by Fintype.sum_equiv α; and β = (·)⁻¹ via char_dual, which gives real characters = real classes. 'Norm 1 ⇒ some χ_j' needs only the character expansion with ℕ multiplicities plus ∑ m_j² = 1. For counting classes, state the predicate rep-free: ∀ g, ConjClasses.mk g = C → IsConj g (β g). Gotcha: simp unfolds IsConj to ∃ c, … via isConj_iff, so finish ite goals with split_ifs rather than simp. if_pos/if_neg and ite_cond_eq_true are deprecated in recent Mathlib.