awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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 ⊤ = ⊤
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)

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']

Premises used: LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq
-- 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')
h' : map f ⊤ = ⊤
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]; exact h'
  | succ k ih => simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']

Premises used: LieModule.lowerCentralSeries_zero, LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq
-- 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'
h₁ : LieRing.IsNilpotent L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw :
  ∀ (h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥) {f : L →ₗ⁅R⁆ L'}
    (h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')),
    ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
⊢ LieRing.IsNilpotent L

Tactic:
rw [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
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h :
  ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥),
    Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥

Tactic:
peel h₁ with k hk
-- 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'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
h : LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
⊢ Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥

Tactic:
apply LieIdeal.bot_of_map_eq_bot h₂

Premises used: LieIdeal.bot_of_map_eq_bot
-- 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'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
h : LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥

Tactic:
rw [eq_bot_iff, ← hk]

Premises used: eq_bot_iff
-- 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'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Tactic:
apply LieIdeal.map_lowerCentralSeries_le

Premises used: LieIdeal.map_lowerCentralSeries_le
-- 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'
h₁ : LieRing.IsNilpotent L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw :
  ∀ (h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥) {f : L →ₗ⁅R⁆ L'}
    (h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')),
    ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
⊢ LieRing.IsNilpotent L'

Tactic:
rw [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
L' : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h :
  ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥),
    Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥

Tactic:
peel h₁ with k hk
-- 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'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
h : LieIdeal.map f ⊥ = ⊥
⊢ Eq (α := LieSubmodule R L' L') (lowerCentralSeries R L' L' k) ⊥

Tactic:
rw [← LieIdeal.lowerCentralSeries_map_eq k h₂, hk]

Premises used: LieIdeal.lowerCentralSeries_map_eq
-- 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'
h₁ : ∃ (k : ℕ), Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective.{v + 1, w + 1} (α := L) (β := L') (⇑f : (a : L) → L')
k : ℕ
hk : Eq (α := LieSubmodule R L L) (lowerCentralSeries R L L k) ⊥
⊢ LieIdeal.map f ⊥ = ⊥

Tactic:
simp only [LieIdeal.map_eq_bot_iff, bot_le]

Premises used: bot_le, LieIdeal.map_eq_bot_iff
-- 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'
e : L ≃ₗ⁅R⁆ L'
mp : LieRing.IsNilpotent L → LieRing.IsNilpotent L'
mpr : LieRing.IsNilpotent L' → LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent L ↔ LieRing.IsNilpotent L'

Tactic:
constructor
-- 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'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent L'

Tactic:
e.symm.injective.lieAlgebra_isNilpotent

Premises used: Function.Injective.lieAlgebra_isNilpotent, LieEquiv.injective, LieEquiv.symm
-- 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'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent L'

Tactic:
exact e.symm.injective.lieAlgebra_isNilpotent

Premises used: Function.Injective.lieAlgebra_isNilpotent, LieEquiv.injective, LieEquiv.symm
-- 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'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L'
⊢ LieRing.IsNilpotent L

Tactic:
e.injective.lieAlgebra_isNilpotent

Premises used: Function.Injective.lieAlgebra_isNilpotent, LieEquiv.injective
-- 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'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L'
⊢ LieRing.IsNilpotent L

Tactic:
exact e.injective.lieAlgebra_isNilpotent

Premises used: Function.Injective.lieAlgebra_isNilpotent, LieEquiv.injective
-- 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'
inst_5 : LieRing.IsNilpotent L
f : L →ₗ⁅R⁆ L'
⊢ LieRing.IsNilpotent.{w} ↥f.range

Tactic:
f.surjective_rangeRestrict.lieAlgebra_isNilpotent

Premises used: LieHom.surjective_rangeRestrict, Function.Surjective.lieAlgebra_isNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L)) ↔ LieRing.IsNilpotent L

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
refine_1 : ∀ (h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))), LieRing.IsNilpotent L
refine_2 : LieRing.IsNilpotent L → LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
⊢ LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L)) ↔ LieRing.IsNilpotent L

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
⊢ Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (center R L)

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
h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
⊢ Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (center R L)

Tactic:
have : (ad R L).ker = center R L := by 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
h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
this : Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (center R L)
⊢ LieRing.IsNilpotent L

