case zero
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lcs I M Nat.zero) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M Nat.zero)

case succ
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ ↑(lcs I M (Nat.succ k)) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M (Nat.succ k))
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
induction' k with k ih
no goals
case zero
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lcs I M Nat.zero) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M Nat.zero)
simp
case succ
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ Submodule.span R {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} =
    Submodule.span R {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
case succ
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ ↑(lcs I M (Nat.succ k)) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M (Nat.succ k))
simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
  (I.lcs M k).mem_coeSubmodule, ih, LieSubmodule.mem_coeSubmodule, LieSubmodule.mem_top,
  true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
case succ.e_s
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} =
    {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
case succ
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ Submodule.span R {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} =
    Submodule.span R {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
congr
case succ.e_s.h
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} ↔
    m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
case succ.e_s
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} =
    {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
ext m
case succ.e_s.h.mp
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}

case succ.e_s.h.mpr
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m}
case succ.e_s.h
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} ↔
    m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
constructor
case succ.e_s.h.mp.intro.intro.intro.intro
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R { x // x ∈ ↑I } M k
⊢ ⁅x, m⁆ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
case succ.e_s.h.mp
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
rintro ⟨x, hx, m, hm, rfl⟩
no goals
case succ.e_s.h.mp.intro.intro.intro.intro
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R { x // x ∈ ↑I } M k
⊢ ⁅x, m⁆ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
exact ⟨⟨x, hx⟩, m, hm, rfl⟩
case succ.e_s.h.mpr.intro.mk.intro.intro
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
x : L
hx : x ∈ ↑I
m : M
hm : m ∈ lowerCentralSeries R { x // x ∈ ↑I } M k
⊢ ⁅↑{ val := x, property := hx }, m⁆ ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m}
case succ.e_s.h.mpr
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m}
rintro ⟨⟨x, hx⟩, m, hm, rfl⟩
no goals
case succ.e_s.h.mpr.intro.mk.intro.intro
R : Type u_2
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
x : L
hx : x ∈ ↑I
m : M
hm : m ∈ lowerCentralSeries R { x // x ∈ ↑I } M k
⊢ ⁅↑{ val := x, property := hx }, m⁆ ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m}
exact ⟨x, hx, m, hm, rfl⟩