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
I J : LieIdeal R L
k : ℕ
h₁ : I ≤ J
⊢ ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
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
I J : LieIdeal R L
k l : ℕ
h₁ : I ≤ J
h₂ : l ≤ k
⊢ D k I ≤ D l J
revert l
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
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l ≤ Nat.zero
⊢ D Nat.zero I ≤ D l J

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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
⊢ D (Nat.succ k) I ≤ D l J
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
I J : LieIdeal R L
k : ℕ
h₁ : I ≤ J
⊢ ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
induction' k with k ih <;> intro l h₂
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
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D Nat.zero I ≤ D l J
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
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l ≤ Nat.zero
⊢ D Nat.zero I ≤ D l J
rw [Nat.zero_eq, le_zero_iff] at h₂
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
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J
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
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D Nat.zero I ≤ D l J
rw [h₂, derivedSeriesOfIdeal_zero]
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
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J
exact h₁
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k ∨ l ≤ k
⊢ D (Nat.succ k) I ≤ D l J
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
⊢ D (Nat.succ k) I ≤ D l J
have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
case succ.inl
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k
⊢ D (Nat.succ k) I ≤ D l J

case succ.inr
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l ≤ k
⊢ D (Nat.succ k) I ≤ D l J
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k ∨ l ≤ k
⊢ D (Nat.succ k) I ≤ D l J
cases' h with h h
no goals
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
⊢ l = Nat.succ k ∨ l ≤ k
rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
case succ.inl
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆
case succ.inl
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k
⊢ D (Nat.succ k) I ≤ D l J
rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
no goals
case succ.inl
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l = Nat.succ k
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆
exact LieSubmodule.mono_lie _ _ _ _ (ih (le_refl k)) (ih (le_refl k))
case succ.inr
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J
case succ.inr
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l ≤ k
⊢ D (Nat.succ k) I ≤ D l J
rw [derivedSeriesOfIdeal_succ]
no goals
case succ.inr
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
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ Nat.succ k
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J
exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)