awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : m < n
h : H (n - m) = H (n - (m + 1) + 1)
⊢ ⁅x, g⁆ ∈ H (n - m)

Tactic:
convert! hH x _ hx g using 1
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : m < n
h : H (n - m) = H (n + 1 - m.succ)
h₁ : H (n - m) = H (n + 1 - (m + 1))
h₂ h₃ : H (n - m) = H (n - m)
⊢ H (n - m) = H (n - (m + 1) + 1)

Tactic:
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]

Premises used: Nat.succ_eq_add_one, Nat.succ_le_of_lt, tsub_add_eq_add_tsub, Nat.add_sub_add_right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
rw :
  (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ↔
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rw [nilpotent_iff_finite_ascending_central_series]

Premises used: Subgroup.nilpotent_iff_finite_ascending_central_series
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
mp :
  (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) →
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
mpr :
  (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
⊢ (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ↔
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩

Premises used: HSub.hSub, Subgroup.is_descending_rev_series_of_is_ascending, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
mp : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊥
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
refine ⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
mp : H (n - n) = ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊥

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
mp : H 0 = ⊥
⊢ H (n - n) = ⊥

Tactic:
rw [tsub_self]

Premises used: tsub_self
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Tactic:
hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Tactic:
exact hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩

Premises used: HSub.hSub, And.intro, Exists.intro, Subgroup.is_ascending_rev_series_of_is_descending
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
mpr : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊤
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
refine ⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
mpr : H (n - n) = ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊤

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
mpr : H 0 = ⊤
⊢ H (n - n) = ⊤

Tactic:
rw [tsub_self]

Premises used: tsub_self
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
exact hH.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G 0) ⊤

Tactic:
rfl

Premises used: Subgroup.lowerCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G 1) (_root_.commutator G)

Tactic:
rfl

Premises used: Set.Mem, setOf, commutator, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_2
inst : AddGroup G
⊢ Eq (α := AddSubgroup G) (AddSubgroup.lowerCentralSeries G 1) (addCommutator G)

Tactic:
rfl

Premises used: Set.Mem, addCommutator, setOf, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
q : G
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) q ↔
    Membership.mem (γ := Subgroup G)
      (closure
        {x : G |
          ∃ (p : G),
            Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧
              ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x})
      q

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
⊢ Eq (α := Subgroup G) (lowerCentralSeries G (n + 1))
    (closure
      {x : G |
        ∃ (p : G),
          Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧
            ∃ (q : G), Membership.mem (γ := Subgroup G) ⊤ q ∧ ⁅p, q⁆ = x})

Tactic:
rfl

Premises used: Subgroup.lowerCentralSeries, rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ Characteristic (lowerCentralSeries G 0)

Tactic:
simp [topCharacteristic]

Premises used: Subgroup.topCharacteristic
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
d : ℕ
hd : Characteristic (lowerCentralSeries G d)
⊢ Characteristic (G := G) (Bracket.bracket (L := Subgroup G) (lowerCentralSeries G d) ⊤)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
n : ℕ
zero : Characteristic (lowerCentralSeries G 0)
succ : ∀ (d : ℕ) (hd : Characteristic (lowerCentralSeries G d)), Characteristic (lowerCentralSeries G (d + 1))
⊢ Characteristic (lowerCentralSeries G n)

Tactic:
induction n with
  | zero => simp [topCharacteristic]
  | succ d hd => unfold lowerCentralSeries; infer_instance

Premises used: Subgroup.lowerCentralSeries, Subgroup.topCharacteristic
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Antitone (β := Subgroup G) (lowerCentralSeries G)

Tactic:
antitone_nat_of_succ_le fun n x hx => ?_

Premises used: antitone_nat_of_succ_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
refine :
  ∀ (n : ℕ) (x : G) (hx : Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) x),
    Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x
⊢ Antitone (β := Subgroup G) (lowerCentralSeries G)

Tactic:
refine antitone_nat_of_succ_le fun n x hx => ?_

Premises used: antitone_nat_of_succ_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx : Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) x
⊢ Membership.mem (γ := Subgroup G)
    (closure {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x}) x

Tactic:
simp only [mem_lowerCentralSeries_succ_iff, mem_top,
    true_and] at hx

Premises used: Subgroup.mem_lowerCentralSeries_succ_iff, Subgroup.mem_top, true_and
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx :
  Membership.mem (γ := Subgroup G)
    (closure {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x}) x
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x

Tactic:
closure_induction ?_ (Subgroup.one_mem _) (fun _ _ _ _ ↦ mul_mem) (fun _ _ ↦ inv_mem) hx

Premises used: Subgroup.closure_induction
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx :
  Membership.mem (γ := Subgroup G)
    (closure {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x}) x
closure_induction :
  ∀ (x : G)
    (hx :
      Membership.mem (γ := Set G)
        {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x} x),
    Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x

Tactic:
refine
    closure_induction ?_ (Subgroup.one_mem _) (fun _ _ _ _ ↦ mul_mem) (fun _ _ ↦ inv_mem) hx
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx :
  Membership.mem (γ := Subgroup G)
    (closure {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x}) x
y z : G
hz : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) z
a : G
ha : ⁅z, a⁆ = y
rw : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) (z * (a * z⁻¹ * a⁻¹))
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) y

Tactic:
rw [← ha, commutatorElement_def, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹]

Premises used: commutatorElement_def, mul_assoc, Inv.inv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx :
  Membership.mem (γ := Subgroup G)
    (closure {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x}) x
y z : G
hz : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) z
a : G
ha : ⁅z, a⁆ = y
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) (z * (a * z⁻¹ * a⁻¹))

Tactic:
mul_mem hz (Normal.conj_mem inferInstance z⁻¹ (inv_mem hz) a)

