chore: make IsSuccLimit a structure

Mathlib/Order/SuccPred/InitialSeg.lean

@@ -49,7 +49,7 @@ theorem isSuccPrelimit_apply_iff (f : α ≤i β) : IsSuccPrelimit (f a) ↔ IsS
 
 @[simp]
 theorem isSuccLimit_apply_iff (f : α ≤i β) : IsSuccLimit (f a) ↔ IsSuccLimit a := by
-  simp [IsSuccLimit]
+  simp [isSuccLimit_iff]
 
 alias ⟨_, map_isSuccPrelimit⟩ := isSuccPrelimit_apply_iff
 alias ⟨_, map_isSuccLimit⟩ := isSuccLimit_apply_iff

Mathlib/Order/SuccPred/Limit.lean

@@ -76,50 +76,64 @@ It's so named because in a successor order, a successor limit can't be the succe
 smaller.
 
 Use `IsSuccPrelimit` if you want to include the case of a minimal element. -/
-@[to_dual
-/-- A predecessor limit is a value that isn't maximal and doesn't cover any other.
+@[mk_iff]
+structure IsSuccLimit (a : α) : Prop where
+  /-- Successor limits aren't minimal. -/
+  not_isMin : ¬ IsMin a
+  /-- Successor limits don't cover any other elements. -/
+  isSuccPrelimit : IsSuccPrelimit a
+
+/-- A predecessor limit is a value that isn't maximal and isn't covered by any other.
 
 It's so named because in a predecessor order, a predecessor limit can't be the predecessor of
 anything larger.
 
-Use `IsPredPrelimit` if you want to include the case of a maximal element. -/]
-def IsSuccLimit (a : α) : Prop :=
-  ¬ IsMin a ∧ IsSuccPrelimit a
+Use `IsPredPrelimit` if you want to include the case of a maximal element. -/
+@[mk_iff, to_dual existing]
+structure IsPredLimit (a : α) : Prop where
+  /-- Predecessor limits aren't maximal. -/
+  not_isMax : ¬ IsMax a
+  /-- Predecessor limits aren't covered by any other elements. -/
+  isPredPrelimit : IsPredPrelimit a
+
+attribute [to_dual existing]
+  IsSuccLimit.mk IsSuccLimit.not_isMin IsSuccLimit.isSuccPrelimit isSuccLimit_iff
+attribute [simp] IsSuccLimit.isSuccPrelimit IsPredLimit.isPredPrelimit
 
 @[to_dual (attr := simp)]
 theorem isSuccLimit_toDual_iff : IsSuccLimit (toDual a) ↔ IsPredLimit a := by
-  simp [IsSuccLimit, IsPredLimit]
+  simp [isSuccLimit_iff, isPredLimit_iff]
 
 @[to_dual] alias ⟨_, IsPredLimit.dual⟩ := isSuccLimit_toDual_iff
 
 @[to_dual]
-protected theorem IsSuccLimit.not_isMin (h : IsSuccLimit a) : ¬ IsMin a := h.1
-
-@[to_dual (attr := simp)]
-protected theorem IsSuccLimit.isSuccPrelimit (h : IsSuccLimit a) : IsSuccPrelimit a := h.2
+theorem not_isSuccLimit_iff : ¬ IsSuccLimit a ↔ IsMin a ∨ ¬ IsSuccPrelimit a := by
+  rw [isSuccLimit_iff, not_and_or, not_not]
 
 @[deprecated IsPredLimit.isPredPrelimit (since := "2026-02-22")]
 theorem not_isPredLimit_of_not_isPredPrelimit : ¬ IsPredPrelimit a → ¬ IsPredLimit a :=
   mt IsPredLimit.isPredPrelimit
 
-@[to_dual]
+set_option linter.existingAttributeWarning false in
+@[to_dual, deprecated IsSuccLimit.mk (since := "2026-04-19")]
 theorem IsSuccPrelimit.isSuccLimit_of_not_isMin (h : IsSuccPrelimit a) (ha : ¬ IsMin a) :
     IsSuccLimit a :=
   ⟨ha, h⟩
 
