feat: generalize IsLUB.mem_of_not_isSuccPrelimit to LinearOrder (#20502)

Author: vihdzp

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

@@ -124,14 +124,7 @@ lemma exists_eq_ciSup_of_not_isSuccPrelimit'
 @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")]
 alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit'
 
-lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := by
-  obtain rfl | hs' := s.eq_empty_or_nonempty
-  · simp [show x = ⊥ by simpa using hs, isSuccPrelimit_bot] at hx
-  · exact hs.mem_of_nonempty_of_not_isSuccPrelimit hs' hx
-
-@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")]
-alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit
-
+@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2025-01-05")]
 lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) :
     ∃ i, f i = x :=
   hf.mem_of_not_isSuccPrelimit hx
@@ -206,12 +199,7 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i))
 @[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")]
 alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit
 
-lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) : x ∈ s :=
-  hs.sInf_eq ▸ sInf_mem_of_not_isPredPrelimit (hs.sInf_eq ▸ hx)
-
-@[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")]
-alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit
-
+@[deprecated IsGLB.mem_of_not_isPredLimit (since := "2025-01-05")]
 lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) :
     ∃ i, f i = x :=
   hf.mem_of_not_isPredPrelimit hx

Mathlib/Order/SuccPred/Limit.lean

@@ -324,6 +324,29 @@ theorem IsSuccPrelimit.lt_iff_exists_lt (h : IsSuccPrelimit b) : a < b ↔ ∃ c
 theorem IsSuccLimit.lt_iff_exists_lt (h : IsSuccLimit b) : a < b ↔ ∃ c < b, a < c :=
   h.isSuccPrelimit.lt_iff_exists_lt
 
+lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
+    IsSuccPrelimit a := by
+  intro b hb
+  obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
+  obtain rfl := (hb.ge_of_gt hbc).antisymm hca
+  contradiction
+
+lemma _root_.IsLUB.mem_of_not_isSuccPrelimit {s : Set α} (hs : IsLUB s a) (ha : ¬IsSuccPrelimit a) :
+    a ∈ s :=
+  ha.imp_symm hs.isSuccPrelimit_of_not_mem
+
+lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
+    (ha : a ∉ s) : IsSuccLimit a := by
+  refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩
+  obtain ⟨b, hb⟩ := hs'
+  obtain rfl | hb := (hs.1 hb).eq_or_lt
+  · contradiction
+  · exact hb.not_isMin
+
+lemma _root_.IsLUB.mem_of_not_isSuccLimit {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
+    (ha : ¬IsSuccLimit a) : a ∈ s :=
+  ha.imp_symm <| hs.isSuccLimit_of_not_mem hs'
+
 theorem IsSuccPrelimit.isLUB_Iio (ha : IsSuccPrelimit a) : IsLUB (Iio a) a := by
   refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩
   obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc
@@ -634,6 +657,22 @@ theorem IsPredPrelimit.lt_iff_exists_lt (h : IsPredPrelimit b) : b < a ↔ ∃ c
 theorem IsPredLimit.lt_iff_exists_lt (h : IsPredLimit b) : b < a ↔ ∃ c, b < c ∧ c < a :=
   h.dual.lt_iff_exists_lt
 
+lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
+    IsPredPrelimit a := by
+  simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha
+
+lemma _root_.IsGLB.mem_of_not_isPredPrelimit {s : Set α} (hs : IsGLB s a) (ha : ¬IsPredPrelimit a) :
+    a ∈ s :=
+  ha.imp_symm hs.isPredPrelimit_of_not_mem
+
+lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
+    (ha : a ∉ s) : IsPredLimit a := by
+  simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha
+
+lemma _root_.IsGLB.mem_of_not_isPredLimit {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
+    (ha : ¬IsPredLimit a) : a ∈ s :=
+  ha.imp_symm <| hs.isPredLimit_of_not_mem hs'
+
 theorem IsPredPrelimit.isGLB_Ioi (ha : IsPredPrelimit a) : IsGLB (Ioi a) a :=
   ha.dual.isLUB_Iio
 

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -1096,7 +1096,7 @@ lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit
     (hω : ¬ IsSuccPrelimit ω)
     (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω := by
   subst h
-  refine (isLUB_csSup' ?_).exists_of_not_isSuccPrelimit hω
+  suffices BddAbove (range f) from (isLUB_csSup' this).mem_of_not_isSuccPrelimit hω
   contrapose! hω with hf
   rw [iSup, csSup_of_not_bddAbove hf, csSup_empty]
   exact isSuccPrelimit_bot