Tactic:
LieAlgebra.nilpotent_of_nilpotent_quotient (le_of_eq this)
        ((ad R L).quotKerEquivRange.nilpotent_iff_equiv_nilpotent.mpr h)

Premises used: Iff.mpr, LieAlgebra.ad, LieEquiv.nilpotent_iff_equiv_nilpotent, LieAlgebra.nilpotent_of_nilpotent_quotient, LieHom.quotKerEquivRange, le_of_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
h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
this : Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (center R L)
⊢ LieRing.IsNilpotent L

Tactic:
exact
      LieAlgebra.nilpotent_of_nilpotent_quotient (le_of_eq this)
        ((ad R L).quotKerEquivRange.nilpotent_iff_equiv_nilpotent.mpr h)

Premises used: Iff.mpr, LieAlgebra.ad, LieEquiv.nilpotent_iff_equiv_nilpotent, LieAlgebra.nilpotent_of_nilpotent_quotient, LieHom.quotKerEquivRange, le_of_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
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))

Tactic:
(ad R L).isNilpotent_range

Premises used: LieAlgebra.ad, LieHom.isNilpotent_range
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))

Tactic:
exact (ad R L).isNilpotent_range

Premises used: LieAlgebra.ad, LieHom.isNilpotent_range
-- 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'
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent.{v} ↥⊤

Tactic:
LieSubalgebra.topEquiv.nilpotent_iff_equiv_nilpotent.mpr h

Premises used: Iff.mpr, LieSubalgebra.topEquiv, LieEquiv.nilpotent_iff_equiv_nilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
⊢ Eq (α := LieSubmodule R L M) (I.lcs M 0) ⊤

Tactic:
rfl

Premises used: Nat.iterate, rfl, LieIdeal.lcs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
⊢ Eq (α := LieSubmodule R L M) (I.lcs M (k + 1)) ⁅I, I.lcs M k⁆

Tactic:
Function.iterate_succ_apply' (fun N => ⁅I, N⁆) k ⊤

Premises used: Function.iterate_succ_apply', Set.Mem, Bracket.bracket, setOf, Top.top, LieIdeal.lcs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
⊢ Eq (α := LieSubmodule R L M) (lcs ⊤ M k) (lowerCentralSeries R L M k)

Tactic:
rfl

Premises used: LieSubmodule.lcs, LieModule.lowerCentralSeries, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule R L M
⊢ Eq (α := Submodule R M) (↑(I.lcs M 0) : Submodule R M) (↑(lowerCentralSeries R (↥I) M 0) : Submodule R M)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k_1 : ℕ
inst_6 : LieModule R L M
k : ℕ
ih : Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)
succ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R
      {x : M |
        ∃ x_1 ∈ I,
          ∃ (n : M),
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥I) M) (lowerCentralSeries R (↥I) M k) n ∧
              ⁅x_1, n⁆ = x})
    (Submodule.span R
      {x : M |
        ∃ (x_1 : ↥I) (n : M),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥I) M) (lowerCentralSeries R (↥I) M k) n ∧
            ⁅(↑x_1 : L), n⁆ = x})
⊢ Eq (α := Submodule R M) (↑(I.lcs M (k + 1)) : Submodule R M) (↑(lowerCentralSeries R (↥I) M (k + 1)) : Submodule R M)

