-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem LieModule.coe_lowerCentralSeries_ideal_le {I : LieIdeal R L} (k : ℕ) :
    LieSubmodule.toSubmodule (lowerCentralSeries R I I k) ≤ lowerCentralSeries R L I k

Proof state:
case succ.h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩

Result:
case succ.h.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
y z : ↥I
hz : z ∈ lowerCentralSeries R (↥I) (↥I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
apply Submodule.span_mono

Result:
case succ.h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.h.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
y z : ↥I
hz : z ∈ lowerCentralSeries R (↥I) (↥I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

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

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)

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⟩

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R (↥I) (↥I) 0) ≤ ↑(lowerCentralSeries R L (↥I) 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ ↑(lowerCentralSeries R (↥I) (↥I) (k + 1)) ≤ ↑(lowerCentralSeries R L (↥I) (k + 1))

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

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}