awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥
⊢ lcs k N = ⊥
have refine_1 : lowerCentralSeries R L (↥N) k ≤ N.incl.ker
Tactic: rw [← N.lowerCentralSeries_map_eq_lcs, ← LieModuleHom.le_ker_iff_map]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst_6 : LieModule R L M
h : lcs k N = ⊥
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥N) (lowerCentralSeries R L (↥N) k) ⊥
have refine_2 : N ⊓ lcs k N = ⊥
Tactic: rw [N.lowerCentralSeries_eq_lcs_comap, comap_incl_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
l : ℕ
h : l ≤ k + 1
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
have succ : ∀ (hk : l ≤ k), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
Tactic: rcases Nat.of_le_succ h with (hk | hk)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
l : ℕ
h : l ≤ k + 1
succ : ∀ (hk : l ≤ k), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
have succ₁ : ∀ (hk : l = k.succ), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
Tactic: rcases Nat.of_le_succ h with (hk | hk)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
have succ : LE.le (α := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
  (lowerCentralSeries R L M l)
Tactic: rw [lowerCentralSeries_succ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
l k : ℕ
⊢ l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
have zero : ∀ ⦃l : ℕ⦄, l ≤ 0 → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M 0) (lowerCentralSeries R L M l)
Tactic: induction k generalizing l with
  | zero => exact fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl
  | succ k ih =>
    intro h
    rcases Nat.of_le_succ h with (hk | hk)
    · rw [lowerCentralSeries_succ]
      exact (LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)
    · exact hk.symm ▸ le_rfl
Cleared hypotheses: l, k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
l k : ℕ
zero : ∀ ⦃l : ℕ⦄, l ≤ 0 → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M 0) (lowerCentralSeries R L M l)
⊢ l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
have succ : ∀ (k : ℕ)
  (ih : ∀ ⦃l : ℕ⦄, l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (lowerCentralSeries R L M l))
  ⦃l : ℕ⦄, l ≤ k + 1 → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)
Tactic: induction k generalizing l with
  | zero => exact fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl
  | succ k ih =>
    intro h
    rcases Nat.of_le_succ h with (hk | hk)
    · rw [lowerCentralSeries_succ]
      exact (LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)
    · exact hk.symm ▸ le_rfl
Cleared hypotheses: l, k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
⊢ ∀ᶠ (l : ℕ) in Filter.atTop,
    Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
have h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
Tactic: have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ :=
    LieSubmodule.wellFoundedLT_of_isArtinian R L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
⊢ ∀ᶠ (l : ℕ) in Filter.atTop,
    Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
have obtain : ∀ (n : ℕ)
  (hn : ∀ (m : ℕ), n ≤ m → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)),
  ∀ᶠ (l : ℕ) in Filter.atTop,
    Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
Tactic: obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
    h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
⊢ ∀ᶠ (l : ℕ) in Filter.atTop,
    Eq (α := LieSubmodule R L M) (⨅ (k : ℕ), lowerCentralSeries R L M k) (lowerCentralSeries R L M l)
have refine : ∀ (l : ℕ) (hl : l ≥ n) (m : ℕ),
  LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
Tactic: refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
l : ℕ
hl : l ≥ n
m : ℕ
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
have inl : ∀ (h : l ≤ m), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
Tactic: rcases le_or_gt l m with h | h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
l : ℕ
hl : l ≥ n
m : ℕ
inl : ∀ (h : l ≤ m), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
have inr : ∀ (h : m < l), LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
Tactic: rcases le_or_gt l m with h | h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
have inl : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
Tactic: rw [← hn _ hl, ← hn _ (hl.trans h)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : IsArtinian R M
h_wf : WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
inl : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M m)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)
have inl₁ : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M n)
Tactic: rw [← hn _ hl, ← hn _ (hl.trans h)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
⊢ IsTrivial L M ↔ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥
have mp : IsTrivial L M → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
mp : IsTrivial L M → Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥
⊢ IsTrivial L M ↔ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥
have mpr : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥ → IsTrivial L M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
h : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥
⊢ IsTrivial L M
have h₁ : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) m → m = 0
Tactic: rw [LieSubmodule.eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
h : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) m → m = 0
⊢ IsTrivial L M
have mpr : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
Tactic: apply IsTrivial.mk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
h : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) m → m = 0
x : L
m : M
⊢ ⁅x, m⁆ = 0
have mpr : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⁅x, m⁆
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
h : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) m → m = 0
x : L
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⁅x, m⁆
have mpr : Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅x, m⁆
Tactic: apply LieSubmodule.subset_lieSpan
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
h : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) m → m = 0
x : L
m : M
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅x, m⁆
have mpr : ∃ (a : L) (a_1 : M), ⁅a, a_1⁆ = ⁅x, m⁆
Tactic: simp only [Subtype.exists, LieSubmodule.mem_top, exists_prop, true_and, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
m : M
k : ℕ
ih :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m)
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k + 1]
      m)
have succ : Membership.mem (γ := LieSubmodule R L M) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
  ⁅x,
    (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m⁆
Tactic: simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
      toEnd_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
m : M
k : ℕ
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m)
have zero : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 0)
  ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
        (a : M) → M)^[0]
    m)
Tactic: induction k with
  | zero => simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]
  | succ k ih =>
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
      toEnd_apply_apply]
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
m : M
k : ℕ
zero :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 0)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[0]
      m)
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k]
      m)
have succ : ∀ (k : ℕ)
  (ih :
    Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k)
      ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
            (a : M) → M)^[k]
        m)),
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)^[k + 1]
      m)
Tactic: induction k with
  | zero => simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]
  | succ k ih =>
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
      toEnd_apply_apply]
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
m : M
k : ℕ
ih :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * (k + 1)))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k + 1]
      m)
have hk : 2 * k.succ = 2 * k + 1 + 1
Tactic: have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
m : M
k : ℕ
ih :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * (k + 1)))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k + 1]
      m)
have succ : Membership.mem (γ := LieSubmodule R L M)
  (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M (2 * k))))
  ⁅x,
    ⁅y,
      (Function.comp (β := M)
            (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
              (a : M) → M)
            (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
              (a : M) → M))^[k]
        m⁆⁆
Tactic: simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
      toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
m : M
k : ℕ
ih :
  Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ Membership.mem (γ := LieSubmodule R L M)
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤
      (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M (2 * k))))
    ⁅x,
      ⁅y,
        (Function.comp (β := M)
              (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                    Module.End R M) :
                (a : M) → M)
              (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                    Module.End R M) :
                (a : M) → M))^[k]
          m⁆⁆
have succ : Membership.mem (γ := LieSubmodule R L M)
  (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M (2 * k)))
  ⁅y,
    (Function.comp (β := M)
          (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
            (a : M) → M)
          (⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
            (a : M) → M))^[k]
      m⁆
Tactic: refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
m : M
k : ℕ
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (2 * k))
    ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
              ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
          (a : M) → M)^[k]
      m)
have zero : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M (HMul.hMul (α := ℕ) 2 0))
  ((⇑(((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x ∘ₗ
            ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
        (a : M) → M)^[0]
    m)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
      toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]
    refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih
Cleared hypotheses: k