Premises used: inferInstance, InvMemClass.inv_mem, Inv.inv, Subgroup.Normal.conj_mem, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx :
  Membership.mem (γ := Subgroup G)
    (closure {x : G | ∃ (p : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) p ∧ ∃ (q : G), ⁅p, q⁆ = x}) x
y z : G
hz : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) z
a : G
ha : ⁅z, a⁆ = y
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) (z * (a * z⁻¹ * a⁻¹))

Tactic:
exact mul_mem hz (Normal.conj_mem inferInstance z⁻¹ (inv_mem hz) a)

Premises used: inferInstance, InvMemClass.inv_mem, Inv.inv, Subgroup.Normal.conj_mem, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
left : Eq (α := Subgroup G) (lowerCentralSeries G 0) ⊤
right :
  ∀ (x : G) (n : ℕ),
    Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x →
      ∀ (g : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) ⁅x, g⁆
⊢ IsDescendingCentralSeries (lowerCentralSeries G)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (lowerCentralSeries G 0) ⊤

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
x : G
n : ℕ
hxn : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x
g : G
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) ⁅x, g⁆

Tactic:
commutator_mem_commutator hxn (mem_top g)

Premises used: Set.Mem, Subgroup.commutator_mem_commutator, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
x : G
n : ℕ
hxn : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x
g : G
⊢ Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) ⁅x, g⁆

Tactic:
exact commutator_mem_commutator hxn (mem_top g)

Premises used: Subgroup.commutator_mem_commutator, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
rw :
  (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ↔
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
rw [nilpotent_iff_finite_descending_central_series]

Premises used: Subgroup.nilpotent_iff_finite_descending_central_series
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
mp :
  (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
mpr :
  (∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) →
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
⊢ (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ↔
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
use n
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
h : lowerCentralSeries G n ≤ H n
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥

Tactic:
rw [eq_bot_iff, ← hn]

Premises used: eq_bot_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n

Tactic:
descending_central_series_ge_lower H ⟨h0, hs⟩ n

Premises used: Subgroup.descending_central_series_ge_lower, And.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n

Tactic:
exact descending_central_series_ge_lower H ⟨h0, hs⟩ n

Premises used: Subgroup.descending_central_series_ge_lower, And.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
⟨n, lowerCentralSeries G, lowerCentralSeries_isDescendingCentralSeries, hn⟩

Premises used: Subgroup.lowerCentralSeries_isDescendingCentralSeries, Subgroup.lowerCentralSeries, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
exact ⟨n, lowerCentralSeries G, lowerCentralSeries_isDescendingCentralSeries, hn⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : ¬IsNilpotent G
⊢ nilpotencyClass G = 0

Tactic:
dif_neg hG

Premises used: Group.nilpotencyClass, dif_neg
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : IsNilpotent G
⊢ nilpotencyClass G = Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯

Tactic:
dif_pos hG

Premises used: dif_pos, Group.nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw :
  Eq (α := Subgroup G)
    (upperCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯)) ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤

Tactic:
rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]

Premises used: Group.nilpotencyClass_def, Group.IsNilpotent.nilpotent, Nat.find_spec
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw :
  Eq (α := Subgroup G)
    (upperCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯)) ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤

Tactic:
classical
  rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]

Premises used: Group.nilpotencyClass_def
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → nilpotencyClass G ≤ n
mpr : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ ↔ nilpotencyClass G ≤ n

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
mp : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ ≤ n
⊢ nilpotencyClass G ≤ n

Tactic:
rw [nilpotencyClass_def]

Premises used: Group.nilpotencyClass_def
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ ≤ n

Tactic:
Nat.find_le h

Premises used: Nat.find_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯ ≤ n

Tactic:
exact Nat.find_le h

Premises used: Nat.find_le
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
mpr : LE.le (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) (upperCentralSeries G n)
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤

Tactic:
rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]

Premises used: eq_top_iff, Subgroup.upperCentralSeries_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ LE.le (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) (upperCentralSeries G n)

Tactic:
upperCentralSeries_mono _ h

Premises used: Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ LE.le (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) (upperCentralSeries G n)

Tactic:
exact upperCentralSeries_mono _ h

Premises used: Subgroup.upperCentralSeries_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → nilpotencyClass G ≤ n
mpr mpr₁ : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ ↔ nilpotencyClass G ≤ n

Tactic:
classical
  constructor
  · intro h
    rw [nilpotencyClass_def]
    exact Nat.find_le h
  · intro h
    rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]
    exact upperCentralSeries_mono _ h

Premises used: eq_top_iff, Group.nilpotencyClass_def, Subgroup.upperCentralSeries_nilpotencyClass
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw :
  Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯ = nilpotencyClass G

Tactic:
rw [nilpotencyClass_def]

Premises used: Group.nilpotencyClass_def
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯

Tactic:
le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Premises used: le_antisymm, Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
refine_1 :
  ∀ (n : ℕ),
    Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
refine_2 :
  ∀ (n : ℕ),
    (∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) → Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Premises used: le_antisymm, Nat.find_mono
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩

Premises used: Subgroup.upperCentralSeries_isAscendingCentralSeries, Subgroup.upperCentralSeries, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
refine_2 : H n ≤ upperCentralSeries G n
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤

Tactic:
rw [← top_le_iff, ← hn]

Premises used: top_le_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
ascending_central_series_le_upper H hH n

Premises used: Subgroup.ascending_central_series_le_upper
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
exact ascending_central_series_le_upper H hH n

Premises used: Subgroup.ascending_central_series_le_upper
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
rw :
  Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ = nilpotencyClass G

Tactic:
rw [← least_ascending_central_series_length_eq_nilpotencyClass]

Premises used: Subgroup.least_ascending_central_series_length_eq_nilpotencyClass