[GOAL]
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ commProb (M × M') = commProb M * commProb M'
[PROOFSTEP]
simp_rw [commProb_def, div_mul_div_comm, Nat.card_prod, Nat.cast_mul, mul_pow, ← Nat.cast_mul, ← Nat.card_prod, Commute,
  SemiconjBy, Prod.ext_iff]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // (p.fst * p.snd).fst = (p.snd * p.fst).fst ∧ (p.fst * p.snd).snd = (p.snd * p.fst).snd }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // p.fst * p.snd = p.snd * p.fst } × { p // p.fst * p.snd = p.snd * p.fst })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ Nat.card { p // (p.fst * p.snd).fst = (p.snd * p.fst).fst ∧ (p.fst * p.snd).snd = (p.snd * p.fst).snd } =
    Nat.card ({ p // p.fst * p.snd = p.snd * p.fst } × { p // p.fst * p.snd = p.snd * p.fst })
[PROOFSTEP]
exact
  Nat.card_congr
    ⟨fun x => ⟨⟨⟨x.1.1.1, x.1.2.1⟩, x.2.1⟩, ⟨⟨x.1.1.2, x.1.2.2⟩, x.2.2⟩⟩, fun x =>
      ⟨⟨⟨x.1.1.1, x.2.1.1⟩, ⟨x.1.1.2, x.2.1.2⟩⟩, ⟨x.1.2, x.2.2⟩⟩, fun x => rfl, fun x => rfl⟩
[GOAL]
M : Type u_1
inst✝² : Mul M
α : Type u_3
i : α → Type u_2
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a : α, commProb (i a)
[PROOFSTEP]
simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod, ← Nat.card_pi, Commute, SemiconjBy,
  Function.funext_iff]
[GOAL]
M : Type u_1
inst✝² : Mul M
α : Type u_3
i : α → Type u_2
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // ∀ (a : α), (p.fst * p.snd) a = (p.snd * p.fst) a }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // p.fst * p.snd = p.snd * p.fst })) / ↑(Nat.card ((a : α) → i a)) ^ 2
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
M : Type u_1
inst✝² : Mul M
α : Type u_3
i : α → Type u_2
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ Nat.card { p // ∀ (a : α), (p.fst * p.snd) a = (p.snd * p.fst) a } =
    Nat.card ((a : α) → { p // p.fst * p.snd = p.snd * p.fst })
[PROOFSTEP]
exact
  Nat.card_congr
    ⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1, fun a => (x a).1.2⟩, fun a => (x a).2⟩,
      fun x => rfl, fun x => rfl⟩
[GOAL]
M : Type u_1
inst✝² : Mul M
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Mul β
⊢ commProb (α → β) = commProb β ^ card α
[PROOFSTEP]
rw [commProb_pi, Finset.prod_const, Finset.card_univ]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ commProb M ≤ 1
[PROOFSTEP]
refine' div_le_one_of_le _ (sq_nonneg (Nat.card M : ℚ))
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ ↑(Nat.card { p // Commute p.fst p.snd }) ≤ ↑(Nat.card M) ^ 2
[PROOFSTEP]
rw [← Nat.cast_pow, Nat.cast_le, sq, ← Nat.card_prod]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ Nat.card { p // Commute p.fst p.snd } ≤ Nat.card (M × M)
[PROOFSTEP]
apply Finite.card_subtype_le
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
haveI := Fintype.ofFinite M
[GOAL]
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
[PROOFSTEP]
rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | Commute x.fst x.snd}) / ↑(card M) ^ 2 = 1 ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
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]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.fst x.snd}) ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
exact ⟨fun h x y ↦ h (x, y), fun h x ↦ h x.1 x.2⟩
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
[PROOFSTEP]
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
[GOAL]
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
⊢ commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
[GOAL]
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
by_cases h : (Nat.card G : ℚ) = 0
[GOAL]
case pos
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
rw [h, zero_mul, div_zero, div_zero]
[GOAL]
case neg
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
exact mul_div_mul_right _ _ h
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ commProb { x // x ∈ H } ≤ commProb G * ↑(index H) ^ 2
[PROOFSTEP]
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]
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.fst p.snd } ≤ Nat.card { p // Commute p.fst p.snd }
[PROOFSTEP]
refine' Finite.card_le_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) _
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Function.Injective fun p =>
    { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }
[PROOFSTEP]
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
p q : { p // Commute p.fst p.snd }
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
[PROOFSTEP]
simpa only [Subtype.ext_iff, Prod.ext_iff] using h
[GOAL]
case h
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0
[PROOFSTEP]
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card { x // x ∈ H }) ^ 2
[PROOFSTEP]
exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2
[GOAL]
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card { x // x ∈ H })
[PROOFSTEP]
rw [commProb_def', commProb_def', div_le_iff, mul_assoc, ← Nat.cast_mul, ← Subgroup.index, H.card_mul_index,
  div_mul_cancel, Nat.cast_le]
[GOAL]
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)
[PROOFSTEP]
apply Finite.card_le_of_surjective
[GOAL]
case hf
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective ?f
case f
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ ConjClasses G → ConjClasses (G ⧸ H)
[PROOFSTEP]
show Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
[GOAL]
case hf
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
[PROOFSTEP]
exact ConjClasses.map_surjective Quotient.surjective_Quotient_mk''
[GOAL]
case h
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ ↑(Nat.card G) ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'
[GOAL]
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ 0 < ↑(Nat.card (G ⧸ H))
[PROOFSTEP]
exact Nat.cast_pos.mpr Finite.card_pos
