awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
⊢ IsDescendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)
have refine : ∀ (x : G) (m : ℕ) (hx : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) m) x) (g : G),
  Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
Tactic: refine ⟨hn, fun x m hx g => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
have pos : ∀ (hm : n ≤ m), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
Tactic: by_cases! hm : n ≤ m
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
pos : ∀ (hm : n ≤ m), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
have neg : ∀ (hm : m < n), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
Tactic: by_cases! hm : n ≤ m
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : n ≤ m
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
have pos : ∀ (hx : x = 1) (g : G) (hm : n ≤ m), Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
Tactic: rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx
Cleared hypotheses: hx, g, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x = 1
g : G
hm : n ≤ m
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
have pos : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) (Bracket.bracket (L := G) 1 g)
Tactic: subst hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) (Bracket.bracket (L := G) 1 g)
have pos : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) 1
Tactic: rw [commutatorElement_one_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) ⁅x, g⁆
have neg : x ∈ H (n - (m + 1) + 1)
Tactic: apply hH
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ x ∈ H (n - (m + 1) + 1)
have h : H (n - (m + 1) + 1) = H (n - m)
Tactic: convert! hx using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ H (n - (m + 1) + 1) = H (n - m)
have h : H (n + 1 - m.succ) = H (n - m)
Tactic: rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
h : H (n + 1 - m.succ) = H (n - m)
h₁ : H (n + 1 - (m + 1)) = H (n - m)
⊢ H (n - (m + 1) + 1) = H (n - m)
have h₂ : H (n - m) = H (n - m)
Tactic: rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
⊢ IsAscendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)
have h0 : H 0 = ⊤
Tactic: obtain ⟨h0, hH⟩ := hdesc
Cleared hypotheses: hdesc
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
h0 : H 0 = ⊤
⊢ IsAscendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)
have hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
Tactic: obtain ⟨h0, hH⟩ := hdesc
Cleared hypotheses: hdesc
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ IsAscendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)
have refine : ∀ (x : G) (m : ℕ) (hx : Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) (m + 1)) x) (g : G),
  Membership.mem (γ := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) m) ⁅x, g⁆
Tactic: refine ⟨hn, fun x m hx g => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ ⁅x, g⁆ ∈ H (n - m)
have pos : ∀ (hm : n ≤ m), ⁅x, g⁆ ∈ H (n - m)
Tactic: by_cases! hm : n ≤ m
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
pos : ∀ (hm : n ≤ m), ⁅x, g⁆ ∈ H (n - m)
⊢ ⁅x, g⁆ ∈ H (n - m)
have neg : ∀ (hm : m < n), ⁅x, g⁆ ∈ H (n - m)
Tactic: by_cases! hm : n ≤ m
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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 : n ≤ m
⊢ ⁅x, g⁆ ∈ H (n - m)
have hnm : n - m = 0
Tactic: have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 : n ≤ m
hnm : n - m = 0
⊢ ⁅x, g⁆ ∈ H (n - m)
have pos : Membership.mem (γ := Subgroup G) ⊤ ⁅x, g⁆
Tactic: rw [hnm, h0]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ ⁅x, g⁆ ∈ H (n - m)
have h : H (n - m) = H (n - (m + 1) + 1)
Tactic: convert! hH x _ hx g using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 (n - m) = H (n - (m + 1) + 1)
have h : H (n - m) = H (n + 1 - m.succ)
Tactic: rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 (n - m) = H (n - (m + 1) + 1)
have h₂ : H (n - m) = H (n - m)
Tactic: rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
have rw : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ↔
  ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
Tactic: rw [nilpotent_iff_finite_ascending_central_series]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ↔
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
have mp : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) →
  ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊥
⊢ (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ↔
    ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
have mpr : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
  ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊥
have mp : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊥
Tactic: refine ⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥
have mp : H 0 = ⊥
Tactic: rw [tsub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊤
have mpr : Eq.{u_1 + 1} (α := Subgroup G) ((fun (m : ℕ) ↦ H (n - m)) n) ⊤
Tactic: refine ⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤
have mpr : H 0 = ⊤
Tactic: rw [tsub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
n : ℕ
⊢ Characteristic (lowerCentralSeries G n)
have zero : Characteristic (lowerCentralSeries G 0)
Tactic: induction n with
  | zero => simp [topCharacteristic]
  | succ d hd => unfold lowerCentralSeries; infer_instance
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
n : ℕ
zero : Characteristic (lowerCentralSeries G 0)
⊢ Characteristic (lowerCentralSeries G n)
have succ : ∀ (d : ℕ) (hd : Characteristic (lowerCentralSeries G d)), Characteristic (lowerCentralSeries G (d + 1))
Tactic: induction n with
  | zero => simp [topCharacteristic]
  | succ d hd => unfold lowerCentralSeries; infer_instance
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Antitone (β := Subgroup G) (lowerCentralSeries G)
have refine : ∀ (n : ℕ) (x : G) (hx : Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) x),
  Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x
Tactic: refine antitone_nat_of_succ_le fun n x hx => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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) (lowerCentralSeries G n) x
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
have 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
Tactic: refine
    closure_induction ?_ (Subgroup.one_mem _) (fun _ _ _ _ ↦ mul_mem) (fun _ _ ↦ inv_mem) hx
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) y
have rw : Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) (z * (a * z⁻¹ * a⁻¹))
Tactic: rw [← ha, commutatorElement_def, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ IsDescendingCentralSeries (lowerCentralSeries G)
have left : Eq (α := Subgroup G) (lowerCentralSeries G 0) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
left : Eq (α := Subgroup G) (lowerCentralSeries G 0) ⊤
⊢ IsDescendingCentralSeries (lowerCentralSeries G)
have right : ∀ (x : G) (n : ℕ),
  Membership.mem (γ := Subgroup G) (lowerCentralSeries G n) x →
    ∀ (g : G), Membership.mem (γ := Subgroup G) (lowerCentralSeries G (n + 1)) ⁅x, g⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have rw : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ↔
  ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: rw [nilpotent_iff_finite_descending_central_series]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ↔
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have mp : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
  ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
mp :
  (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) →
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ (∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ↔
    ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have mpr : (∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥) →
  ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have h : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
Tactic: use n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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)
⊢ Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
have h : lowerCentralSeries G n ≤ H n
Tactic: rw [eq_bot_iff, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤
have rw : Eq (α := Subgroup G)
  (upperCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry)) ⊤
Tactic: rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊤) ⋯)) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤
have rw₁ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
Tactic: rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤
have rw : Eq (α := Subgroup G)
  (upperCentralSeries G (Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry)) ⊤
Tactic: classical
  rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊤) ⋯)) ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) ⊤
have rw₁ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
Tactic: classical
  rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ ↔ nilpotencyClass G ≤ n
have mp : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → nilpotencyClass G ≤ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → nilpotencyClass G ≤ n
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ ↔ nilpotencyClass G ≤ n
have mpr : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
⊢ nilpotencyClass G ≤ n
have mp : Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry ≤ n
Tactic: rw [nilpotencyClass_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
have mpr : LE.le (α := Subgroup G) (upperCentralSeries G (nilpotencyClass G)) (upperCentralSeries G n)
Tactic: rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ ↔ nilpotencyClass G ≤ n
have mp : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
mp : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → nilpotencyClass G ≤ n
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ ↔ nilpotencyClass G ≤ n
have mpr : nilpotencyClass G ≤ n → Eq (α := Subgroup G) (upperCentralSeries 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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯ = nilpotencyClass G
have rw : Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) sorry =
  Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) sorry
Tactic: rw [nilpotencyClass_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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) ⊤) ⋯
have refine_1 : ∀ (n : ℕ),
  Eq (α := Subgroup G) (upperCentralSeries G n) ⊤ → ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
Tactic: refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 = ⊤
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ⋯
have refine_2 : ∀ (n : ℕ),
  (∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) → Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
Tactic: refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
have refine_2 : H n ≤ upperCentralSeries G n
Tactic: rw [← top_le_iff, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ = nilpotencyClass G
have rw : Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) sorry =
  Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) sorry
Tactic: rw [← least_ascending_central_series_length_eq_nilpotencyClass]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
hG : Group.IsNilpotent G
⊢ Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) ⋯
have refine_1 : ∀ (n : ℕ),
  (∃ (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) →
    ∃ (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥
Tactic: refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)