refactor: delete IsWellOrderLimitElement.lean (#15904)

I understand this is quite a bold move, and I hope not to come off as confrontational. I argue that `Order/IsWellOrderLimitElement.lean` duplicates existing API, and that all the theorems proven within it already exist in some other form.

First, note that the typeclass assumptions `LinearOrder α` + `IsWellOrder α (· < ·)` **very nearly** imply `ConditionallyCompleteLinearOrderBot α` through [`IsWellOrder.conditionallyCompleteLinearOrderBot`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/ConditionallyCompleteLattice/Basic.html#IsWellOrder.conditionallyCompleteLinearOrderBot). The only missing assumption is `OrderBot α`, which actually follows from `Nonempty α` through [`WellFoundedLT.toOrderBot`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/WellFounded.html#WellFoundedLT.toOrderBot). All theorems in this file assume the existence of some `a : α`, so that's covered. Most of the only other file importing this one assumes `OrderBot α` directly.

`ConditionallyCompleteLinearOrder α` in turn implies `SuccOrder α` through `ConditionallyCompleteLinearOrder.toSuccOrder` (#15863), so assuming it yields no loss of generality. In fact, doing things this way means we can set nicer def-eqs for `@succ α`, such as `succ o = o + 1` on ordinals.

As for `IsWellOrderLimitElement`, we already have [`Order.IsSuccLimit`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Limit.html#Order.IsSuccLimit) with only trivial typeclass assumptions.

To summarize, here are the correspondences between definitions and theorems in this file and other definitions and theorems in Mathlib, applicable under equivalent typeclasss assumptions:
- `wellOrderSucc` → [`Order.succ`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Basic.html#Order.succ)
- `self_le_wellOrderSucc` → [`Order.le_succ`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Basic.html#Order.le_succ)
- `wellOrderSucc_le` → [`Order.succ_le_of_lt`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Basic.html#Order.succ_le_of_lt)
- `self_lt_wellOrderSucc` → [`Order.lt_succ_of_not_isMax`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Basic.html#Order.lt_succ_of_not_isMax)
- `le_of_lt_wellOrderSucc` → [`Order.le_of_lt_succ`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Basic.html#Order.le_of_lt_succ).
- `IsWellOrderLimitElement`→ [`Order.IsSuccLimit`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Limit.html#Order.IsSuccLimit)
- `IsWellOrderLimitElement.neq_bot` → (already implied by `IsSuccLimit`)
- `IsWellOrderLimitElement.bot_lt` → [`Ne.bot_lt`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/BoundedOrder.html#Ne.bot_lt)
- `IsWellOrderLimitElement.wellOrderSucc_lt` → [`Order.IsSuccLimit.succ_lt`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Limit.html#Order.IsSuccLimit.succ_lt)
- `eq_bot_or_eq_succ_or_isWellOrderLimitElement` → [`Order.isSuccLimitRecOn`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Limit.html#Order.isSuccLimitRecOn)
- `Nat.wellOrderSucc_eq` → [`Nat.succ_eq_succ`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/SuccPred.html#Nat.succ_eq_succ)
- `Nat.not_isWellOrderLimitElement` → [`Order.IsSuccLimit.isMin_of_noMax`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/SuccPred/Limit.html#Order.IsSuccLimit.isMin_of_noMax)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

Mathlib.lean

@@ -3801,7 +3801,6 @@ import Mathlib.Order.Interval.Set.SurjOn
 import Mathlib.Order.Interval.Set.UnorderedInterval
 import Mathlib.Order.Interval.Set.WithBotTop
 import Mathlib.Order.Irreducible
-import Mathlib.Order.IsWellOrderLimitElement
 import Mathlib.Order.Iterate
 import Mathlib.Order.JordanHolder
 import Mathlib.Order.KonigLemma

Mathlib/CategoryTheory/SmallObject/Iteration.lean

@@ -5,7 +5,8 @@ Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Limits.IsLimit
-import Mathlib.Order.IsWellOrderLimitElement
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Order.SuccPred.Limit
 
 /-! # Transfinite iterations of a functor
 
@@ -37,19 +38,19 @@ namespace CategoryTheory
 open Category Limits
 
 variable {C : Type*} [Category C] {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ)
-  {J : Type u} [LinearOrder J]
+  {J : Type u} [Preorder J]
 
 namespace Functor
 
 namespace Iteration
 
 variable {j : J} (F : { i // i ≤ j } ⥤ C)
 
-/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨wellOrderSucc i, _⟩` when `F : { i // i ≤ j } ⥤ C`
+/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩` when `F : { i // i ≤ j } ⥤ C`
 and `i : J` is such that `i < j`. -/
-noncomputable abbrev mapSucc' [IsWellOrder J (· < ·)] (i : J) (hi : i < j) :
-    F.obj ⟨i, hi.le⟩ ⟶ F.obj ⟨wellOrderSucc i, wellOrderSucc_le hi⟩ :=
-  F.map (homOfLE (by simpa only [Subtype.mk_le_mk] using self_le_wellOrderSucc i))
+noncomputable abbrev mapSucc' [SuccOrder J] (i : J) (hi : i < j) :
+    F.obj ⟨i, hi.le⟩ ⟶ F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ :=
+  F.map <| homOfLE <| Subtype.mk_le_mk.2 <| Order.le_succ i
 
 variable {i : J} (hi : i ≤ j)
 
@@ -78,29 +79,26 @@ def coconeOfLE : Cocone (restrictionLT F hi) where
 
 end Iteration
 
-variable [IsWellOrder J (· < ·)] [OrderBot J]
-
 /-- The category of `j`th iterations of a functor `Φ` equipped with a natural
 transformation `ε : 𝟭 C ⟶ Φ`. An object consists of the data of all iterations
 of `Φ` for `i : J` such that `i ≤ j` (this is the field `F`). Such objects are
 equipped with data and properties which characterizes the iterations up to a unique
 isomorphism for the three types of elements: `⊥`, successors, limit elements. -/
-structure Iteration (j : J) where
+structure Iteration [Preorder J] [OrderBot J] [SuccOrder J] (j : J) where
   /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/
   F : { i // i ≤ j } ⥤ C ⥤ C
   /-- The zeroth iteration is the identity functor. -/
   isoZero : F.obj ⟨⊥, bot_le⟩ ≅ 𝟭 C
   /-- The iteration on a successor element is obtained by composition of
   the previous iteration with `Φ`. -/
-  isoSucc (i : J) (hi : i < j) :
-    F.obj ⟨wellOrderSucc i, wellOrderSucc_le hi⟩ ≅ F.obj ⟨i, hi.le⟩ ⋙ Φ
+  isoSucc (i : J) (hi : i < j) : F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅ F.obj ⟨i, hi.le⟩ ⋙ Φ
   /-- The natural map from an iteration to its successor is induced by `ε`. -/
   mapSucc'_eq (i : J) (hi : i < j) :
     Iteration.mapSucc' F i hi = whiskerLeft _ ε ≫ (isoSucc i hi).inv
   /-- If `i` is a limit element, the `i`th iteration is the colimit
   of `k`th iterations for `k < i`. -/
-  isColimit (i : J) [IsWellOrderLimitElement i] (hi : i ≤ j) :
-    IsColimit (Iteration.coconeOfLE F hi)
+  isColimit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
+    IsColimit (Iteration.coconeOfLE F hij)
 
 namespace Iteration
 
@@ -109,12 +107,12 @@ variable {j : J}
 
 section
 
-variable (iter : Φ.Iteration ε j)
+variable [OrderBot J] [SuccOrder J] (iter : Φ.Iteration ε j)
 
 /-- For `iter : Φ.Iteration.ε j`, this is the map
-`iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨wellOrderSucc i, _⟩` if `i : J` is such that `i < j`. -/
+`iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨Order.succ i, _⟩` if `i : J` is such that `i < j`. -/
 noncomputable abbrev mapSucc (i : J) (hi : i < j) :
-    iter.F.obj ⟨i, hi.le⟩ ⟶ iter.F.obj ⟨wellOrderSucc i, wellOrderSucc_le hi⟩ :=
+    iter.F.obj ⟨i, hi.le⟩ ⟶ iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ :=
   mapSucc' iter.F i hi
 
 lemma mapSucc_eq (i : J) (hi : i < j) :
@@ -123,7 +121,7 @@ lemma mapSucc_eq (i : J) (hi : i < j) :
 
 end
 
-variable (iter₁ iter₂ : Φ.Iteration ε j)
+variable [OrderBot J] [SuccOrder J] (iter₁ iter₂ : Φ.Iteration ε j)
 
 /-- A morphism between two objects `iter₁` and `iter₂` in the
 category `Φ.Iteration ε j` of `j`th iterations of a functor `Φ`
@@ -136,7 +134,7 @@ structure Hom where
   natTrans_app_zero :
     natTrans.app ⟨⊥, bot_le⟩ = iter₁.isoZero.hom ≫ iter₂.isoZero.inv := by aesop_cat
   natTrans_app_succ (i : J) (hi : i < j) :
-    natTrans.app ⟨wellOrderSucc i, wellOrderSucc_le hi⟩ = (iter₁.isoSucc i hi).hom ≫
+    natTrans.app ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = (iter₁.isoSucc i hi).hom ≫
       whiskerRight (natTrans.app ⟨i, hi.le⟩) _ ≫ (iter₂.isoSucc i hi).inv := by aesop_cat
 
 namespace Hom
@@ -172,17 +170,27 @@ instance : Category (Iteration ε j) where
   id := id
   comp := comp
 
-instance : Subsingleton (iter₁ ⟶ iter₂) where
-  allEq f g := ext' (by
-    let P := fun (i : J) => ∀ (hi : i ≤ j), f.natTrans.app ⟨i, hi⟩ = g.natTrans.app ⟨i, hi⟩
-    suffices ∀ (i : J), P i by
+instance {J} {j : J} [PartialOrder J] [OrderBot J] [WellFoundedLT J] [SuccOrder J]
+    {iter₁ iter₂ : Iteration ε j} :
+    Subsingleton (iter₁ ⟶ iter₂) where
+  allEq f g := by
+    apply ext'
+    suffices ∀ i hi, f.natTrans.app ⟨i, hi⟩ = g.natTrans.app ⟨i, hi⟩ by
       ext ⟨i, hi⟩ : 2
       apply this
-    refine fun _ => WellFoundedLT.induction _ (fun i hi hi' => ?_)
-    obtain rfl|⟨i, rfl, hi''⟩|_ := eq_bot_or_eq_succ_or_isWellOrderLimitElement i
-    · simp only [natTrans_app_zero]
-    · simp only [Hom.natTrans_app_succ _ i (lt_of_lt_of_le hi'' hi'), hi i hi'']
-    · exact (iter₁.isColimit i hi').hom_ext (fun ⟨k, hk⟩ => by simp [hi k hk]))
+    intro i
+    induction i using SuccOrder.limitRecOn with
+    | hm j H =>
+      have := H.eq_bot
+      subst this
+      simp [natTrans_app_zero]
+    | hs j H IH =>
+      intro hj
+      simp [Hom.natTrans_app_succ, IH, (Order.lt_succ_of_not_isMax H).trans_le hj]
+    | hl j H IH =>
+      apply fun hj ↦ (iter₁.isColimit j H hj).hom_ext ?_
+      rintro ⟨k, hk⟩
+      simp [IH k hk]
 
 end Hom