M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ ↑(Nat.card { p // p.fst * p.snd = p.snd * p.fst }) ≤ ↑(Nat.card M) ^ 2
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ commProb M ≤ 1
refine' div_le_one_of_le _ (sq_nonneg (Nat.card M : ℚ))
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } ≤ Nat.card (M × M)
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ ↑(Nat.card { p // p.fst * p.snd = p.snd * p.fst }) ≤ ↑(Nat.card M) ^ 2
rw [← Nat.cast_pow, Nat.cast_le, sq, ← Nat.card_prod]
no goals
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } ≤ Nat.card (M × M)
apply Finite.card_subtype_le