Tactic:
simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieSubalgebra.coe_bracket_of_module, LieModule.lowerCentralSeries_succ, LieIdeal.lcs_succ, LieIdeal.toLieSubalgebra, LieSubmodule.mem_top, true_and, LieIdeal.lcs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k_1 : ℕ
inst_6 : LieModule R L M
k : ℕ
ih : Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (Submodule.span R
      {x : M |
        ∃ x_1 ∈ I,
          ∃ (n : M),
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥I) M) (lowerCentralSeries R (↥I) M k) n ∧
              ⁅x_1, n⁆ = x})
    (Submodule.span R
      {x : M |
        ∃ (x_1 : ↥I) (n : M),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥I) M) (lowerCentralSeries R (↥I) M k) n ∧
            ⁅(↑x_1 : L), n⁆ = x})

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule R L M
zero : Eq (α := Submodule R M) (↑(I.lcs M 0) : Submodule R M) (↑(lowerCentralSeries R (↥I) M 0) : Submodule R M)
succ :
  ∀ (k : ℕ)
    (ih : Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)),
    Eq (α := Submodule R M) (↑(I.lcs M (k + 1)) : Submodule R M)
      (↑(lowerCentralSeries R (↥I) M (k + 1)) : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
    simp

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieSubalgebra.coe_bracket_of_module, LieModule.lowerCentralSeries_succ, LieIdeal.lcs_succ, LieIdeal.toLieSubalgebra, LieSubmodule.mem_top, true_and, LieIdeal.lcs
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule.IsNilpotent L ↥I
f : ↥I →ₗ⁅R⁆ L := I.incl
g : ↥I →ₗ⁅R⁆ ↥I := LieHom.id
⊢ ∀ (x m : ↥I),
    Eq (α := ↥I) (Bracket.bracket (L := L) ((f : (a : ↥I) → L) x : L) ((g : (a : ↥I) → ↥I) m) : ↥I)
      ((g : (a : ↥I) → ↥I) ⁅x, m⁆ : ↥I)

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule.IsNilpotent L ↥I
f : ↥I →ₗ⁅R⁆ L := I.incl
g : ↥I →ₗ⁅R⁆ ↥I := LieHom.id
⊢ ∀ (x m : ↥I),
    Eq (α := ↥I) (Bracket.bracket (L := L) ((f : (a : ↥I) → L) x : L) ((g : (a : ↥I) → ↥I) m) : ↥I)
      ((g : (a : ↥I) → ↥I) ⁅x, m⁆ : ↥I)

Tactic:
have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule.IsNilpotent L ↥I
f : ↥I →ₗ⁅R⁆ L := I.incl
g : ↥I →ₗ⁅R⁆ ↥I := LieHom.id
hfg :
  ∀ (x m : ↥I),
    Eq (α := ↥I) (Bracket.bracket (L := L) ((f : (a : ↥I) → L) x : L) ((g : (a : ↥I) → ↥I) m) : ↥I)
      ((g : (a : ↥I) → ↥I) ⁅x, m⁆ : ↥I)
⊢ LieRing.IsNilpotent.{u_2} ↥I

Tactic:
Function.injective_id.lieModuleIsNilpotent hfg

Premises used: Function.injective_id, Function.Injective.lieModuleIsNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule.IsNilpotent L ↥I
f : ↥I →ₗ⁅R⁆ L := I.incl
g : ↥I →ₗ⁅R⁆ ↥I := LieHom.id
hfg :
  ∀ (x m : ↥I),
    Eq (α := ↥I) (Bracket.bracket (L := L) ((f : (a : ↥I) → L) x : L) ((g : (a : ↥I) → ↥I) m) : ↥I)
      ((g : (a : ↥I) → ↥I) ⁅x, m⁆ : ↥I)
⊢ LieRing.IsNilpotent.{u_2} ↥I

Tactic:
exact Function.injective_id.lieModuleIsNilpotent hfg

Premises used: Function.injective_id, Function.Injective.lieModuleIsNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) 0)
    (baseChange A (lowerCentralSeries R L M 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
k : ℕ
ih :
  Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k)
    (baseChange A (lowerCentralSeries R L M k))
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) (k + 1))
    (baseChange A (lowerCentralSeries R L M (k + 1)))

Tactic:
simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.lie_baseChange, LieSubmodule.baseChange_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
k : ℕ
zero :
  Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) 0)
    (baseChange A (lowerCentralSeries R L M 0))
succ :
  ∀ (k : ℕ)
    (ih :
      Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k)
        (baseChange A (lowerCentralSeries R L M k))),
    Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) (k + 1))
      (baseChange A (lowerCentralSeries R L M (k + 1)))
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k)
    (baseChange A (lowerCentralSeries R L M k))

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

Premises used: LieModule.lowerCentralSeries_succ, LieSubmodule.lie_baseChange, LieSubmodule.baseChange_top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : IsNilpotent L M
obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥), IsNilpotent (A ⊗[R] L) (A ⊗[R] M)
⊢ IsNilpotent (A ⊗[R] L) (A ⊗[R] M)

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M

Premises used: LieModule.IsNilpotent.nilpotent