-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem antitone_lowerCentralSeries : Antitone <| lowerCentralSeries R L M

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

Tactic:
rcases Nat.of_le_succ h with (hk | hk)

Result:
case succ.inl
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

case succ.inr
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l = k.succ
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
l : ℕ
⊢ l ≤ 0 → lowerCentralSeries R L M 0 ≤ lowerCentralSeries R L M l

Tactic:
exact fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl

Result:
no goals

Proof state:
case succ.inl
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

Tactic:
rw [lowerCentralSeries_succ]

Result:
case succ.inl
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ ≤ lowerCentralSeries R L M l

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
⊢ Antitone (lowerCentralSeries R L M)

Tactic:
intro l k

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
l k : ℕ
⊢ l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l

Proof state:
case succ.inl
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ ≤ lowerCentralSeries R L M l

Tactic:
exact (LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)

Result:
no goals

Proof state:
case succ.inr
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l = k.succ
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

Tactic:
exact hk.symm ▸ le_rfl

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
⊢ l ≤ k + 1 → lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

Tactic:
intro h

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l