case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
⊢ derivedSeries R { x // x ∈ ↑I } Nat.zero = comap (incl I) (derivedSeriesOfIdeal R L Nat.zero I)

case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeries R { x // x ∈ ↑I } k = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ derivedSeries R { x // x ∈ ↑I } (Nat.succ k) = comap (incl I) (derivedSeriesOfIdeal R L (Nat.succ k) I)
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
⊢ derivedSeries R { x // x ∈ ↑I } k = comap (incl I) (derivedSeriesOfIdeal R L k I)
induction' k with k ih
no goals
case zero
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
⊢ derivedSeries R { x // x ∈ ↑I } Nat.zero = comap (incl I) (derivedSeriesOfIdeal R L Nat.zero I)
simp only [Nat.zero_eq, derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤ = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤, derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤⁆ =
    comap (incl I) ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeries R { x // x ∈ ↑I } k = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ derivedSeries R { x // x ∈ ↑I } (Nat.succ k) = comap (incl I) (derivedSeriesOfIdeal R L (Nat.succ k) I)
simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤ = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap (incl I) (derivedSeriesOfIdeal R L k I), comap (incl I) (derivedSeriesOfIdeal R L k I)⁆ =
    comap (incl I) ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤ = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤, derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤⁆ =
    comap (incl I) ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
rw [ih]
no goals
case succ
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
k : ℕ
ih : derivedSeriesOfIdeal R { x // x ∈ ↑I } k ⊤ = comap (incl I) (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap (incl I) (derivedSeriesOfIdeal R L k I), comap (incl I) (derivedSeriesOfIdeal R L k I)⁆ =
    comap (incl I) ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
exact comap_bracket_incl_of_le I
  (derivedSeriesOfIdeal_le_self I k) (derivedSeriesOfIdeal_le_self I k)