awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀
refine_4 : b ≤ g → ¬b = 0 → b < a → a⁻¹ < b⁻¹
⊢ b ≤ g → ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
_
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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⁻¹

Tactic:
inv_strictAnti₀ ?_

Premises used: inv_strictAnti₀
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_4 : 0 < b
⊢ b < a → a⁻¹ < b⁻¹

Tactic:
refine inv_strictAnti₀ ?_

Premises used: inv_strictAnti₀
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 0 < b

Tactic:
simp [zero_lt_iff, hb0]

Premises used: zero_lt_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
⊢ WellFoundedGT { v : WithZero (Multiplicative ℤ) // v ≤ 1 }

Tactic:
{ wf :=
    (LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
    one_ne_zero).mpr instNonemptyOfInhabited }

Premises used: Iff.mpr, IsWellFounded.mk, instNonemptyOfInhabited, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, one_ne_zero
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CommMonoid β
inst_3 : PartialOrder β
e : α ≃*o β
inst_4 : MulArchimedean α
arch : ∀ (x : β) {y : β}, 1 < y → ∃ (n : ℕ), x ≤ y ^ n
⊢ MulArchimedean β

Tactic:
constructor
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ LT.lt.{u_2} (α := α) (1 : α) ((e.symm : (a : β) → α) y : α)

Tactic:
simp [← map_lt_map_iff e, hxy]

Premises used: map_lt_map_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ LT.lt.{u_2} (α := α) (1 : α) ((e.symm : (a : β) → α) y : α)

Tactic:
replace hxy : 1 < e.symm y := by simp [← map_lt_map_iff e, hxy]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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

Tactic:
(MulArchimedean.arch (e.symm x) hxy).imp ?_

Premises used: Exists.imp, OrderMonoidIso.symm, DFunLike.coe, MulArchimedean.arch
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : α)
arch : ∀ (a : ℕ), (e.symm : (a : β) → α) x ≤ HPow.hPow (α := α) ((e.symm : (a : β) → α) y : α) a → x ≤ y ^ a
⊢ ∃ (n : ℕ), x ≤ y ^ n

Tactic:
refine (MulArchimedean.arch (e.symm x) hxy).imp ?_

Premises used: Exists.imp, OrderMonoidIso.symm, DFunLike.coe, MulArchimedean.arch
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : α)
⊢ ∀ (a : ℕ), (e.symm : (a : β) → α) x ≤ HPow.hPow (α := α) ((e.symm : (a : β) → α) y : α) a → x ≤ y ^ a

Tactic:
simp [← map_pow, ← map_le_map_iff e]

Premises used: OrderIsoClass.map_le_map_iff, map_pow
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
mp : MulArchimedean.{u_2} (WithZero α) → MulArchimedean α
mpr : MulArchimedean α → MulArchimedean.{u_2} (WithZero α)
⊢ MulArchimedean.{u_2} (WithZero α) ↔ MulArchimedean α

Tactic:
constructor
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
h : MulArchimedean.{u_2} (WithZero α)
⊢ MulArchimedean α

Tactic:
OrderMonoidIso.unitsWithZero.mulArchimedean

Premises used: OrderMonoidIso.mulArchimedean
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
h : MulArchimedean.{u_2} (WithZero α)
⊢ MulArchimedean α

Tactic:
exact OrderMonoidIso.unitsWithZero.mulArchimedean

Premises used: OrderMonoidIso.mulArchimedean
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
h : MulArchimedean α
⊢ MulArchimedean.{u_2} (WithZero α)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
mp : MulArchimedean.{u_2} G₀ˣ → MulArchimedean G₀
mpr : MulArchimedean G₀ → MulArchimedean.{u_2} G₀ˣ
⊢ MulArchimedean.{u_2} G₀ˣ ↔ MulArchimedean G₀

Tactic:
constructor
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
h : MulArchimedean.{u_2} G₀ˣ
⊢ MulArchimedean G₀

Tactic:
OrderMonoidIso.withZeroUnits.mulArchimedean

Premises used: OrderMonoidIso.mulArchimedean
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
h : MulArchimedean.{u_2} G₀ˣ
⊢ MulArchimedean G₀

Tactic:
exact OrderMonoidIso.withZeroUnits.mulArchimedean

