-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem coe_lowerCentralSeries_ideal_quot_eq {I : LieIdeal R L} (k : ℕ) :
    LieSubmodule.toSubmodule (lowerCentralSeries R L (L ⧸ I) k) =
      LieSubmodule.toSubmodule (lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)

Proof state:
case succ.e_s.h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
constructor

Result:
case succ.e_s.h.mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

case succ.e_s.h.mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R L (L ⧸ I) 0) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) 0)

Tactic:
simp only [LieModule.lowerCentralSeries_zero, LieSubmodule.top_toSubmodule,
  LieIdeal.top_toLieSubalgebra, LieSubalgebra.top_toSubmodule]

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
congr

Result:
case succ.e_s
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ ↑(lowerCentralSeries R L (L ⧸ I) (k + 1)) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) (k + 1))

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.e_s.h.mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩

Result:
case succ.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R L (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R L (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rw [← LieSubmodule.mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule] at hz

Result:
case succ.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R (L ⧸ I) (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.e_s.h.mpr.intro.mk.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
val✝ : L ⧸ I
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R (L ⧸ I) (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rw [← LieSubmodule.mem_toSubmodule, ← ih, LieSubmodule.mem_toSubmodule] at hz

Result:
case succ.e_s.h.mpr.intro.mk.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
val✝ : L ⧸ I
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R L (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.e_s
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
ext x

Result:
case succ.e_s.h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.e_s.h.mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩

Result:
case succ.e_s.h.mpr.intro.mk.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
val✝ : L ⧸ I
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R (L ⧸ I) (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case succ.e_s.h.mpr.intro.mk.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
val✝ : L ⧸ I
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R L (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩

Result:
no goals

Proof state:
case succ.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R (L ⧸ I) (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩

Result:
no goals