-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem coe_lcs_eq [LieModule R L M] :
    LieSubmodule.toSubmodule (I.lcs M k) = lowerCentralSeries R I M k

Proof state:
case zero
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
inst✝ : LieModule R L M
⊢ ↑(I.lcs M 0) = ↑(lowerCentralSeries R (↥I) M 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ.e_s
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} =
    {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Tactic:
ext m

Result:
case succ.e_s.h
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} ↔
    m ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Proof state:
case succ.e_s.h
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} ↔
    m ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Tactic:
constructor

Result:
case succ.e_s.h.mp
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

case succ.e_s.h.mpr
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
m : M
⊢ m ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x}

Proof state:
case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ ↑(I.lcs M (k + 1)) = ↑(lowerCentralSeries R (↥I) M (k + 1))

Tactic:
simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
  (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
  true_and, (I : LieSubalgebra R L).coe_bracket_of_module]

Result:
case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Proof state:
case succ.e_s.h.mpr.intro.mk.intro.intro
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R (↥I) M k
⊢ ⁅↑⟨x, hx⟩, m⁆ ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x}

Tactic:
exact ⟨x, hx, m, hm, rfl⟩

Result:
no goals

Proof state:
case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Tactic:
congr

Result:
case succ.e_s
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} =
    {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Proof state:
case succ.e_s.h.mp.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R (↥I) M k
⊢ ⁅x, m⁆ ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Tactic:
exact ⟨⟨x, hx⟩, m, hm, rfl⟩

Result:
no goals

Proof state:
case succ.e_s.h.mpr
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
m : M
⊢ m ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x}

Tactic:
rintro ⟨⟨x, hx⟩, m, hm, rfl⟩

Result:
case succ.e_s.h.mpr.intro.mk.intro.intro
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R (↥I) M k
⊢ ⁅↑⟨x, hx⟩, m⁆ ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x}

Proof state:
case succ.e_s.h.mp
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
m : M
⊢ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} →
    m ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}

Tactic:
rintro ⟨x, hx, m, hm, rfl⟩

Result:
case succ.e_s.h.mp.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R (↥I) M k
⊢ ⁅x, m⁆ ∈ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}