refactor(Order/OrderIsoNat): use WellFoundedGT in monotone chain co…

…ndition (#20782)

Instead of `WellFounded (· > ·)`, we write `WellFoundedGT α`. We also add some docstrings, and one-sided versions of the theorem which take in `WellFoundedGT α` as a typeclass argument.

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -171,7 +171,7 @@ theorem eventually_iInf_lowerCentralSeries_eq [IsArtinian R M] :
   have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ :=
     LieSubmodule.wellFoundedLT_of_isArtinian R L M
   obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
-    WellFounded.monotone_chain_condition.mp h_wf.wf ⟨_, antitone_lowerCentralSeries R L M⟩
+    h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩
   refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
   rcases le_or_lt l m with h | h
   · rw [← hn _ hl, ← hn _ (hl.trans h)]

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -263,10 +263,9 @@ noncomputable def maxUnifEigenspaceIndex (f : End R M) (μ : R) :=
 
 /-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
 `(f - μ • id) ^ k` for some `k`. -/
-lemma genEigenspace_top_eq_maxUnifEigenspaceIndex [h : IsNoetherian R M] (f : End R M) (μ : R) :
+lemma genEigenspace_top_eq_maxUnifEigenspaceIndex [IsNoetherian R M] (f : End R M) (μ : R) :
     genEigenspace f μ ⊤ = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) := by
-  rw [isNoetherian_iff] at h
-  have := WellFounded.iSup_eq_monotonicSequenceLimit h <|
+  have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <|
     (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom
   convert this using 1
   simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe,

Mathlib/Order/OrderIsoNat.lean

@@ -203,24 +203,50 @@ theorem exists_increasing_or_nonincreasing_subseq (r : α → α → Prop) [IsTr
       exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
   · exact ⟨g, Or.intro_right _ hnr⟩
 
-theorem WellFounded.monotone_chain_condition' [Preorder α] :
-    WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m := by
+/-- The **monotone chain condition**: a preorder is co-well-founded iff every increasing sequence
+contains two non-increasing indices.
+
+See `wellFoundedGT_iff_monotone_chain_condition` for a stronger version on partial orders. -/
+theorem wellFoundedGT_iff_monotone_chain_condition' [Preorder α] :
+    WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m := by
   refine ⟨fun h a => ?_, fun h => ?_⟩
-  · have hne : (Set.range a).Nonempty := ⟨a 0, by simp⟩
-    obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.has_min _ hne
+  · obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
     exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
-  · refine RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun a => ?_⟩
-    obtain ⟨n, hn⟩ := h (a.swap : ((· < ·) : ℕ → ℕ → Prop) →r ((· < ·) : α → α → Prop)).toOrderHom
+  · rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_no_descending_seq]
+    refine ⟨fun a => ?_⟩
+    obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
     exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)
 
-/-- The "monotone chain condition" below is sometimes a convenient form of well foundedness. -/
-theorem WellFounded.monotone_chain_condition [PartialOrder α] :
-    WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m :=
-  WellFounded.monotone_chain_condition'.trans <| by
+theorem WellFoundedGT.monotone_chain_condition' [Preorder α] [h : WellFoundedGT α] (a : ℕ →o α) :
+    ∃ n, ∀ m, n ≤ m → ¬a n < a m :=
+  wellFoundedGT_iff_monotone_chain_condition'.1 h a
+
+/-- A stronger version of the **monotone chain** condition for partial orders.
+
+See `wellFoundedGT_iff_monotone_chain_condition'` for a version on preorders.  -/
+theorem wellFoundedGT_iff_monotone_chain_condition [PartialOrder α] :
+    WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m :=
+  wellFoundedGT_iff_monotone_chain_condition'.trans <| by
   congrm ∀ a, ∃ n, ∀ m h, ?_
   rw [lt_iff_le_and_ne]
   simp [a.mono h]
 
+theorem WellFoundedGT.monotone_chain_condition [PartialOrder α] [h : WellFoundedGT α] (a : ℕ →o α) :
+    ∃ n, ∀ m, n ≤ m → a n = a m :=
+  wellFoundedGT_iff_monotone_chain_condition.1 h a
+
+@[deprecated wellFoundedGT_iff_monotone_chain_condition' (since := "2025-01-15")]
+theorem WellFounded.monotone_chain_condition' [Preorder α] :
+    WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m := by
+  rw [← isWellFounded_iff]
+  exact wellFoundedGT_iff_monotone_chain_condition'
+
+@[deprecated wellFoundedGT_iff_monotone_chain_condition (since := "2025-01-15")]
+theorem WellFounded.monotone_chain_condition [PartialOrder α] :
+    WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m := by
+  rw [← isWellFounded_iff]
+  exact wellFoundedGT_iff_monotone_chain_condition
+
 /-- Given an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered
 type, `monotonicSequenceLimitIndex a` is the least natural number `n` for which `aₙ` reaches the
 constant value. For sequences that are not eventually constant, `monotonicSequenceLimitIndex a`
@@ -233,16 +259,23 @@ partially-ordered type. -/
 noncomputable def monotonicSequenceLimit [Preorder α] (a : ℕ →o α) :=
   a (monotonicSequenceLimitIndex a)
 
-theorem WellFounded.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
-    (h : WellFounded ((· > ·) : α → α → Prop)) (a : ℕ →o α) :
-    iSup a = monotonicSequenceLimit a := by
+-- TODO: generalize to a conditionally complete lattice
+theorem WellFoundedGT.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
+    [WellFoundedGT α] (a : ℕ →o α) : iSup a = monotonicSequenceLimit a := by
   refine (iSup_le fun m => ?_).antisymm (le_iSup a _)
   rcases le_or_lt m (monotonicSequenceLimitIndex a) with hm | hm
   · exact a.monotone hm
-  · cases' WellFounded.monotone_chain_condition'.1 h a with n hn
+  · cases' WellFoundedGT.monotone_chain_condition' a with n hn
     have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)
     exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge
 
+@[deprecated WellFoundedGT.iSup_eq_monotonicSequenceLimit (since := "2025-01-15")]
+theorem WellFounded.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
+    (h : WellFounded ((· > ·) : α → α → Prop)) (a : ℕ →o α) :
+    iSup a = monotonicSequenceLimit a := by
+  have : WellFoundedGT α := ⟨h⟩
+  exact WellFoundedGT.iSup_eq_monotonicSequenceLimit a
+
 theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α) [Preorder α]
     [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] :
     ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1) := by

Mathlib/RingTheory/Artinian/Module.lean

@@ -140,9 +140,8 @@ theorem IsArtinian.set_has_minimal [IsArtinian R M] (a : Set <| Submodule R M) (
 
 /-- A module is Artinian iff every decreasing chain of submodules stabilizes. -/
 theorem monotone_stabilizes_iff_artinian :
-    (∀ f : ℕ →o (Submodule R M)ᵒᵈ, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsArtinian R M := by
-  rw [isArtinian_iff]
-  exact WellFounded.monotone_chain_condition.symm
+    (∀ f : ℕ →o (Submodule R M)ᵒᵈ, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsArtinian R M :=
+  wellFoundedGT_iff_monotone_chain_condition.symm
 
 namespace IsArtinian
 

Mathlib/RingTheory/Noetherian/Defs.lean

@@ -160,7 +160,7 @@ theorem set_has_maximal_iff_noetherian :
 /-- A module is Noetherian iff every increasing chain of submodules stabilizes. -/
 theorem monotone_stabilizes_iff_noetherian :
     (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by
-  rw [isNoetherian_iff, WellFounded.monotone_chain_condition]
+  rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]
 
 variable [IsNoetherian R M]