M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)

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

M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ 0 < ↑(Nat.card (G ⧸ H))
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card { x // x ∈ H })
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]
case hf
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective ?f

case f
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ConjClasses G → ConjClasses (G ⧸ H)
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)
apply Finite.card_le_of_surjective
case hf
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
case hf
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective ?f

case f
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ConjClasses G → ConjClasses (G ⧸ H)
show Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
no goals
case hf
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
exact ConjClasses.map_surjective Quotient.surjective_Quotient_mk''
no goals
case h
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ↑(Nat.card G) ≠ 0
exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'
no goals
M : Type ?u.28957
inst✝⁵ : Mul M
inst✝⁴ : Finite M
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ 0 < ↑(Nat.card (G ⧸ H))
exact Nat.cast_pos.mpr Finite.card_pos