-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lowerCentralSeries_eq_lcs_comap : lowerCentralSeries R L N k = (N.lcs k).comap N.incl

Proof state:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lowerCentralSeries R L (↥N) (k + 1) = comap N.incl (lcs (k + 1) N)

Tactic:
simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢

Result:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ ⁅⊤, lowerCentralSeries R L (↥N) k⁆ = comap N.incl ⁅⊤, lcs k N⁆

Proof state:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lcs k N ≤ N.incl.range

Tactic:
rw [N.range_incl]

Result:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lcs k N ≤ N

Proof state:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ ⁅⊤, lowerCentralSeries R L (↥N) k⁆ = comap N.incl ⁅⊤, lcs k N⁆

Tactic:
have : N.lcs k ≤ N.incl.range := by
  rw [N.range_incl]
  apply lcs_le_self

Result:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
this : lcs k N ≤ N.incl.range
⊢ ⁅⊤, lowerCentralSeries R L (↥N) k⁆ = comap N.incl ⁅⊤, lcs k N⁆

Proof state:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lcs k N ≤ N

Tactic:
apply lcs_le_self

Result:
no goals

Proof state:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
this : lcs k N ≤ N.incl.range
⊢ ⁅⊤, lowerCentralSeries R L (↥N) k⁆ = comap N.incl ⁅⊤, lcs k N⁆

Tactic:
rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl this]

Result:
no goals

Proof state:
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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)

Tactic:
induction k with
| zero => simp
| succ k ih =>
  simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
  have : N.lcs k ≤ N.incl.range := by
    rw [N.range_incl]
    apply lcs_le_self
  rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl this]

Result:
no goals

Proof state:
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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ lowerCentralSeries R L (↥N) 0 = comap N.incl (lcs 0 N)

Tactic:
simp

Result:
no goals