-@[to_dual]
-theorem IsSuccPrelimit.isSuccLimit [NoMinOrder α] (h : IsSuccPrelimit a) : IsSuccLimit a :=
-  h.isSuccLimit_of_not_isMin (not_isMin a)
+attribute [deprecated IsPredLimit.mk (since := "2026-04-19")]
+IsPredPrelimit.isPredLimit_of_not_isMax
 
 @[to_dual]
 theorem isSuccPrelimit_iff_isSuccLimit_of_not_isMin (h : ¬ IsMin a) :
-    IsSuccPrelimit a ↔ IsSuccLimit a :=
-  ⟨fun ha ↦ ha.isSuccLimit_of_not_isMin h, IsSuccLimit.isSuccPrelimit⟩
+    IsSuccPrelimit a ↔ IsSuccLimit a := by
+  simp [isSuccLimit_iff, h]
 
 @[to_dual]
 theorem isSuccPrelimit_iff_isSuccLimit [NoMinOrder α] : IsSuccPrelimit a ↔ IsSuccLimit a :=
   isSuccPrelimit_iff_isSuccLimit_of_not_isMin (not_isMin a)
 
+@[to_dual] alias ⟨IsSuccPrelimit.isSuccLimit, _⟩ := isSuccPrelimit_iff_isSuccLimit
+
 @[to_dual]
 protected theorem _root_.IsMin.not_isSuccLimit (h : IsMin a) : ¬ IsSuccLimit a :=
   fun ha ↦ ha.not_isMin h
@@ -151,10 +165,6 @@ theorem IsSuccLimit.ne_bot [OrderBot α] (h : IsSuccLimit a) : a ≠ ⊥ := by
   rintro rfl
   exact not_isSuccLimit_bot h
 
-@[to_dual]
-theorem not_isSuccLimit_iff : ¬ IsSuccLimit a ↔ IsMin a ∨ ¬ IsSuccPrelimit a := by
-  rw [IsSuccLimit, not_and_or, not_not]
-
 @[to_dual]
 theorem IsSuccPrelimit.subtypeVal {s : Set α} (hs : IsLowerSet s) {a : s}
     (ha : IsSuccPrelimit a) : IsSuccPrelimit a.1 := by
@@ -261,10 +271,7 @@ variable [PartialOrder α]
 
 @[to_dual]
 theorem isSuccLimit_iff_of_orderBot [OrderBot α] : IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a := by
-  rw [IsSuccLimit, isMin_iff_eq_bot]
-
-@[deprecated (since := "2026-03-31")] alias isSuccLimit_iff := isSuccLimit_iff_of_orderBot
-@[deprecated (since := "2026-03-31")] alias isPredLimit_iff := isPredLimit_iff_of_orderTop
+  rw [isSuccLimit_iff, isMin_iff_eq_bot]
 
 @[to_dual lt_top]
 theorem IsSuccLimit.bot_lt [OrderBot α] (h : IsSuccLimit a) : ⊥ < a :=
@@ -298,7 +305,7 @@ theorem mem_range_succ_or_isSuccPrelimit (a) : a ∈ range (succ : α → α) 
 @[to_dual]
 theorem isMin_or_mem_range_succ_or_isSuccLimit (a) :
     IsMin a ∨ a ∈ range (succ : α → α) ∨ IsSuccLimit a := by
-  rw [IsSuccLimit]
+  rw [isSuccLimit_iff]
   have := mem_range_succ_or_isSuccPrelimit a
   tauto
 
@@ -527,7 +534,7 @@ and successor limits. -/
 and predecessor limits. -/]
 noncomputable def isSuccLimitRecOn : motive b :=
   isSuccPrelimitRecOn b succ fun a ha ↦
-    if h : IsMin a then isMin a h else isSuccLimit a (ha.isSuccLimit_of_not_isMin h)
+    if h : IsMin a then isMin a h else isSuccLimit a ⟨h, ha⟩
 
 @[to_dual (attr := simp)]
 theorem isSuccLimitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
@@ -640,7 +647,7 @@ minimal element. -/
 minimal element. -/]
 noncomputable def limitRecOn : motive b :=
   prelimitRecOn b succ fun a ha IH ↦
-    if h : IsMin a then isMin a h else isSuccLimit a (ha.isSuccLimit_of_not_isMin h) IH
+    if h : IsMin a then isMin a h else isSuccLimit a ⟨h, ha⟩ IH
 
 @[to_dual (attr := simp)]
 theorem limitRecOn_isMin (hb : IsMin b) : limitRecOn b isMin succ isSuccLimit = isMin b hb := by