awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
hkB'₁ : k • B' = B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hgkB'₁ : k • B' = g • B'
Tactic: rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'
Cleared hypotheses: hkB', hgkB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
inr : k • B' = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have inr₁ : B' = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
Tactic: rw [← hgkB', hkB']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
    Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
have H : 0 < Fintype.card.{u_1} ↥(stabilizer α (φ ω))
Tactic: rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
        Fintype.card_prod, Nat.mul_div_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
have this : ∀ (ω : Quotient (orbitRel α β)),
  Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
    Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
Tactic: 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)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
have simp_rw : Fintype.card β =
  ∑ x : Quotient (orbitRel α β), Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ x)))
Tactic: simp_rw [this, ← Fintype.card_sigma,
      Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
simp_rw :
  Fintype.card β =
    ∑ x : Quotient (orbitRel α β), Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ x)))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
have simp_rw₁ : Fintype.card β =
  Fintype.card ((i : Quotient (orbitRel α β)) × HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ i)))
Tactic: simp_rw [this, ← Fintype.card_sigma,
      Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
have have : ∀ (ω : Quotient (orbitRel α β)),
  Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
    Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
Tactic: 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φ)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Group α
inst_1 : MulAction α β
inst_2 : Fintype α
inst_3 : Fintype β
inst_4 : Fintype (Quotient (orbitRel α β))
inst_5 : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
have :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
      Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
have have₁ : ∀
  (this :
    ∀ (ω : Quotient (orbitRel α β)),
      Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω)) =
        Fintype.card.{u_1} (HasQuotient.Quotient α (B := Subgroup α) (stabilizer α (φ ω)))),
  Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card.{u_1} ↥(stabilizer α (φ ω))
Tactic: 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φ)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
Tactic: rcases fintypeOrInfinite G
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inr : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
Tactic: rcases fintypeOrInfinite G
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Infinite G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inr : Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card G * Nat.card.{u_3} (ConjClasses G)
Tactic: rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Infinite G
inr : Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card G * Nat.card.{u_3} (ConjClasses G)
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inr₁ : 0 = Nat.card G * Nat.card.{u_3} (ConjClasses G)
Tactic: rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Infinite G
inr : Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card G * Nat.card.{u_3} (ConjClasses G)
inr₁ : 0 = Nat.card G * Nat.card.{u_3} (ConjClasses G)
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inr₂ : 0 = 0 * Nat.card.{u_3} (ConjClasses G)
Tactic: rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Infinite G
inr : Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card G * Nat.card.{u_3} (ConjClasses G)
inr₁ : 0 = Nat.card G * Nat.card.{u_3} (ConjClasses G)
inr₂ : 0 = 0 * Nat.card.{u_3} (ConjClasses G)
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inr₃ : Eq (α := ℕ) 0 0
Tactic: rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inl : card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} (ConjClasses G) * card G
Tactic: simp only [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) * card.{u_3} (ConjAct G) =
    card.{u_3} (ConjClasses G) * card G
have e_a : card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) = card.{u_3} (ConjClasses G)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) = card.{u_3} (ConjClasses G)
have e_a : Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G
Tactic: apply card_congr'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G
have e_a : MulAction.orbitRel (ConjAct G) G = IsConj.setoid G
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G
have e_a : ∀ (a b : G), (MulAction.orbitRel (ConjAct G) G : G → G → Prop) a b ↔ (IsConj.setoid G : G → G → Prop) a b
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
val : Fintype G
⊢ card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} (ConjClasses G) * card G
have calc : card.{u_3} (Quotient (MulAction.orbitRel (ConjAct G) G)) * card.{u_3} (ConjAct G) = card.{u_3} (ConjClasses G) * card G
Tactic: calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            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
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
Tactic: 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]
  calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            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
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inr : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
Tactic: 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]
  calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            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
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.CardCommute (goal)
Goal:
G : Type u_3
inst : Group G
inl : ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inr : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inl₁ :
  ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inr₁ inr₂ : Infinite G → Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
inl₂ inl₃ :
  ∀ (val : Fintype G), Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
⊢ Nat.card.{u_3} { p : G × G // Commute p.1 p.2 } = Nat.card.{u_3} (ConjClasses G) * Nat.card G
have inl₄ : ∀ (val : Fintype G), card.{u_3} { p : G × G // Commute p.1 p.2 } = card.{u_3} (ConjClasses G) * card G
Tactic: 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]
  calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            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
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
inst_1 : SMul α M
inst_2 : SMulCommClass α M M
inst_3 : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • um • m = um • a • m
have rw : a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
  um • a • m
Tactic: rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
inst_1 : SMul α M
inst_2 : SMulCommClass α M M
inst_3 : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
rw :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    um • a • m
⊢ a • um • m = um • a • m
have rw₁ : a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
  (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * a • m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
Tactic: rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
inst_1 : SMul α M
inst_2 : SMulCommClass α M M
inst_3 : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
rw :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    um • a • m
rw₁ :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * a • m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
⊢ a • um • m = um • a • m
have rw₂ : a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m) * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
Tactic: rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Monoid M
inst_1 : SMul α M
inst_2 : SMulCommClass α M M
inst_3 : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
rw :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    um • a • m
rw₁ :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * a • m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
rw₂ :
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
    a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m) * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)
⊢ a • um • m = um • a • m
have rw₃ : a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M)) =
  a • ((↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um) : M) * m * (↑((ofConjAct : (a : ConjAct Mˣ) → Mˣ) um)⁻¹ : M))
Tactic: rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ HSMul.hSMul (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) g⁻¹ : ConjAct G) h = g⁻¹ * h * g
have rw : g⁻¹ * h * g⁻¹⁻¹ = g⁻¹ * h * g
Tactic: rw [toConjAct_smul, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
G : Type u_3
inst : Group G
g h : G
rw : g⁻¹ * h * g⁻¹⁻¹ = g⁻¹ * h * g
⊢ HSMul.hSMul (α := ConjAct G) ((toConjAct : (a : G) → ConjAct G) g⁻¹ : ConjAct G) h = g⁻¹ * h * g
have rw₁ : g⁻¹ * h * g = g⁻¹ * h * g
Tactic: rw [toConjAct_smul, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
inst_1 : SMul α G
inst_2 : SMulCommClass α G G
inst_3 : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • ug • g = ug • a • g
have rw : a •
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
  ug • a • g
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
inst_1 : SMul α G
inst_2 : SMulCommClass α G G
inst_3 : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
rw :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    ug • a • g
⊢ a • ug • g = ug • a • g
have rw₁ : a •
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
  HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) (a • g))
    (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.ConjAct (goal)
Goal:
α : Type u_1
M : Type u_2
G : Type u_3
inst : Group G
inst_1 : SMul α G
inst_2 : SMulCommClass α G G
inst_3 : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
rw :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    ug • a • g
rw₁ :
  a •
      HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
        (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) (a • g))
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
⊢ a • ug • g = ug • a • g
have rw₂ : a •
    HMul.hMul (β := G) (HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
      (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G) =
  HMul.hMul (β := G) (a • HMul.hMul (α := G) ((ofConjAct : (a : ConjAct G) → G) ug : G) g)
    (((ofConjAct : (a : ConjAct G) → G) ug)⁻¹ : G)
Tactic: rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]