awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥

Tactic:
hL.nilpotent_int

Premises used: LieModule.IsNilpotent.nilpotent_int
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
obtain : ∀ (k : ℕ) (h : Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥), IsSolvable L
⊢ IsSolvable L

Tactic:
obtain ⟨k, h⟩ : ∃ k, LieModule.lowerCentralSeries ℤ L L k = ⊥ := hL.nilpotent_int

Premises used: LieModule.IsNilpotent.nilpotent_int
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥
h₁ : Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥
⊢ IsSolvable L

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : Eq (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥
h₁ :
  ∀ (h : LE.le (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥),
    LE.le (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥
⊢ Eq (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥

Tactic:
rw [← le_bot_iff] at h ⊢

Premises used: le_bot_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : LE.le (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥
⊢ LE.le (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥

Tactic:
le_trans (LieModule.derivedSeries_le_lowerCentralSeries ℤ L k) h

Premises used: LieModule.derivedSeries_le_lowerCentralSeries, Int, le_trans
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
L : Type v
inst : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : LE.le (α := LieSubmodule ℤ L L) (LieModule.lowerCentralSeries ℤ L L k) ⊥
⊢ LE.le (α := LieIdeal ℤ L) (derivedSeries ℤ L k) ⊥

Tactic:
exact le_trans (LieModule.derivedSeries_le_lowerCentralSeries ℤ L k) h

Premises used: LieModule.derivedSeries_le_lowerCentralSeries, Int, le_trans
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing.IsNilpotent L
⊢ ∃ (k : ℕ), ∀ (x : L), HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) k = 0

Tactic:
LieModule.exists_forall_pow_toEnd_eq_zero R L L

Premises used: LieModule.exists_forall_pow_toEnd_eq_zero
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) 0) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) 0) : Submodule R (L ⧸ I))

Tactic:
simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule]

Premises used: LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
succ :
  Eq.{v + 1} (α := Submodule R (L ⧸ I))
    (Submodule.span R
      {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x})
    (Submodule.span R
      {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x})
⊢ Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
succ :
  Eq.{v + 1} (α := L ⧸ I → Prop)
    (fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x)
    fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
⊢ Eq.{v + 1} (α := Submodule R (L ⧸ I))
    (Submodule.span R
      {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x})
    (Submodule.span R
      {x : L ⧸ I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x})

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
succ :
  ∀ (x : L ⧸ I),
    (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) ↔
      ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
⊢ Eq.{v + 1} (α := L ⧸ I → Prop)
    (fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x)
    fun (x : L ⧸ I) ↦ ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
x : L ⧸ I
succ :
  (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) →
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x
succ₁ :
  (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x) →
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x
⊢ (∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x_1 : L), (↑n : L ⧸ I)⁆ = x) ↔
    ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x_1 : L ⧸ I), (↑n : L ⧸ I)⁆ = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) z
⊢ Membership.mem (γ := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) z

Tactic:
rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz

Premises used: LieSubmodule.mem_toSubmodule
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) z
⊢ ∃ (x : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x : L ⧸ I), (↑n : L ⧸ I)⁆ = ⁅y, z⁆

Tactic:
⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩

Premises used: LieSubmodule.Quotient.mk, Subtype.mk, Exists.intro, LieSubmodule.mem_top, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) z
⊢ ∃ (x : ↥⊤) (n : ↥(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)), ⁅(↑x : L ⧸ I), (↑n : L ⧸ I)⁆ = ⁅y, z⁆

Tactic:
exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
val : L ⧸ I
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) z
⊢ Membership.mem (γ := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) z

Tactic:
rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz

Premises used: LieSubmodule.mem_toSubmodule
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
val : L ⧸ I
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) z
⊢ ∃ (x : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x : L), (↑n : L ⧸ I)⁆ = ⁅y, z⁆

