-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeriesOfIdeal_le {I J : LieIdeal R L} {k l : ℕ} (h₁ : I ≤ J) (h₂ : l ≤ k) :
    D k I ≤ D l J

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ D (k + 1) I ≤ D l J

Tactic:
have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ ∨ l ≤ k
⊢ D (k + 1) I ≤ D l J

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J

Tactic:
exact h₁

Result:
no goals

Proof state:
case succ.inl
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ D (k + 1) I ≤ D l J

Tactic:
rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]

Result:
case succ.inl
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
h₁ : I ≤ J
h₂ : l ≤ k
⊢ D k I ≤ D l J

Tactic:
revert l

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k : ℕ
h₁ : I ≤ J
⊢ ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D 0 I ≤ D l J

Tactic:
rw [h₂, derivedSeriesOfIdeal_zero]

Result:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J

Proof state:
case succ.inl
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ ⁅D k I, D k I⁆ ≤ ⁅D k J, D k J⁆

Tactic:
exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ l = k.succ ∨ l ≤ k

Tactic:
rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k : ℕ
h₁ : I ≤ J
⊢ ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J

Tactic:
induction' k with k ih <;> intro l h₂

Result:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l ≤ 0
⊢ D 0 I ≤ D l J

case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ D (k + 1) I ≤ D l J

Proof state:
case succ.inr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ D (k + 1) I ≤ D l J

Tactic:
rw [derivedSeriesOfIdeal_succ]

Result:
case succ.inr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J

Proof state:
case succ.inr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J

Tactic:
exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l ≤ 0
⊢ D 0 I ≤ D l J

Tactic:
rw [le_zero_iff] at h₂

Result:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D 0 I ≤ D l J

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ ∨ l ≤ k
⊢ D (k + 1) I ≤ D l J

Tactic:
rcases h with h | h

Result:
case succ.inl
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ
⊢ D (k + 1) I ≤ D l J

case succ.inr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ D (k + 1) I ≤ D l J