awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀
⊢ Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) x →
    Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} ((fun (x : G₀) ↦ x⁻¹) x)
have refine_3 : x ≤ g → ¬x = 0 → g⁻¹ ≤ x⁻¹
Tactic: simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, and_imp]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ g⁻¹ ≤ x⁻¹
have refine_3 : 0 < x
Tactic: refine inv_anti₀ ?_ hxg
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
⊢ ∀ (a : G₀),
    Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) a →
      ∀ (b : G₀),
        Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) b →
          a > b → Function.onFun (fun (x1 x2 : G₀) ↦ x1 < x2) (fun (x : G₀) ↦ x⁻¹) a b
have refine_4 : ∀ a ≤ g, ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹
Tactic: simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, gt_iff_lt, Function.onFun, and_imp]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
a : G₀
h_1 : a ≤ g
h_2 : ¬a = 0
b : G₀
h_3 : b ≤ g
hb0 : ¬b = 0
⊢ b < a → a⁻¹ < b⁻¹
have refine_4 : 0 < b
Tactic: refine inv_strictAnti₀ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CommMonoid β
inst_3 : PartialOrder β
e : α ≃*o β
inst_4 : MulArchimedean α
⊢ MulArchimedean β
have arch : ∀ (x : β) {y : β}, 1 < y → ∃ (n : ℕ), x ≤ y ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CommMonoid β
inst_3 : PartialOrder β
e : α ≃*o β
inst_4 : MulArchimedean α
x y : β
hxy : 1 < y
⊢ ∃ (n : ℕ), x ≤ y ^ n
have hxy₁ : LT.lt.{u_2} (α := α) (1 : α) ((e.symm : (a : β) → α) y : α)
Tactic: replace hxy : 1 < e.symm y := by simp [← map_lt_map_iff e, hxy]
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CommMonoid β
inst_3 : PartialOrder β
e : α ≃*o β
inst_4 : MulArchimedean α
x y : β
hxy : LT.lt.{u_2} (α := α) (1 : α) ((e.symm : (a : β) → α) y : α)
⊢ ∃ (n : ℕ), x ≤ y ^ n
have arch : ∀ (a : ℕ), (e.symm : (a : β) → α) x ≤ HPow.hPow (α := α) ((e.symm : (a : β) → α) y : α) a → x ≤ y ^ a
Tactic: refine (MulArchimedean.arch (e.symm x) hxy).imp ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
⊢ MulArchimedean.{u_2} (WithZero α) ↔ MulArchimedean α
have mp : MulArchimedean.{u_2} (WithZero α) → MulArchimedean α
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
mp : MulArchimedean.{u_2} (WithZero α) → MulArchimedean α
⊢ MulArchimedean.{u_2} (WithZero α) ↔ MulArchimedean α
have mpr : MulArchimedean α → MulArchimedean.{u_2} (WithZero α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean.{u_2} G₀ˣ ↔ MulArchimedean G₀
have mp : MulArchimedean.{u_2} G₀ˣ → MulArchimedean G₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
mp : MulArchimedean.{u_2} G₀ˣ → MulArchimedean G₀
⊢ MulArchimedean.{u_2} G₀ˣ ↔ MulArchimedean G₀
have mpr : MulArchimedean G₀ → MulArchimedean.{u_2} G₀ˣ
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype (ConjClasses G)
inst_2 : Fintype G
inst_3 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_1)
⊢ ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G
have suffices : (x : ConjClasses G) × (↑x.carrier : Type u_1) ≃ G
Tactic: suffices (Σ x : ConjClasses G, x.carrier) ≃ G by simpa using (Fintype.card_congr this)
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
have intro : ∀ (val : Fintype G), ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
have intro : ∀ (val : Fintype G), ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
Tactic: classical
  cases nonempty_fintype G
  simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro : ∀ (val : Fintype G),
  Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro : Nat.card.{u_1} ↥(Subgroup.center G) +
    ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
      Nat.card.{u_1} (↑x.carrier : Type u_1) =
  HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
    (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
Tactic: rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
      (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
have intro : Fintype.card.{u_1} ↥(Subgroup.center G) +
    ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
      Fintype.card.{u_1} (↑x.carrier : Type u_1) =
  HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
    (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
Tactic: simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Fintype.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Fintype.card.{u_1} (↑x.carrier : Type u_1) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
      (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
have intro : Fintype.card.{u_1} ↥(Subgroup.center G) =
  ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
intro :
  Fintype.card.{u_1} ↥(Subgroup.center G) =
    ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
⊢ Fintype.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Fintype.card.{u_1} (↑x.carrier : Type u_1) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
      (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
have intro₁ : Eq (α := ℕ)
  (∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
    Fintype.card.{u_1} (↑x.carrier : Type u_1))
  (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Eq (α := ℕ)
    (∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
      Fintype.card.{u_1} (↑x.carrier : Type u_1))
    (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
have intro : ∀ {x : ConjClasses G},
  Fintype.card.{u_1} (↑x.carrier : Type u_1) ≠ 0 →
    (Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x ↔
      Membership.mem (γ := Finset (ConjClasses G)) (Set.toFinset (noncenter G)) x)
Tactic: convert! finsum_cond_eq_sum_of_cond_iff _ _
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Fintype.card.{u_1} (↑(noncenter G)ᶜ : Type u_1) =
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
have rw : Finset.card (α := ConjClasses G) (Set.toFinset (noncenter G)ᶜ) =
  Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
Tactic: rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
rw :
  Finset.card (α := ConjClasses G) (Set.toFinset (noncenter G)ᶜ) =
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
⊢ Fintype.card.{u_1} (↑(noncenter G)ᶜ : Type u_1) =
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
have rw₁ : Finset.card (α := ConjClasses G) (Set.toFinset (noncenter G))ᶜ =
  Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
Tactic: rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
rw :
  Finset.card (α := ConjClasses G) (Set.toFinset (noncenter G)ᶜ) =
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
rw₁ :
  Finset.card (α := ConjClasses G) (Set.toFinset (noncenter G))ᶜ =
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
⊢ Fintype.card.{u_1} (↑(noncenter G)ᶜ : Type u_1) =
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
have rw₂ : Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G)) =
  Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G))
Tactic: rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Fintype.card.{u_1} ↥(Subgroup.center G) =
    ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
have intro : Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G)) =
  ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
Tactic: calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G)) =
    ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