Premises used: OrderMonoidIso.mulArchimedean
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
h : MulArchimedean G₀
⊢ MulArchimedean.{u_2} G₀ˣ

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
X : Type u_2
inst_4 : Preorder X
inst_5 : LocallyFiniteOrder X
⊢ ∀ {a b : Multiplicative X},
    LE.le (α := X) ((Multiplicative.toAdd : (a : Multiplicative X) → X) a : X)
        ((Multiplicative.toAdd : (a : Multiplicative X) → X) b : X) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
X : Type u_2
inst_4 : Preorder X
inst_5 : LocallyFiniteOrder X
⊢ ∀ {a b : Additive X},
    LE.le (α := X) ((Additive.toMul : (a : Additive X) → X) a : X) ((Additive.toMul : (a : Additive X) → X) b : X) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
X : Type u_2
inst_4 : Preorder X
inst_5 : LocallyFiniteOrder X
inst_6 : Monoid X
⊢ ∀ {a b : Xˣ},
    LE.le (α := X) (({ toFun := Units.val, inj' := ⋯ } : (a : Xˣ) → X) a : X)
        (({ toFun := Units.val, inj' := ⋯ } : (a : Xˣ) → X) b : X) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
X : Type u_2
inst : LT X
⊢ DenselyOrdered.{u_2} (Additive X) ↔ DenselyOrdered X

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
X : Type u_2
inst : LT X
⊢ DenselyOrdered.{u_2} (Multiplicative X) ↔ DenselyOrdered X

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
X : Type u_2
inst_4 : LT X
inst_5 : DenselyOrdered X
⊢ DenselyOrdered.{u_2} (Multiplicative X)

Tactic:
denselyOrdered_multiplicative_iff.2 ‹_›

Premises used: Iff.mpr, denselyOrdered_multiplicative_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
X : Type u_2
inst_4 : LT X
inst_5 : DenselyOrdered X
⊢ DenselyOrdered.{u_2} (Additive X)

Tactic:
denselyOrdered_additive_iff.2 ‹_›

Premises used: Iff.mpr, denselyOrdered_additive_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
M : Type u_3
inst : Preorder M
inst_1 : NoMinOrder M
⊢ DenselyOrdered.{u_3} (WithZero M) ↔ DenselyOrdered M

Tactic:
WithBot.denselyOrdered_iff

Premises used: WithZero, WithBot.denselyOrdered_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
X_1 : Type u_2
inst_4 : LT X_1
X : Type u_3
inst_5 : Preorder X
inst_6 : NoMinOrder X
inst_7 : DenselyOrdered X
⊢ DenselyOrdered.{u_3} (WithZero X)

Tactic:
WithZero.denselyOrdered_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, WithZero.denselyOrdered_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ ¬DenselyOrdered ℤ

Tactic:
(LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered ℤ).mp ⟨.refl _⟩

Premises used: OrderAddMonoidIso.refl, LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered, Int, Nonempty.intro, Iff.mp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ ¬DenselyOrdered (WithZero (Multiplicative ℤ))

Tactic:
(LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered _).mp ⟨.refl _⟩

Premises used: Nonempty.intro, OrderMonoidIso.refl, Iff.mp, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : LocallyFiniteOrder X
s : Set (WithZero X)
⊢ DenselyOrdered.{u_3} (↑s : Type u_3) ↔ s.Subsingleton

Tactic:
WithBot.denselyOrdered_set_iff_subsingleton

Premises used: Set.Mem, WithZero, WithBot.denselyOrdered_set_iff_subsingleton
-- Module: Mathlib.GroupTheory.ClassEquation
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)
this : (x : ConjClasses G) × (↑x.carrier : Type u_1) ≃ G
⊢ ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G

Tactic:
simpa using (Fintype.card_congr this)

Premises used: Fintype.card_congr
-- Module: Mathlib.GroupTheory.ClassEquation
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)
suffices : (x : ConjClasses G) × (↑x.carrier : Type u_1) ≃ G
⊢ ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G

Tactic:
suffices (Σ x : ConjClasses G, x.carrier) ≃ G by simpa using (Fintype.card_congr this)
-- Module: Mathlib.GroupTheory.ClassEquation
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 : Type u_1) ≃ G

Tactic:
simpa [carrier_eq_preimage_mk] using Equiv.sigmaFiberEquiv ConjClasses.mk

Premises used: ConjClasses.carrier_eq_preimage_mk, Equiv.sigmaFiberEquiv, ConjClasses.mk
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro : ∀ (val : Fintype G), ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]

Premises used: sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro : ∀ (val : Fintype G), ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card 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]

Premises used: sum_conjClasses_card_eq_card, nonempty_fintype, finsum_eq_sum_of_fintype
-- Module: Mathlib.GroupTheory.ClassEquation
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

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
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)
⊢ 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:
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]