Tactic:
⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, LieSubmodule.mem_top, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))
val : L ⧸ I
y : L
z : L ⧸ I
hz : Membership.mem (γ := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) z
⊢ ∃ (x : ↥⊤) (n : ↥(lowerCentralSeries R L (L ⧸ I) k)), ⁅(↑x : L), (↑n : L ⧸ I)⁆ = ⁅y, z⁆

Tactic:
exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
zero :
  Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) 0) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) 0) : Submodule R (L ⧸ I))
succ :
  ∀ (k : ℕ)
    (ih :
      Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
        (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))),
    Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
      (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) (k + 1)) : Submodule R (L ⧸ I))
⊢ Eq (α := Submodule R (L ⧸ I)) (↑(lowerCentralSeries R L (L ⧸ I) k) : Submodule R (L ⧸ I))
    (↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) : Submodule R (L ⧸ I))

Tactic:
induction k with
  | zero =>
    simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    congr
    ext x
    constructor
    · rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
    · rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
      rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz
      exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩

Premises used: LieModule.lowerCentralSeries_zero, LieSubmodule.mem_toSubmodule, LieModule.lowerCentralSeries_succ, LieSubmodule.top_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) 0) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) 0) : Submodule R ↥I)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)
succ :
  LE.le.{v} (α := Submodule R ↥I)
    (Submodule.span R {x : ↥I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R (↥I) (↥I) k)), ⁅(↑x_1 : ↥I), (↑n : ↥I)⁆ = x})
    (Submodule.span R {x : ↥I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (↥I) k)), ⁅(↑x_1 : L), (↑n : ↥I)⁆ = x})
⊢ LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) (k + 1)) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) (k + 1)) : Submodule R ↥I)

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)
y z : ↥I
hz : Membership.mem (γ := LieSubmodule R ↥I ↥I) (lowerCentralSeries R (↥I) (↥I) k) z
⊢ Membership.mem (γ := Set ↥I)
    {x : ↥I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (↥I) k)), ⁅(↑x_1 : L), (↑n : ↥I)⁆ = x} ⁅y, z⁆

Tactic:
⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, LieSubmodule.mem_top, Subtype.val, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih :
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)
y z : ↥I
hz : Membership.mem (γ := LieSubmodule R ↥I ↥I) (lowerCentralSeries R (↥I) (↥I) k) z
⊢ Membership.mem (γ := Set ↥I)
    {x : ↥I | ∃ (x_1 : ↥⊤) (n : ↥(lowerCentralSeries R L (↥I) k)), ⁅(↑x_1 : L), (↑n : ↥I)⁆ = x} ⁅y, z⁆

Tactic:
exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
zero :
  LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) 0) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) 0) : Submodule R ↥I)
succ :
  ∀ (k : ℕ)
    (ih :
      LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
        (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)),
    LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) (k + 1)) : Submodule R ↥I)
      (↑(lowerCentralSeries R L (↥I) (k + 1)) : Submodule R ↥I)
⊢ LE.le (α := Submodule R ↥I) (↑(lowerCentralSeries R (↥I) (↥I) k) : Submodule R ↥I)
    (↑(lowerCentralSeries R L (↥I) k) : Submodule R ↥I)

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    apply Submodule.span_mono
    rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
    exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩

