case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } Nat.zero) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } Nat.zero)

case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } (Nat.succ k)) ≤
    ↑(lowerCentralSeries R L { x // x ∈ ↑I } (Nat.succ k))
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
induction' k with k ih
no goals
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } Nat.zero) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } Nat.zero)
simp
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } (Nat.succ k)) ≤
    ↑(lowerCentralSeries R L { x // x ∈ ↑I } (Nat.succ k))
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
case succ.h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
apply Submodule.span_mono
case succ.h.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
y z : { x // x ∈ ↑I }
hz : z ∈ lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case succ.h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
no goals
case succ.h.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
y z : { x // x ∈ ↑I }
hz : z ∈ lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