Premises used: sum_conjClasses_card_eq_card, Set.toFinset, ConjClasses.noncenter, Finset.subset_univ, Nat.card_eq_fintype_card, Finset.sum_sdiff
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
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))
⊢ 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:
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]

Premises used: Set.toFinset_card, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.ClassEquation
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)
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))
⊢ 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:
congr 1
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Eq (α := ℕ)
    (∑ᶠ (i : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) i),
      Fintype.card.{u_1} (↑i.carrier : Type u_1))
    (∑ i ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑i.carrier : Type u_1))

Tactic:
finsum_cond_eq_sum_of_cond_iff _ _

Premises used: finsum_cond_eq_sum_of_cond_iff
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
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)
⊢ 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:
convert! finsum_cond_eq_sum_of_cond_iff _ _

Premises used: finsum_cond_eq_sum_of_cond_iff
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ ∀ {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:
simp [Set.mem_toFinset]

Premises used: Set.mem_toFinset
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
⊢ Fintype.card.{u_1} ↥(Subgroup.center G) = Fintype.card.{u_1} (↑(noncenter G)ᶜ : Type u_1)

Tactic:
Fintype.card_congr ((mk_bijOn G).equiv _)

Premises used: Fintype.card_congr, ConjClasses.mk_bijOn, Set.BijOn.equiv
-- Module: Mathlib.GroupTheory.ClassEquation
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))
rw₂ rw₃ :
  Finset.card (α := ConjClasses G) (Finset.univ \ 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))

Tactic:
rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]

Premises used: Finset.compl_eq_univ_sdiff, Set.toFinset_compl, Set.toFinset_card
-- Module: Mathlib.GroupTheory.ClassEquation
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)

Tactic:
?_
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
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)
⊢ Fintype.card.{u_1} ↥(Subgroup.center 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]
    _ = _ := ?_

Premises used: Fintype.card_congr, Finset.univ, Compl.compl, Membership.mem, Set.Elem, Fintype.card, Subtype, Subgroup.center, Set.toFinset, SDiff.sdiff, ConjClasses.mk_bijOn, Finset.card, ConjClasses.noncenter, Set.BijOn.equiv
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
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))
⊢ 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:
rw [Finset.card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones
-- Module: Mathlib.GroupTheory.ClassEquation
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))

Tactic:
Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
val : Fintype G
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)
⊢ 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:
refine Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.GroupTheory.ClassEquation
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)
⊢ (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

Premises used: Finset.mem_univ, Finset.mem_sdiff, Set.not_nontrivial_iff, Finset.mem_filter, Set.toFinset_setOf, ConjClasses.noncenter, true_and
-- Module: Mathlib.GroupTheory.ClassEquation
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
intro : ∃ (a : G), (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).toFinset = {a}
⊢ 1 = Fintype.card.{u_1} (↑(carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)) : Type u_1)

Tactic:
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]

Premises used: Finset.card_eq_one, Set.toFinset_card, eq_comm
-- Module: Mathlib.GroupTheory.ClassEquation
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
⊢ (↑(carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).toFinset : Set G) = (↑{g} : Set G)

Tactic:
simpa using hg.eq_singleton_of_mem mem_carrier_mk

Premises used: Set.Subsingleton.eq_singleton_of_mem, ConjClasses.mem_carrier_mk
-- Module: Mathlib.GroupTheory.ClassEquation
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
⊢ ∃ (a : G), (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).toFinset = {a}

Tactic:
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_2
inst : Group G
inst_1 : (x : ConjClasses G) → Fintype (↑x.carrier : Type u_2)
inst_2 : Fintype G
inst_3 : Fintype ↥(Subgroup.center G)
inst_4 : Fintype (↑(noncenter G) : Type u_2)
⊢ Nat.card.{u_2} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_2} (↑x.carrier : Type u_2) =
    Nat.card G

Tactic:
Group.nat_card_center_add_sum_card_noncenter_eq_card G

Premises used: Group.nat_card_center_add_sum_card_noncenter_eq_card