M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
haveI := Fintype.ofFinite M
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | x.fst * x.snd = x.snd * x.fst}) / ↑(card M) ^ 2 = 1 ↔ Commutative fun x x_1 => x * x_1
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | x.fst * x.snd = x.snd * x.fst}) ↔ Commutative fun x x_1 => x * x_1

M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | x.fst * x.snd = x.snd * x.fst}) / ↑(card M) ^ 2 = 1 ↔ Commutative fun x x_1 => x * x_1
rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
  set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
no goals
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | x.fst * x.snd = x.snd * x.fst}) ↔ Commutative fun x x_1 => x * x_1
exact ⟨fun h x y ↦ h (x, y), fun h x ↦ h x.1 x.2⟩
no goals
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)