-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem coe_lcs_range_toEnd_eq (k : ℕ) :
    (lowerCentralSeries R (toEnd R L M).range M k : Submodule R M) =
      lowerCentralSeries R L M k

Proof state:
case succ.e_s
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} =
    {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Tactic:
ext m

Result:
case succ.e_s.h
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} ↔
    m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Proof state:
case succ.e_s.h
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} ↔
    m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Tactic:
constructor

Result:
case succ.e_s.h.mp
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

case succ.e_s.h.mpr
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x}

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
inst✝ : LieModule R L M
k : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Tactic:
congr

Result:
case succ.e_s
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} =
    {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Proof state:
case succ.e_s.h.mp.intro.mk.intro.intro.intro.intro
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
y : L
n : M
hn : n ∈ ↑(lowerCentralSeries R L M k)
⊢ ⁅⟨↑(toEnd R L M) y, ⋯⟩, n⁆ ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Tactic:
exact ⟨y, LieSubmodule.mem_top _, n, hn, rfl⟩

Result:
no goals

Proof state:
case succ.e_s.h.mpr
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x}

Tactic:
rintro ⟨x, -, n, hn, rfl⟩

Result:
case succ.e_s.h.mpr.intro.intro.intro.intro
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
x : L
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ⁅x, n⁆ ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x}

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
inst✝ : LieModule R L M
k : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ ↑(lowerCentralSeries R (↥(toEnd R L M).range) M (k + 1)) = ↑(lowerCentralSeries R L M (k + 1))

Tactic:
simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
  (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, 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
inst✝ : LieModule R L M
k : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Proof state:
case succ.e_s.h.mpr.intro.intro.intro.intro
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
x : L
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ⁅x, n⁆ ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x}

Tactic:
exact
  ⟨⟨toEnd R L M x, LieHom.mem_range_self _ x⟩, LieSubmodule.mem_top _, n, hn, rfl⟩

Result:
no goals

Proof state:
case succ.e_s.h.mp
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

Tactic:
rintro ⟨⟨-, ⟨y, rfl⟩⟩, -, n, hn, rfl⟩

Result:
case succ.e_s.h.mp.intro.mk.intro.intro.intro.intro
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 : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
y : L
n : M
hn : n ∈ ↑(lowerCentralSeries R L M k)
⊢ ⁅⟨↑(toEnd R L M) y, ⋯⟩, n⁆ ∈ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}

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
inst✝ : LieModule R L M
⊢ ↑(lowerCentralSeries R (↥(toEnd R L M).range) M 0) = ↑(lowerCentralSeries R L M 0)

Tactic:
simp

Result:
no goals