refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier (#6290)

This PR moves a formula for the number of conjugacy classes earlier. The proof uses Burnside's theorem, so it cannot be moved any earlier than `GroupTheory/GroupAction/Quotient`.

Author: tb65536

Mathlib/Data/Fintype/Card.lean

@@ -1061,6 +1061,10 @@ instance Prod.infinite_of_left [Infinite α] [Nonempty β] : Infinite (α × β)
   Infinite.of_surjective Prod.fst Prod.fst_surjective
 #align prod.infinite_of_left Prod.infinite_of_left
 
+instance instInfiniteProdSubtypeCommute [Mul α] [Infinite α] :
+    Infinite { p : α × α // _root_.Commute p.1 p.2 } :=
+  Infinite.of_injective (fun a => ⟨⟨a, a⟩, rfl⟩) (by intro; simp)
+
 namespace Infinite
 
 private noncomputable def natEmbeddingAux (α : Type _) [Infinite α] : ℕ → α

Mathlib/GroupTheory/CommutingProbability.lean

@@ -60,9 +60,6 @@ theorem commProb_function [Fintype α] [Mul β] :
     commProb (α → β) = (commProb β) ^ Fintype.card α := by
   rw [commProb_pi, Finset.prod_const, Finset.card_univ]
 
-instance instInfiniteProdSubtypeCommute [Infinite M] : Infinite { p : M × M // Commute p.1 p.2 } :=
-  Infinite.of_injective (fun m => ⟨⟨m, m⟩, rfl⟩) (by intro; simp)
-
 @[simp]
 theorem commProb_eq_zero_of_infinite [Infinite M] : commProb M = 0 :=
   div_eq_zero_iff.2 (Or.inl (Nat.cast_eq_zero.2 Nat.card_eq_zero_of_infinite))
@@ -95,22 +92,6 @@ theorem commProb_eq_one_iff [h : Nonempty M] :
 
 variable (G : Type _) [Group G]
 
-theorem card_comm_eq_card_conjClasses_mul_card :
-    Nat.card { p : G × G // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G := by
-  rcases fintypeOrInfinite G; swap
-  · rw [Nat.card_eq_zero_of_infinite, @Nat.card_eq_zero_of_infinite G, mul_zero]
-  simp only [Nat.card_eq_fintype_card]
-  -- Porting note: Changed `calc` proof into a `rw` proof.
-  rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype fun g h : G ↦ Commute g h), card_sigma,
-    sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
-      (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g))
-      fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
-    MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, ConjAct.card,
-    (Setoid.ext fun g h ↦ (Setoid.comm' _).trans isConj_iff.symm :
-      MulAction.orbitRel (ConjAct G) G = IsConj.setoid G),
-    @card_congr' (Quotient (IsConj.setoid G)) (ConjClasses G) _ _ rfl]
-#align card_comm_eq_card_conj_classes_mul_card card_comm_eq_card_conjClasses_mul_card
-
 theorem commProb_def' : commProb G = Nat.card (ConjClasses G) / Nat.card G := by
   rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
   by_cases h : (Nat.card G : ℚ) = 0

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
+import Mathlib.Algebra.Group.ConjFinite
 import Mathlib.Algebra.Hom.GroupAction
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Dynamics.PeriodicPts
@@ -401,3 +402,25 @@ theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G)
 #align subgroup.quotient_center_embedding_apply Subgroup.quotientCenterEmbedding_apply
 
 end Subgroup
+
+section conjClasses
+
+open Fintype
+
+theorem card_comm_eq_card_conjClasses_mul_card (G : Type _) [Group G] :
+    Nat.card { p : G × G // _root_.Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G := by
+  classical
+  rcases fintypeOrInfinite G; swap
+  · rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
+  simp only [Nat.card_eq_fintype_card]
+  -- Porting note: Changed `calc` proof into a `rw` proof.
+  rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype _root_.Commute), card_sigma,
+    sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // _root_.Commute a b })
+      (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g))
+      fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
+    MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]
+  congr 1; apply card_congr'; congr; ext;
+  exact (Setoid.comm' _).trans isConj_iff.symm
+#align card_comm_eq_card_conj_classes_mul_card card_comm_eq_card_conjClasses_mul_card
+
+end conjClasses