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
h : Function.Surjective ↑f
⊢ map f (derivedSeries R L' Nat.zero) = derivedSeries R L Nat.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
h : Function.Surjective ↑f
k : ℕ
ih : map f (derivedSeries R L' k) = derivedSeries R L k
⊢ map f (derivedSeries R L' (Nat.succ k)) = derivedSeries R L (Nat.succ k)
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 : ℕ
h : Function.Surjective ↑f
⊢ map f (derivedSeries R L' k) = derivedSeries R L k
induction' k with k ih
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
h : Function.Surjective ↑f
⊢ map f ⊤ = ⊤
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
h : Function.Surjective ↑f
⊢ map f (derivedSeries R L' Nat.zero) = derivedSeries R L Nat.zero
change (⊤ : LieIdeal R L').map f = ⊤
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
h : Function.Surjective ↑f
⊢ LieHom.idealRange f = ⊤
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
h : Function.Surjective ↑f
⊢ map f ⊤ = ⊤
rw [← f.idealRange_eq_map]
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
h : Function.Surjective ↑f
⊢ LieHom.idealRange f = ⊤
exact f.idealRange_eq_top_of_surjective h
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
h : Function.Surjective ↑f
k : ℕ
ih : map f (derivedSeries R L' k) = derivedSeries R L k
⊢ map f (derivedSeries R L' (Nat.succ k)) = derivedSeries R L (Nat.succ k)
simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]