Lean: a free action on conjugacy classes, and 1-dim reps are irreducible, in a few lines

Two small patterns from Frobenius-group and Mackey work.

(1) Let a group H act on {C : ConjClasses K // C ≠ ConjClasses.mk 1} through automorphisms c h : MulAut K. Define smul h C := ⟨ConjClasses.map (c h).toMonoidHom C.1, _⟩. To prove one_smul and mul_smul, take obtain ⟨x, rfl⟩ := ConjClasses.mk_surjective C, then change ConjClasses.mk _ = ConjClasses.mk _, because map on mk is definitional. Finish with congr 1 and Subtype.ext (by simp). For a fixed class, rewrite with ConjClasses.mk_eq_mk_iff_isConj, which gives an IsConj statement. To get x = 1 from (c h) x = 1, use (c h).injective (h1.trans (map_one _).symm); rw [map_eq_one_iff] failed because of the MulEquiv.toMonoidHom coercion. With trivial stabilizers, MulAction.card_eq_sum_card_group_div_card_stabilizer, then Fintype.card_subtype_compl and Fintype.card_subtype_eq, give |H| ∣ k(K) - 1.

(2) A rep ψ with finrank U = 1 is irreducible because dim End(ψ) = 1. For the upper bound, use LinearMap.finrank_le_finrank_of_injective on IntertwiningMap.toLinearMapl ψ ψ: its explicit arguments are the two reps, and injectivity is fun f g h ↦ IntertwiningMap.ext (by simpa using h). Combine with Module.finrank_linearMap. For the lower bound, use IntertwiningMap.id ≠ 0. Get FiniteDimensional from Module.finite_of_finrank_eq_succ hU. Then the irreducible-from-dim-End-1 lemma (via isSimpleModule_of_finrank_end_eq_one) finishes.