-- Mathlib/GroupTheory/GroupAction/CardCommute.lean
theorem card_comm_eq_card_conjClasses_mul_card (G : Type*) [Group G] :
    Nat.card { p : G × G // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Proof state:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card { p // Commute p.1 p.2 } = card (ConjClasses G) * card G

Tactic:
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 G g))
    fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq,
  MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]

Result:
case inl
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

Proof state:
case inl.e_a
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)

Tactic:
apply card_congr'

Result:
case inl.e_a.h
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G

Proof state:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]

Result:
no goals

Proof state:
case inl.e_a.h
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G

Tactic:
congr

Result:
case inl.e_a.h.e_s
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G

Proof state:
G : Type u_1
inst✝ : Group G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
rcases fintypeOrInfinite G

Result:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Proof state:
case inl.e_a.h.e_s.a
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
a✝ b✝ : G
⊢ (MulAction.orbitRel (ConjAct G) G) a✝ b✝ ↔ (IsConj.setoid G) a✝ b✝

Tactic:
exact (Setoid.comm' _).trans isConj_iff.symm

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
swap

Result:
case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Proof state:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
simp only [Nat.card_eq_fintype_card]

Result:
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card { p // Commute p.1 p.2 } = card (ConjClasses G) * card G

Proof state:
case inl
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

Tactic:
congr 1

Result:
case inl.e_a
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)

Proof state:
case inl.e_a.h.e_s
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G

Tactic:
ext

Result:
case inl.e_a.h.e_s.a
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
a✝ b✝ : G
⊢ (MulAction.orbitRel (ConjAct G) G) a✝ b✝ ↔ (IsConj.setoid G) a✝ b✝