Premises used: LieModule.lowerCentralSeries_succ, Submodule.span_mono, LieSubmodule.lieIdeal_oper_eq_linear_span, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent.{v} (L ⧸ I)
this : LieModule.IsNilpotent L (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
LieModule.nilpotentOfNilpotentQuotient R L L h₁ this

Premises used: LieModule.nilpotentOfNilpotentQuotient
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent.{v} (L ⧸ I)
this : LieModule.IsNilpotent L (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this

Premises used: LieModule.nilpotentOfNilpotentQuotient
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent.{v} (L ⧸ I)
suffices : LieModule.IsNilpotent L (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
suffices LieModule.IsNilpotent L (L ⧸ I) by
    exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent.{v} (L ⧸ I)
simp :
  ∀ (h₂ : ∃ (k : ℕ), Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥),
    ∃ (k : ℕ), Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥
⊢ LieModule.IsNilpotent L (L ⧸ I)

Tactic:
simp only [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₂ ⊢

Premises used: LieRing.IsNilpotent, LieModule.isNilpotent_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ (k : ℕ), Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥
h :
  ∀ (k : ℕ) (hk : Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥),
    Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥

Tactic:
peel h₂ with k hk
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ (k : ℕ), Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥
k : ℕ
hk : Eq.{v + 1} (α := LieSubmodule R (L ⧸ I) (L ⧸ I)) (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k) ⊥
⊢ Eq (α := LieSubmodule R L (L ⧸ I)) (lowerCentralSeries R L (L ⧸ I) k) ⊥

Tactic:
simp [← LieSubmodule.toSubmodule_inj, coe_lowerCentralSeries_ideal_quot_eq, hk]

Premises used: LieSubmodule.toSubmodule_inj, coe_lowerCentralSeries_ideal_quot_eq
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Nontrivial L
inst_4 : LieRing.IsNilpotent L
⊢ Nontrivial.{v} ↥(center R L)

Tactic:
LieModule.nontrivial_max_triv_of_isNilpotent R L L

Premises used: Set.Mem, LieModule.nontrivial_max_triv_of_isNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L 0) ≤ lowerCentralSeries R L' L' 0

Tactic:
simp only [LieModule.lowerCentralSeries_zero, le_top]

Premises used: LieModule.lowerCentralSeries_zero, le_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
succ :
  map f (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k)) ≤
    Bracket.bracket (L := LieIdeal R L') ⊤ (lowerCentralSeries R L' L' k)
⊢ map f (lowerCentralSeries R L L (k + 1)) ≤ lowerCentralSeries R L' L' (k + 1)

Tactic:
simp only [LieModule.lowerCentralSeries_succ]

Premises used: LieModule.lowerCentralSeries_succ
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k)) ≤
    Bracket.bracket (L := LieIdeal R L') ⊤ (lowerCentralSeries R L' L' k)

Tactic:
le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

Premises used: LieIdeal.map_bracket_le, LieSubmodule.mono_lie, le_top, le_trans
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f (Bracket.bracket (L := LieIdeal R L) ⊤ (lowerCentralSeries R L L k)) ≤
    Bracket.bracket (L := LieIdeal R L') ⊤ (lowerCentralSeries R L' L' k)

Tactic:
exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

Premises used: LieIdeal.map_bracket_le, LieSubmodule.mono_lie, le_top, le_trans
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
zero : map f (lowerCentralSeries R L L 0) ≤ lowerCentralSeries R L' L' 0
succ :
  ∀ (k : ℕ) (ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k),
    map f (lowerCentralSeries R L L (k + 1)) ≤ lowerCentralSeries R L' L' (k + 1)
⊢ map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Tactic:
induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ]
    exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

Premises used: LieModule.lowerCentralSeries_zero, LieModule.lowerCentralSeries_succ, le_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw : f.idealRange = ⊤
⊢ map f ⊤ = ⊤

Tactic:
rw [← f.idealRange_eq_map]

Premises used: LieHom.idealRange_eq_map
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ f.idealRange = ⊤

Tactic:
f.idealRange_eq_top_of_surjective h

Premises used: LieHom.idealRange_eq_top_of_surjective
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ f.idealRange = ⊤

Tactic:
exact f.idealRange_eq_top_of_surjective h

Premises used: LieHom.idealRange_eq_top_of_surjective
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ map f ⊤ = ⊤

Tactic:
have h' : (⊤ : LieIdeal R L).map f = ⊤ := by
    rw [← f.idealRange_eq_map]
    exact f.idealRange_eq_top_of_surjective h
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h' : map f ⊤ = ⊤
⊢ map f ⊤ = ⊤

Tactic:
h'