M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } ≤ Nat.card { p // p.fst * p.snd = p.snd * p.fst }

case h
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0

M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ 0 < ↑(Nat.card { x // x ∈ H }) ^ 2
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ commProb { x // x ∈ H } ≤ commProb G * ↑(index H) ^ 2
rw [commProb_def, commProb_def, div_le_iff, mul_assoc, ← mul_pow, ← Nat.cast_mul,
  mul_comm H.index, H.card_mul_index, div_mul_cancel, Nat.cast_le]
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ Function.Injective fun p =>
    { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } ≤ Nat.card { p // p.fst * p.snd = p.snd * p.fst }
refine' Finite.card_le_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) _
no goals
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ Function.Injective fun p =>
    { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h
no goals
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
p q : { p // p.fst * p.snd = p.snd * p.fst }
h :
  (fun p => { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }) p =
    (fun p => { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }) q
⊢ p = q
simpa only [Subtype.ext_iff, Prod.ext_iff] using h
no goals
case h
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
no goals
M : Type ?u.20589
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Group G
H : Subgroup G
⊢ 0 < ↑(Nat.card { x // x ∈ H }) ^ 2
exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2