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 { x // x ∈ LieHom.range (toEndomorphism R L M) } M Nat.zero) =
    ↑(lowerCentralSeries R L M Nat.zero)

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 { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M (Nat.succ k)) =
    ↑(lowerCentralSeries R L M (Nat.succ k))
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 : ℕ
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
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 { x // x ∈ LieHom.range (toEndomorphism R L M) } M Nat.zero) =
    ↑(lowerCentralSeries R L M Nat.zero)
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 { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ Submodule.span R {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    Submodule.span R {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
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 { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M (Nat.succ k)) =
    ↑(lowerCentralSeries R L M (Nat.succ k))
simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
  (lowerCentralSeries R (toEndomorphism R L M).range M k).mem_coeSubmodule, ih]
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
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 { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ Submodule.span R {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    Submodule.span R {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
congr
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} ↔
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
ext m
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}

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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m}
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} ↔
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
constructor
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
y : L
n : M
hn : n ∈ ↑(lowerCentralSeries R L M k)
⊢ ⁅{ val := ↑↑(toEndomorphism R L M) y,
        property := (_ : ∃ y_1, ↑↑(toEndomorphism R L M) y_1 = ↑↑(toEndomorphism R L M) y) },
      n⁆ ∈
    {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
rintro ⟨⟨-, ⟨y, rfl⟩⟩, -, n, hn, rfl⟩
no goals
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
y : L
n : M
hn : n ∈ ↑(lowerCentralSeries R L M k)
⊢ ⁅{ val := ↑↑(toEndomorphism R L M) y,
        property := (_ : ∃ y_1, ↑↑(toEndomorphism R L M) y_1 = ↑↑(toEndomorphism R L M) y) },
      n⁆ ∈
    {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
exact ⟨y, LieSubmodule.mem_top _, n, hn, rfl⟩
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
x : L
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ⁅x, n⁆ ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m}
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m}
rintro ⟨x, -, n, hn, rfl⟩
no goals
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✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
x : L
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ⁅x, n⁆ ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m}
exact
  ⟨⟨toEndomorphism R L M x, LieHom.mem_range_self _ x⟩, LieSubmodule.mem_top _, n, hn, rfl⟩