-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem eventually_iInf_lowerCentralSeries_eq [IsArtinian R M] :
    ∀ᶠ l in Filter.atTop, ⨅ 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
inst✝ : IsArtinian R M
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l

Tactic:
have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ :=
  LieSubmodule.wellFoundedLT_of_isArtinian R L M

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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l

Proof state:
case intro
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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : l ≥ n
m : ℕ
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

Tactic:
rcases le_or_lt l m with h | h

Result:
case intro.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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

case intro.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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : l ≥ n
m : ℕ
h : m < l
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

Proof state:
case intro.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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : l ≥ n
m : ℕ
h : m < l
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

Tactic:
exact antitone_lowerCentralSeries R L M (le_of_lt h)

Result:
no goals

Proof state:
case intro.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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

Tactic:
rw [← hn _ hl, ← hn _ (hl.trans h)]

Result:
no goals

Proof state:
case intro
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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l

Tactic:
refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

Result:
case intro
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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : l ≥ n
m : ℕ
⊢ lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m

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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
  h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩

Result:
case intro
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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l