[Merged by Bors] - feat(Mathlib/Order/SuccPred/Limit): more WithTop lemmas about IsMin/CovBy/IsSuccLimit

Counterexamples/SeparableNotSecondCountable.lean

@@ -48,7 +48,7 @@ instance instSeparableSpace : SeparableSpace (ℝ ×ₗ Bool) := by
 theorem not_secondCountableTopology : ¬SecondCountableTopology (ℝ ×ₗ Bool) := by
   intro h
   have : {x : ℝ ×ₗ Bool | (ofLex x).2}.Countable := by
-    simpa [Prod.Lex.covBy_iff, Bool.covBy_iff, exists_or, not_covBy, (Bool.le_true _).not_gt,
+    simpa [Prod.Lex.covBy_iff, not_covBy_of_denselyOrdered, (Bool.le_true _).not_gt,
       (Bool.false_le _).lt_iff_ne] using countable_setOfPred_covBy_left (α := ℝ ×ₗ Bool)
   refine not_countable_univ <| (this.image fun x ↦ (ofLex x).1).mono fun x _ ↦ ?_
   exact ⟨toLex (x, true), rfl, rfl⟩

Mathlib/MeasureTheory/Measure/Stieltjes.lean

@@ -418,7 +418,8 @@ theorem outer_Ioc [DenselyOrdered R] (a b : R) : f.outer (Ioc a b) = ofReal (f b
       rintro x hx
       simp only [Iotop, htq', ↓reduceIte, mem_Ioc]
       exact ⟨(A hx).1, htq' _⟩
-    have : (𝓝[>] q').NeBot := by simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy]
+    have : (𝓝[>] q').NeBot := by
+      simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy_of_denselyOrdered]
     have : ContinuousWithinAt (fun r => ofReal (f r - f p)) (Ioi q') q' := by
       apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
       refine ContinuousWithinAt.sub ?_ continuousWithinAt_const

Mathlib/Order/Cover.lean

@@ -193,10 +193,14 @@ variable [LT α] {a b : α}
 theorem CovBy.lt (h : a ⋖ b) : a < b :=
   h.1
 
+@[to_dual none]
+theorem not_covBy : ¬a ⋖ b ↔ a < b → ∃ c, a < c ∧ c < b := by
+  simp_rw [CovBy, not_and, not_forall, not_not, exists_prop]
+
 /-- If `a < b`, then `b` does not cover `a` iff there's an element in between. -/
 @[to_dual none]
 theorem not_covBy_iff (h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b := by
-  simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
+  simp_rw [not_covBy, h, true_implies]
 
 @[to_dual none]
 alias ⟨exists_lt_lt_of_not_covBy, _⟩ := not_covBy_iff
@@ -206,12 +210,12 @@ alias LT.lt.exists_lt_lt := exists_lt_lt_of_not_covBy
 
 /-- In a dense order, nothing covers anything. -/
 @[to_dual self]
-theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h =>
+theorem not_covBy_of_denselyOrdered [DenselyOrdered α] : ¬a ⋖ b := fun h =>
   let ⟨_, hc⟩ := exists_between h.1
   h.2 hc.1 hc.2
 
 theorem denselyOrdered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b :=
-  ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h =>
+  ⟨fun h _ _ => @not_covBy_of_denselyOrdered _ _ _ _ h, fun h =>
     ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩
 
 @[to_dual self, simp]
@@ -290,6 +294,10 @@ theorem wcovBy_iff_covBy_or_le_and_le : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b 
 @[to_dual self]
 alias ⟨WCovBy.covBy_or_le_and_le, _⟩ := wcovBy_iff_covBy_or_le_and_le
 
+@[to_dual (attr := simp) wcovBy_bot_iff]
+theorem top_wcovBy_iff [OrderTop α] {a : α} : ⊤ ⩿ a ↔ ⊤ ≤ a := by
+  simp [wcovBy_iff_covBy_or_le_and_le]
+
 theorem AntisymmRel.trans_covBy (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⋖ c) : a ⋖ c :=
   ⟨hab.1.trans_lt hbc.lt, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩
 
@@ -765,27 +773,44 @@ end Pi
 
 namespace WithTop
 
-variable [Preorder α] {a b : α}
+section LT
+
+variable [LT α] {a b : α}
 
 @[to_dual (attr := simp, norm_cast)]
-lemma coe_wcovBy_coe : (a : WithTop α) ⩿ b ↔ a ⩿ b :=
-  Set.OrdConnected.apply_wcovBy_apply_iff WithTop.coeOrderHom <| by
-    simp [WithTop.range_coe, ordConnected_Iio]
+lemma coe_covBy_coe : (a : WithTop α) ⋖ b ↔ a ⋖ b := by
+  simp [CovBy, WithTop.forall]
+
+@[to_dual (attr := simp) not_bot_covBy]
+theorem not_covBy_top [NoMaxOrder α] {a : WithTop α} : ¬ a ⋖ ⊤ := by
+  refine not_covBy.mpr fun ha ↦ ?_
+  obtain ⟨a, rfl⟩ := ne_top_iff_exists.mp <| WithTop.lt_top_iff_ne_top.mp ha
+  have ⟨b, hab⟩ := NoMaxOrder.exists_gt a
+  exact ⟨b, coe_lt_coe.mpr hab, coe_lt_top b⟩
+
+@[to_dual (attr := simp) not_covBy_bot]
+theorem not_top_covBy {a : WithTop α} : ¬⊤ ⋖ a :=
+  mt CovBy.lt a.not_top_lt
+
+end LT
+
+section Preorder
+
+variable [Preorder α] {a b : α}
 
 @[to_dual (attr := simp, norm_cast)]
-lemma coe_covBy_coe : (a : WithTop α) ⋖ b ↔ a ⋖ b :=
-  Set.OrdConnected.apply_covBy_apply_iff WithTop.coeOrderHom <| by
-    simp [WithTop.range_coe, ordConnected_Iio]
+lemma coe_wcovBy_coe : (a : WithTop α) ⩿ b ↔ a ⩿ b := by
+  simp [WCovBy, WithTop.forall]
 
-@[to_dual]
-theorem covBy_top_iff {a : WithTop α} : a ⋖ ⊤ ↔ ∃ b : α, IsMax b ∧ a = b := by
+@[to_dual bot_covBy_iff]
+theorem covBy_top_iff {a : WithTop α} : a ⋖ ⊤ ↔ ∃ b : α, a = b ∧ IsMax b := by
   cases a with
   | coe a => simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]
   | top => simp [CovBy]
 
-@[to_dual (attr := simp)]
-theorem not_covBy_top [NoMaxOrder α] {a : WithTop α} : ¬ a ⋖ ⊤ := by
-  simp [covBy_top_iff]
+@[to_dual bot_wcovBy_iff]
+theorem wcovBy_top_iff {a : WithTop α} : a ⩿ ⊤ ↔ a = ⊤ ∨ ∃ b : α, a = b ∧ IsMax b := by
+  simp [wcovBy_iff_covBy_or_le_and_le, covBy_top_iff, or_comm]
 
 @[to_dual (attr := simp) bot_covBy_coe]
 lemma coe_covBy_top : (a : WithTop α) ⋖ ⊤ ↔ IsMax a := by
@@ -795,6 +820,16 @@ lemma coe_covBy_top : (a : WithTop α) ⋖ ⊤ ↔ IsMax a := by
 lemma coe_wcovBy_top : (a : WithTop α) ⩿ ⊤ ↔ IsMax a := by
   simp only [wcovBy_iff_Ioo_eq, ← image_coe_Ioi, le_top, image_eq_empty, true_and, Ioi_eq_empty_iff]
 
+@[to_dual not_bot_wcovBy]
+theorem not_coe_wcovBy_top [NoMaxOrder α] {a : α} : ¬(a : WithTop α) ⩿ ⊤ := by
+  simp
+
+@[to_dual not_wcovBy_bot]
+theorem not_top_wcovBy_coe {a : α} : ¬⊤ ⩿ (a : WithTop α) := by
+  simp
+
+end Preorder
+
 end WithTop
 
 section WellFounded

Mathlib/Order/SuccPred/Limit.lean

@@ -65,7 +65,8 @@ alias not_isSuccPrelimit_iff_exists_covBy := not_isSuccPrelimit_iff
 alias not_isPredPrelimit_iff_exists_covBy := not_isPredPrelimit_iff
 
 @[to_dual (attr := simp)]
-theorem IsSuccPrelimit.of_dense [DenselyOrdered α] (a : α) : IsSuccPrelimit a := fun _ => not_covBy
+theorem IsSuccPrelimit.of_dense [DenselyOrdered α] (a : α) : IsSuccPrelimit a :=
+  fun _ ↦ not_covBy_of_denselyOrdered
 
 @[to_dual (attr := simp)]
 theorem isSuccPrelimit_toDual_iff : IsSuccPrelimit (toDual a) ↔ IsPredPrelimit a := by
@@ -211,33 +212,41 @@ strictly between `i` and `j`. -/]
 noncomputable def IsSuccPrelimit.mid {i j : α} (hi : IsSuccPrelimit i) (hj : j < i) : Ioo j i :=
   Classical.indefiniteDescription _ ((not_covBy_iff_nonempty_Ioo hj).mp <| hi j)
 
-@[to_dual]
-theorem _root_.WithTop.isSuccPrelimit_iff [NoMaxOrder α] {x : WithTop α} :
-    IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ y : α, x = y ∧ IsSuccPrelimit y := by
-  cases x with
-  | coe x => simp [IsSuccPrelimit, WithTop.forall]
-  | top => simp [IsSuccPrelimit]
+@[to_dual (attr := simp)]
+theorem _root_.WithTop.isSuccPrelimit_coe_iff {α} [LT α] {x : α} :
+    IsSuccPrelimit (x : WithTop α) ↔ IsSuccPrelimit x := by
+  simp [IsSuccPrelimit, WithTop.forall]
 
 @[to_dual]
-theorem IsSuccPrelimit.withTopCoe {x : α} (h : IsSuccPrelimit x) :
-    IsSuccPrelimit (x : WithTop α) := by
-  simpa [IsSuccPrelimit, WithTop.forall]
+alias ⟨_, IsSuccPrelimit.withTopCoe⟩ := WithTop.isSuccPrelimit_coe_iff
 
 @[to_dual (attr := simp)]
-theorem _root_.WithTop.isSuccPrelimit_top [NoMaxOrder α] : IsSuccPrelimit (⊤ : WithTop α) := by
-  simp [WithTop.isSuccPrelimit_iff]
+theorem _root_.WithTop.isSuccPrelimit_top {α} [LT α] [NoMaxOrder α] :
+    IsSuccPrelimit (⊤ : WithTop α) := by
+  intro a ha
+  obtain ⟨a, rfl⟩ := WithTop.ne_top_iff_exists.mp <| WithTop.lt_top_iff_ne_top.mp ha.lt
+  have ⟨b, hab⟩ := NoMaxOrder.exists_gt a
+  exact ha.right (WithTop.coe_lt_coe.mpr hab) (WithTop.coe_lt_top b)
+
+@[to_dual]
+theorem _root_.WithTop.isSuccPrelimit_iff {α} [LT α] [NoMaxOrder α] {x : WithTop α} :
+    IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ y : α, x = y ∧ IsSuccPrelimit y := by
+  cases x with
+  | coe x => simp
+  | top => simp [IsSuccPrelimit]
 
 @[to_dual]
 theorem _root_.WithTop.isSuccLimit_iff [Nonempty α] [NoMaxOrder α] {x : WithTop α} :
     IsSuccLimit x ↔ x = ⊤ ∨ ∃ y : α, x = y ∧ IsSuccLimit y := by
-  cases x with
-  | coe x => simp [Order.isSuccLimit_iff, WithTop.isSuccPrelimit_iff, WithTop.exists]
-  | top => simp [Order.isSuccLimit_iff, WithTop.exists]
+  cases x <;> simp [Order.isSuccLimit_iff]
+
+@[to_dual (attr := simp)]
+theorem _root_.WithTop.isSuccLimit_coe_iff {x : α} :
+    IsSuccLimit (x : WithTop α) ↔ IsSuccLimit x := by
+  simp [isSuccLimit_iff]
 
 @[to_dual]
-theorem IsSuccLimit.withTopCoe {x : α} (h : IsSuccLimit x) :
-    IsSuccLimit (x : WithTop α) := by
-  simpa [isSuccLimit_iff, WithTop.exists, h.isSuccPrelimit.withTopCoe] using h.not_isMin
+alias ⟨_, IsSuccLimit.withTopCoe⟩ := WithTop.isSuccLimit_coe_iff
 
 @[to_dual]
 theorem _root_.WithTop.isSuccLimit_top [Nonempty α] [NoMaxOrder α] :
@@ -251,9 +260,18 @@ theorem _root_.WithTop.isPredPrelimit_iff {x : WithTop α} :
   | coe x => simp [IsPredPrelimit, Order.isPredLimit_iff, WithTop.forall]
   | top => simp
 
+@[to_dual (attr := simp)]
+theorem _root_.WithTop.isPredLimit_coe_iff {x : α} :
+    IsPredLimit (x : WithTop α) ↔ IsPredLimit x := by
+  simp [WithTop.isPredPrelimit_iff, isPredLimit_iff, WithTop.exists]
+
 @[to_dual]
-theorem IsPredLimit.withTopCoe {x : α} (h : IsPredLimit x) : IsPredLimit (x : WithTop α) := by
-  simpa [WithTop.isPredPrelimit_iff, isPredLimit_iff, WithTop.exists] using h
+alias ⟨_, IsPredLimit.withTopCoe⟩ := WithTop.isPredLimit_coe_iff
+
+@[to_dual]
+theorem _root_.WithTop.isPredLimit_iff {x : WithTop α} :
+    IsPredLimit x ↔ ∃ y : α, x = y ∧ IsPredLimit y := by
+  grind [isPredLimit_iff, WithTop.isPredPrelimit_iff, isMax_top, not_isMax_iff, WithTop.coe_lt_top]
 
 variable [SuccOrder α]
 
@@ -456,6 +474,22 @@ alias not_isSuccPrelimit := not_isSuccPrelimit_of_isSuccArchimedean
 @[deprecated (since := "2026-04-19")]
 alias not_isPredPrelimit := not_isPredPrelimit_of_isPredArchimedean
 
+@[to_dual]
+theorem isSuccPrelimit_iff_of_orderBot [OrderBot α] {a : α} : IsSuccPrelimit a ↔ a = ⊥ := by
+  rw [isSuccPrelimit_iff_isMin, isMin_iff_eq_bot]
+
+@[to_dual]
+theorem _root_.WithTop.isSuccPrelimit_iff_of_isSuccArchimedean {α} [Preorder α] [SuccOrder α]
+    [IsSuccArchimedean α] [NoMaxOrder α] {a : WithTop α} : IsSuccPrelimit a ↔ a = ⊤ ∨ IsMin a := by
+  cases isEmpty_or_nonempty α
+  · simp [WithTop.eq_top_of_isEmpty]
+  · simp [WithTop.isSuccPrelimit_iff, WithTop.isMin_iff]
+
+@[to_dual]
+theorem _root_.WithTop.isSuccLimit_iff_of_isSuccArchimedean {α} [Preorder α] [SuccOrder α]
+    [IsSuccArchimedean α] [NoMaxOrder α] [Nonempty α] {a : WithTop α} : IsSuccLimit a ↔ a = ⊤ := by
+  simp [WithTop.isSuccLimit_iff]
+
 end IsSuccArchimedean
 
 end PartialOrder

Mathlib/Order/WithBot.lean

@@ -75,6 +75,12 @@ theorem bot_ne_coe : ⊥ ≠ (a : WithBot α) :=
 theorem coe_ne_bot : (a : WithBot α) ≠ ⊥ :=
   nofun
 
+@[to_dual]
+theorem eq_bot_of_isEmpty [IsEmpty α] {a : WithBot α} : a = ⊥ :=
+  match a with
+  | ⊥ => rfl
+  | (a : α) => IsEmpty.elim ‹_› a
+
 /-- Specialization of `Option.getD` to values in `WithBot α` that respects API boundaries. -/
 @[to_dual
 /-- Specialization of `Option.getD` to values in `WithTop α` that respects API boundaries. -/]
@@ -425,9 +431,23 @@ theorem coe_le_iff : a ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b := by simp [le_if
 @[to_dual coe_le_iff]
 theorem le_coe_iff : x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b := by simp [le_iff_forall]
 
+@[to_dual (attr := simp)]
+theorem isMax_coe_iff : IsMax (a : WithBot α) ↔ IsMax a := by
+  simp [IsMax, WithBot.forall]
+
 @[to_dual]
 protected theorem _root_.IsMax.withBot (h : IsMax a) : IsMax (a : WithBot α) :=
-  fun x ↦ by cases x <;> simp; simpa using @h _
+  isMax_coe_iff.mpr h
+
+@[to_dual (attr := simp)]
+theorem not_isMax_top [Nonempty α] : ¬IsMax (⊥ : WithBot α) := by
+  intro h
+  have ⟨a⟩ := ‹Nonempty α›
+  exact WithBot.not_coe_le_bot a <| h bot_le
+
+@[to_dual]
+theorem isMax_iff [Nonempty α] {x : WithBot α} : IsMax x ↔ ∃ y : α, x = y ∧ IsMax y := by
+  cases x <;> simp
 
 @[to_dual (attr := simp) untop_le_iff]
 lemma le_unbot_iff (hx : x ≠ ⊥) : a ≤ unbot x hx ↔ a ≤ x := by lift x to α using hx; simp