M : Type ?u.17813
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
M : Type ?u.17813
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
no goals
M : Type ?u.17813
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
exact mul_div_mul_right _ _ (Nat.cast_ne_zero.mpr Finite.card_pos.ne')