awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Nilpotent
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) (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))
    (lowerCentralSeries R L M l)

Tactic:
exact (LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)

Premises used: LieSubmodule.mono_lie_right, LieSubmodule.lie_le_right, LE.le.trans, Top.top
-- Module: Mathlib.Algebra.Lie.Nilpotent
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.succ
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)

Tactic:
hk.symm ▸ le_rfl

Premises used: le_rfl, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Lie.Nilpotent
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.succ
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1)) (lowerCentralSeries R L M l)

Tactic:
exact hk.symm ▸ le_rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
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)
⊢ l ≤ k → LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M k) (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

Premises used: LieModule.lowerCentralSeries_succ
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
⊢ WellFoundedGT.{w} (LieSubmodule R L M)ᵒᵈ

Tactic:
have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ :=
    LieSubmodule.wellFoundedLT_of_isArtinian R L M
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)ᵒᵈ
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)
⊢ ∀ᶠ (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⟩

Premises used: WellFoundedGT.monotone_chain_condition, LieModule.antitone_lowerCentralSeries, OrderHom.mk
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)

Tactic:
Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

Premises used: Iff.mpr, le_iInf, le_antisymm, LieModule.lowerCentralSeries, Exists.intro, Filter.eventually_atTop, iInf_le
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
refine :
  ∀ (l : ℕ) (hl : l ≥ n) (m : ℕ),
    LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (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:
refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

Premises used: Iff.mpr, le_iInf, le_antisymm, Exists.intro, Filter.eventually_atTop, iInf_le
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
inr : ∀ (h : m < l), 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)

Tactic:
rcases le_or_gt l m with h | h

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
inl₁ inl₂ : LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M n) (lowerCentralSeries R L M n)
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)

Tactic:
rw [← hn _ hl, ← hn _ (hl.trans h)]

Premises used: LE.le.trans
-- Module: Mathlib.Algebra.Lie.Nilpotent
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 : m < l
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)

Tactic:
antitone_lowerCentralSeries R L M (le_of_lt h)

Premises used: le_of_lt, LieModule.antitone_lowerCentralSeries
-- Module: Mathlib.Algebra.Lie.Nilpotent
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 : m < l
⊢ LE.le (α := LieSubmodule R L M) (lowerCentralSeries R L M l) (lowerCentralSeries R L M m)

Tactic:
exact antitone_lowerCentralSeries R L M (le_of_lt h)

Premises used: le_of_lt, LieModule.antitone_lowerCentralSeries
-- Module: Mathlib.Algebra.Lie.Nilpotent
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) ⊥
mpr : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥ → IsTrivial L M
⊢ IsTrivial L M ↔ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Nilpotent
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 : IsTrivial L M
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
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) ⊥
⊢ ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) m → m = 0

Tactic:
rw [LieSubmodule.eq_bot_iff] at h

Premises used: LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
mpr : ∀ (x : L) (m : M), ⁅x, m⁆ = 0
⊢ IsTrivial L M

Tactic:
apply IsTrivial.mk

Premises used: LieModule.IsTrivial.mk
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
mpr : Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⁅x, m⁆
⊢ ⁅x, m⁆ = 0

Tactic:
apply h
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
mpr : Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅x, m⁆
⊢ Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M 1) ⁅x, m⁆

Tactic:
apply LieSubmodule.subset_lieSpan

Premises used: LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
mpr : ∃ (a : L) (a_1 : M), ⁅a, a_1⁆ = ⁅x, m⁆
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅x, m⁆

Tactic:
simp only [Subtype.exists, LieSubmodule.mem_top, exists_prop, true_and, Set.mem_setOf]

Premises used: Subtype.exists, exists_prop, Set.mem_setOf, LieSubmodule.mem_top, true_and
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
⊢ ∃ (a : L) (a_1 : M), ⁅a, a_1⁆ = ⁅x, m⁆

Tactic:
⟨x, m, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
⊢ ∃ (a : L) (a_1 : M), ⁅a, a_1⁆ = ⁅x, m⁆

Tactic:
exact ⟨x, m, rfl⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
⊢ 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:
simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]

Premises used: LieModule.lowerCentralSeries_zero, Function.iterate_zero, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
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⁆
⊢ 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:
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
      toEnd_apply_apply]

Premises used: Function.iterate_succ', LieModule.lowerCentralSeries_succ, LieModule.toEnd_apply_apply, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.Nilpotent
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) (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:
LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
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) (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:
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
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)
⊢ 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)

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

Premises used: LieModule.lowerCentralSeries_zero, Function.iterate_zero, Function.iterate_succ', LieModule.lowerCentralSeries_succ, LieModule.toEnd_apply_apply, LieSubmodule.mem_top, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
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)
⊢ 2 * k.succ = 2 * k + 1 + 1

Tactic:
have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
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⁆⁆
⊢ 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)

Tactic:
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
      toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]

Premises used: Function.iterate_succ', LieModule.lowerCentralSeries_succ, LieModule.toEnd_apply_apply, LinearMap.coe_comp, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.Nilpotent
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⁆⁆

Tactic:
LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
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
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⁆
⊢ 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:
refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.mem_top