M : Type ?u.6837
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } = Nat.card (ConjClasses G) * Nat.card G
M : Type ?u.6837
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } = Nat.card (ConjClasses G) * Nat.card G
haveI := Fintype.ofFinite G
M : Type ?u.6837
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ card { p // p.fst * p.snd = p.snd * p.fst } = card (ConjClasses G) * card G
M : Type ?u.6837
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ Nat.card { p // p.fst * p.snd = p.snd * p.fst } = Nat.card (ConjClasses G) * Nat.card G
simp only [Nat.card_eq_fintype_card]
no goals
M : Type ?u.6837
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ card { p // p.fst * p.snd = p.snd * p.fst } = card (ConjClasses G) * card G
rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype fun g h : G ↦ g * h = h * g), card_sigma,
  sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // a * b = b * a })
    (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, ConjAct.card,
  (Setoid.ext fun g h ↦ (Setoid.comm' _).trans isConj_iff.symm :
    MulAction.orbitRel (ConjAct G) G = IsConj.setoid G),
  @card_congr' (Quotient (IsConj.setoid G)) (ConjClasses G) _ _ rfl]