have intro : Eq (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), 1)
  (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
Tactic: rw [Finset.card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Eq (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), 1)
    (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
have intro : ∀ (x : ConjClasses G),
  Membership.mem (γ := Finset (ConjClasses G)) (Finset.univ \ Set.toFinset (noncenter G)) x →
    1 = Fintype.card.{u_1} (↑x.carrier : Type u_1)
Tactic: refine Finset.sum_congr rfl ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
x : ConjClasses G
g : G
hg :
  Membership.mem (γ := Finset (ConjClasses G)) (Finset.univ \ Set.toFinset (noncenter G))
    (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ 1 = Fintype.card.{u_1} (↑(carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)) : Type u_1)
have hg₁ : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
Tactic: simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
x : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
⊢ 1 = Fintype.card.{u_1} (↑(carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)) : Type u_1)
have intro : ∃ (a : G), (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).toFinset = {a}
Tactic: rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro : ∀ (val : Fintype G),
  Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
Tactic: classical
  cases nonempty_fintype G
  rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
  simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
  congr 1
  swap
  · convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]
  calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
  rw [Finset.card_eq_sum_ones]
  refine Finset.sum_congr rfl ?_
  rintro ⟨g⟩ hg
  simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
  rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
  exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      Nat.card G
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro₁ : ∀ (val : Fintype G),
  Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
      (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
Tactic: classical
  cases nonempty_fintype G
  rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
  simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
  congr 1
  swap
  · convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]
  calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
  rw [Finset.card_eq_sum_ones]
  refine Finset.sum_congr rfl ?_
  rintro ⟨g⟩ hg
  simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
  rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
  exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      Nat.card G
intro₁ :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
        (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro₂ : ∀ (val : Fintype G),
  Fintype.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Fintype.card.{u_1} (↑x.carrier : Type u_1) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
      (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
Tactic: classical
  cases nonempty_fintype G
  rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
  simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
  congr 1
  swap
  · convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]
  calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
  rw [Finset.card_eq_sum_ones]
  refine Finset.sum_congr rfl ?_
  rintro ⟨g⟩ hg
  simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
  rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
  exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      Nat.card G
intro₁ :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
        (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
intro₂ :
  ∀ (val : Fintype G),
    Fintype.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Fintype.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
        (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G
have intro₃ : ∀ (val : Fintype G),
  Fintype.card.{u_1} ↥(Subgroup.center G) =
    ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
Tactic: classical
  cases nonempty_fintype G
  rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
  simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
  congr 1
  swap
  · convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]
  calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
  rw [Finset.card_eq_sum_ones]
  refine Finset.sum_congr rfl ?_
  rintro ⟨g⟩ hg
  simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
  rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
  exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