-- Mathlib/Algebra/Lie/Engel.lean
theorem isNilpotentOfIsNilpotentSpanSupEqTop (hnp : IsNilpotent <| toEnd R L M x)
    (hIM : IsNilpotent I M) : IsNilpotent L M

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hnp : _root_.IsNilpotent ((toEnd R L M) x)
hIM : LieModule.IsNilpotent (↥I) M
⊢ LieModule.IsNilpotent L M

Tactic:
obtain ⟨n, hn⟩ := hnp

Result:
case intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
⊢ LieModule.IsNilpotent L M

Proof state:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
have hk' : I.lcs M k = ⊥ := by
  simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]

Result:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
⊢ LieModule.IsNilpotent L M

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
use k * n

Result:
case h
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ lowerCentralSeries R L M (k * n) = ⊥

Proof state:
case h
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ lowerCentralSeries R L M (k * n) = ⊥

Tactic:
simpa [hk'] using this k

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ LieModule.IsNilpotent L M

Tactic:
rw [isNilpotent_iff R]

Result:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Proof state:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
⊢ ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l

Tactic:
intro l

Result:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
l : ℕ
⊢ lowerCentralSeries R L M (l * n) ≤ I.lcs M l

Proof state:
case intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
⊢ LieModule.IsNilpotent L M

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

Result:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
⊢ LieModule.IsNilpotent L M

Proof state:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
l : ℕ
⊢ lowerCentralSeries R L M (l * n) ≤ I.lcs M l

Tactic:
induction l with
| zero => simp
| succ l ih => exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih

Result:
no goals