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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
⊢ D (k + l) (I + J) ≤ 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
J : LieIdeal R L
k l : ℕ
⊢ D (k + l) (I + J) ≤ D k I + D l J
let D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆
    monotone' := fun I J h => LieSubmodule.mono_lie I J I J h h }
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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
h₁ : ∀ (I J : LieIdeal R L), ↑D₁ (I ⊔ J) ≤ ↑D₁ I ⊔ J
⊢ D (k + l) (I + J) ≤ 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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
⊢ D (k + l) (I + J) ≤ D k I + D l J
have h₁ : ∀ I J : LieIdeal R L, D₁ (I ⊔ J) ≤ D₁ I ⊔ J := by
  simp [LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]
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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (↑D₁^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑D₁^[n₁]) a₁ ⊔ (↑D₁^[n₂]) a₂
⊢ D (k + l) (I + J) ≤ 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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
h₁ : ∀ (I J : LieIdeal R L), ↑D₁ (I ⊔ J) ≤ ↑D₁ I ⊔ J
⊢ D (k + l) (I + J) ≤ D k I + D l J
rw [← D₁.iterate_sup_le_sup_iff] at 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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
h₁ : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : LieIdeal R L), (↑D₁^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑D₁^[n₁]) a₁ ⊔ (↑D₁^[n₂]) a₂
⊢ D (k + l) (I + J) ≤ D k I + D l J
exact h₁ k l I J
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
J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L :=
  { toFun := fun I => ⁅I, I⁆, monotone' := (_ : ∀ (I J : LieIdeal R L), I ≤ J → ⁅I, I⁆ ≤ ⁅J, J⁆) }
⊢ ∀ (I J : LieIdeal R L), ↑D₁ (I ⊔ J) ≤ ↑D₁ I ⊔ J
simp [LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]