[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
x✝³ x✝² x✝¹ : α
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H
[PROOFSTEP]
rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
b : { x // x ∈ ↑opposite (normalizer H) }
c x✝¹ : α
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (b • c)⁻¹ * b • x✝¹ ∈ H
[PROOFSTEP]
rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc, mem_normalizer_iff'.mp b.prop,
  mul_assoc, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
hH : Normal H
x✝³ : αᵐᵒᵖ
x✝² x✝¹ : α
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H
[PROOFSTEP]
rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc, mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : Group α
inst✝² : Monoid β
inst✝¹ : MulAction β α
H : Subgroup α
inst✝ : QuotientAction β H
b : β
q : α ⧸ H
⊢ ↑(b • Quotient.out' q) = b • q
[PROOFSTEP]
rw [← Quotient.smul_mk, QuotientGroup.out_eq']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
a : α
q : α ⧸ H
⊢ (Quotient.out' q)⁻¹ * a ^ minimalPeriod ((fun x x_1 => x • x_1) a) q * Quotient.out' q ∈ H
[PROOFSTEP]
rw [mul_assoc, ← QuotientGroup.eq', QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out', eq_comm,
  pow_smul_eq_iff_minimalPeriod_dvd]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
g : α ⧸ stabilizer α x
g1 g2 : α
H : Setoid.r g1 g2
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x
[PROOFSTEP]
rw [smul_smul, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ Setoid.r g₁ g₂
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer α x
[PROOFSTEP]
show (g₁⁻¹ * g₂) • x = x
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x
[PROOFSTEP]
rw [mul_smul, ← H, inv_smul_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x✝ b : β
x y : α ⧸ stabilizer α b
hxy :
  (fun g => { val := ofQuotientStabilizer α b g, property := (_ : ofQuotientStabilizer α b g ∈ orbit α b) }) x =
    (fun g => { val := ofQuotientStabilizer α b g, property := (_ : ofQuotientStabilizer α b g ∈ orbit α b) }) y
⊢ ofQuotientStabilizer α b x = ofQuotientStabilizer α b y
[PROOFSTEP]
convert congr_arg Subtype.val hxy
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁵ inst✝⁴ : Group α
inst✝³ : MulAction α β
x b : β
inst✝² : Fintype α
inst✝¹ : Fintype ↑(orbit α b)
inst✝ : Fintype { x // x ∈ stabilizer α b }
⊢ Fintype.card ↑(orbit α b) * Fintype.card { x // x ∈ stabilizer α b } = Fintype.card α
[PROOFSTEP]
rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ stabilizer G ↑1 = H
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G
⊢ x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H
[PROOFSTEP]
simp [QuotientGroup.eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
classical
have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω)) :=
  by
  intro ω
  rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)), Fintype.card_prod,
    Nat.mul_div_cancel]
  exact Fintype.card_pos_iff.mpr (by infer_instance)
simp_rw [this, ← Fintype.card_sigma, Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω)) :=
  by
  intro ω
  rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)), Fintype.card_prod,
    Nat.mul_div_cancel]
  exact Fintype.card_pos_iff.mpr (by infer_instance)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
[PROOFSTEP]
intro ω
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
[PROOFSTEP]
rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)), Fintype.card_prod,
  Nat.mul_div_cancel]
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr (by infer_instance)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Nonempty { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
simp_rw [this, ← Fintype.card_sigma, Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁵ inst✝⁴ : Group α
inst✝³ : MulAction α β
x : β
inst✝² : Fintype α
inst✝¹ : (a : α) → Fintype ↑(fixedBy α β a)
inst✝ : Fintype (Quotient (orbitRel α β))
⊢ ∑ a : α, Fintype.card ↑(fixedBy α β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α
[PROOFSTEP]
rw [← Fintype.card_prod, ← Fintype.card_sigma, Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y
[PROOFSTEP]
{ rintro ⟨x⟩ ⟨y⟩
  refine' ⟨y * x⁻¹, QuotientGroup.eq.mpr _⟩
  simp only [smul_eq_mul, H.one_mem, mul_left_inv, inv_mul_cancel_right]
}
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x✝¹ : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ∃ g, g • Quot.mk Setoid.r x = Quot.mk Setoid.r y
[PROOFSTEP]
refine' ⟨y * x⁻¹, QuotientGroup.eq.mpr _⟩
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x✝¹ : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ((fun x x_1 => x • x_1) (y * x⁻¹) x)⁻¹ * y ∈ H
[PROOFSTEP]
simp only [smul_eq_mul, H.one_mem, mul_left_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) =
    Fintype.card G / Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
classical
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
exact Fintype.card_pos_iff.mpr inferInstance
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) =
    Fintype.card G / Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) =
    Fintype.card (ConjAct G) / Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) = Fintype.card ↑(MulAction.orbit (ConjAct G) g)
case H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ 0 < Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ 0 < Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr inferInstance
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H = MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H ≤ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
[PROOFSTEP]
intro g hg
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
[PROOFSTEP]
apply Equiv.Perm.ext
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ ∀ (x : G ⧸ H), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) x = ↑1 x
[PROOFSTEP]
refine' fun q ↦ QuotientGroup.induction_on q _
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
⊢ ∀ (z : G), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) ↑z = ↑1 ↑z
[PROOFSTEP]
refine' fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr _)
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H
[PROOFSTEP]
rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
[PROOFSTEP]
exact H.normalCore.inv_mem hg g'⁻¹
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)) ≤ normalCore H
[PROOFSTEP]
refine' (Subgroup.normal_le_normalCore.mpr fun g hg => _)
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ g ∈ H
[PROOFSTEP]
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ ↑(g * 1) = ↑1
[PROOFSTEP]
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
classical
rcases fintypeOrInfinite G; swap
· rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
simp only [Nat.card_eq_fintype_card]
  -- Porting note: Changed `calc` proof into a `rw` proof.
rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma,
  sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
    (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g)) fun g ↦
    card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
  MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]
congr 1; apply card_congr'; congr; ext; exact (Setoid.comm' _).trans isConj_iff.symm
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
rcases fintypeOrInfinite G
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
case inr
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
swap
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card]
  -- Porting note: Changed `calc` proof into a `rw` proof.
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card { p // Commute p.fst p.snd } = card (ConjClasses G) * card G
[PROOFSTEP]
rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma,
  sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
    (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g)) fun g ↦
    card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
  MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) = card (ConjClasses G) * card G
[PROOFSTEP]
congr 1
[GOAL]
case inl.e_a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)
[PROOFSTEP]
apply card_congr'
[GOAL]
case inl.e_a.h
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G
[PROOFSTEP]
congr
[GOAL]
case inl.e_a.h.e_s
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G
[PROOFSTEP]
ext
[GOAL]
case inl.e_a.h.e_s.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
a✝ b✝ : G
⊢ Setoid.Rel (MulAction.orbitRel (ConjAct G) G) a✝ b✝ ↔ Setoid.Rel (IsConj.setoid G) a✝ b✝
[PROOFSTEP]
exact (Setoid.comm' _).trans isConj_iff.symm
