case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ ∃ k, lowerCentralSeries R L L k = ⊥
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
⊢ ∃ k, lowerCentralSeries R L L k = ⊥
obtain ⟨k, hk⟩ := id h₁
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ lowerCentralSeries R L L k = ⊥
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ ∃ k, lowerCentralSeries R L L k = ⊥
use k
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ lowerCentralSeries R L L k = ⊥
apply LieIdeal.bot_of_map_eq_bot h₂
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
rw [eq_bot_iff, ← hk]
no goals
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
apply LieIdeal.map_lowerCentralSeries_le