case zero
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeries R L { x // x ∈ ↑N } Nat.zero = comap (incl N) (lcs Nat.zero N)

case succ
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lowerCentralSeries R L { x // x ∈ ↑N } (Nat.succ k) = comap (incl N) (lcs (Nat.succ k) N)
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
induction' k with k ih
no goals
case zero
R : Type u
L : Type v
M : Type w
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
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeries R L { x // x ∈ ↑N } Nat.zero = comap (incl N) (lcs Nat.zero N)
simp
case succ
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ ⁅⊤, lowerCentralSeries R L { x // x ∈ ↑N } k⁆ = comap (incl N) ⁅⊤, lcs k N⁆
case succ
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lowerCentralSeries R L { x // x ∈ ↑N } (Nat.succ k) = comap (incl N) (lcs (Nat.succ k) N)
simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
case succ
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
this : lcs k N ≤ LieModuleHom.range (incl N)
⊢ ⁅⊤, lowerCentralSeries R L { x // x ∈ ↑N } k⁆ = comap (incl N) ⁅⊤, lcs k N⁆
case succ
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ ⁅⊤, lowerCentralSeries R L { x // x ∈ ↑N } k⁆ = comap (incl N) ⁅⊤, lcs k N⁆
have : N.lcs k ≤ N.incl.range := by
  rw [N.range_incl]
  apply lcs_le_self
no goals
case succ
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
this : lcs k N ≤ LieModuleHom.range (incl N)
⊢ ⁅⊤, lowerCentralSeries R L { x // x ∈ ↑N } k⁆ = comap (incl N) ⁅⊤, lcs k N⁆
rw [ih, LieSubmodule.comap_bracket_eq _ _ N.incl N.ker_incl this]
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lcs k N ≤ N
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lcs k N ≤ LieModuleHom.range (incl N)
rw [N.range_incl]
no goals
R : Type u
L : Type v
M : Type w
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lcs k N ≤ N
apply lcs_le_self