refactor(GroupTheory/CommutingProbability): Remove finite assumption (#…

…6224)

This PR removes the finite assumption on a couple lemmas.

Mathlib/GroupTheory/CommutingProbability.lean

@@ -93,11 +93,12 @@ theorem commProb_eq_one_iff [h : Nonempty M] :
   · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
 #align comm_prob_eq_one_iff commProb_eq_one_iff
 
-variable (G : Type _) [Group G] [Finite G]
+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
-  haveI := Fintype.ofFinite G
+  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,
@@ -112,11 +113,13 @@ theorem 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]
-  exact mul_div_mul_right _ _ (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
+  by_cases h : (Nat.card G : ℚ) = 0
+  · rw [h, zero_mul, div_zero, div_zero]
+  · exact mul_div_mul_right _ _ h
 #align comm_prob_def' commProb_def'
 
--- porting note: inserted [Group G]
-variable {G} [Group G] (H : Subgroup G)
+variable {G}
+variable [Finite G] (H : Subgroup G)
 
 theorem Subgroup.commProb_subgroup_le : commProb H ≤ commProb G * (H.index : ℚ) ^ 2 := by
   /- After rewriting with `commProb_def`, we reduce to showing that `G` has at least as many