diff --git a/Mathlib.lean b/Mathlib.lean
index 22ed0dfb439f3f..ed746164599cb7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5577,7 +5577,9 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompleteLattice.Finset
 public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover
diff --git a/Mathlib/Order/CompleteLattice/Basic.lean b/Mathlib/Order/CompleteLattice/Basic.lean
index aeb6ddd624ce67..8dee71787136de 100644
--- a/Mathlib/Order/CompleteLattice/Basic.lean
+++ b/Mathlib/Order/CompleteLattice/Basic.lean
@@ -225,7 +225,7 @@ protected theorem Equiv.iSup_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x,
     ⨆ x, f x = ⨆ y, g y :=
   e.surjective.iSup_congr _ h
 
-@[congr]
+@[to_dual (attr := congr)]
 theorem iSup_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
     (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iSup f₁ = iSup f₂ := by
   obtain rfl := propext pq
@@ -241,6 +241,7 @@ theorem iSup_plift_down (f : ι → α) : ⨆ i, f (PLift.down i) = ⨆ i, f i :
 theorem iSup_range' (g : β → α) (f : ι → β) : ⨆ b : range f, g b = ⨆ i, g (f i) := by
   rw [iSup, iSup, ← image_eq_range, ← range_comp']
 
+@[to_dual]
 theorem sSup_image' {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a : s, f a := by
   rw [iSup, image_eq_range]
 
@@ -283,11 +284,6 @@ protected theorem Equiv.iInf_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x,
     ⨅ x, f x = ⨅ y, g y :=
   @Equiv.iSup_congr αᵒᵈ _ _ _ _ _ e h
 
-@[congr]
-theorem iInf_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
-    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iInf f₁ = iInf f₂ :=
-  @iSup_congr_Prop αᵒᵈ _ p q f₁ f₂ pq f
-
 theorem iInf_plift_up (f : PLift ι → α) : ⨅ i, f (PLift.up i) = ⨅ i, f i :=
   (PLift.up_surjective.iInf_congr _) fun _ => rfl
 
@@ -297,9 +293,6 @@ theorem iInf_plift_down (f : ι → α) : ⨅ i, f (PLift.down i) = ⨅ i, f i :
 theorem iInf_range' (g : β → α) (f : ι → β) : ⨅ b : range f, g b = ⨅ i, g (f i) :=
   @iSup_range' αᵒᵈ _ _ _ _ _
 
-theorem sInf_image' {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a : s, f a :=
-  @sSup_image' αᵒᵈ _ _ _ _
-
 end InfSet
 
 section
@@ -1034,13 +1027,10 @@ end le
 ### `iSup` and `iInf` under `Type`
 -/
 
-
+@[to_dual iInf_of_isEmpty]
 theorem iSup_of_empty' {α ι} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup (∅ : Set α) :=
   congr_arg sSup (range_eq_empty f)
 
-theorem iInf_of_isEmpty {α ι} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf (∅ : Set α) :=
-  congr_arg sInf (range_eq_empty f)
-
 theorem iSup_of_empty [IsEmpty ι] (f : ι → α) : iSup f = ⊥ :=
   (iSup_of_empty' f).trans sSup_empty
 
diff --git a/Mathlib/Order/CompletePartialOrder.lean b/Mathlib/Order/CompletePartialOrder.lean
index 454422dcee76f6..cbd2c57ab8b005 100644
--- a/Mathlib/Order/CompletePartialOrder.lean
+++ b/Mathlib/Order/CompletePartialOrder.lean
@@ -6,6 +6,7 @@ Authors: Christopher Hoskin
 module
 
 public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 
 /-!
 # Complete Partial Orders
@@ -75,14 +76,20 @@ lemma CompletePartialOrder.scottContinuous {f : α → β} :
 open OmegaCompletePartialOrder
 
 /-- A complete partial order is an ω-complete partial order. -/
-instance CompletePartialOrder.toOmegaCompletePartialOrder : OmegaCompletePartialOrder α where
+instance (priority := 100) CompletePartialOrder.toOmegaCompletePartialOrder :
+    OmegaCompletePartialOrder α where
   ωSup c := ⨆ n, c n
   le_ωSup c := c.directed.le_iSup
   ωSup_le c _ := c.directed.iSup_le
 
+/-- A complete partial order is an conditionally complete partial order. -/
+instance (priority := 100) [CompletePartialOrder α] : ConditionallyCompletePartialOrderSup α where
+  isLUB_csSup_of_directed _ h_dir _ _ := h_dir.isLUB_sSup
+
 end CompletePartialOrder
 
 /-- A complete lattice is a complete partial order. -/
-instance CompleteLattice.toCompletePartialOrder [CompleteLattice α] : CompletePartialOrder α where
+instance (priority := 100) CompleteLattice.toCompletePartialOrder [CompleteLattice α] :
+    CompletePartialOrder α where
   sSup := sSup
   lubOfDirected _ _ := isLUB_sSup _
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
index 67987d5447714b..3c1dea47e10fc1 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Set.Lattice
 public import Mathlib.Order.ConditionallyCompleteLattice.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
 
 /-!
 # Theory of conditionally complete lattices
@@ -224,22 +225,13 @@ theorem isGLB_csInf (ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s) :=
 theorem IsLUB.csSup_eq (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a :=
   (isLUB_csSup ne ⟨a, H.1⟩).unique H
 
-/-- A greatest element of a set is the supremum of this set. -/
-theorem IsGreatest.csSup_eq (H : IsGreatest s a) : sSup s = a :=
-  H.isLUB.csSup_eq H.nonempty
-
-theorem IsGreatest.csSup_mem (H : IsGreatest s a) : sSup s ∈ s :=
-  H.csSup_eq.symm ▸ H.1
-
 theorem IsGLB.csInf_eq (H : IsGLB s a) (ne : s.Nonempty) : sInf s = a :=
   (isGLB_csInf ne ⟨a, H.1⟩).unique H
 
-/-- A least element of a set is the infimum of this set. -/
-theorem IsLeast.csInf_eq (H : IsLeast s a) : sInf s = a :=
-  H.isGLB.csInf_eq H.nonempty
-
-theorem IsLeast.csInf_mem (H : IsLeast s a) : sInf s ∈ s :=
-  H.csInf_eq.symm ▸ H.1
+instance (priority := 100) ConditionallyCompleteLattice.toConditionallyCompletePartialOrder :
+    ConditionallyCompletePartialOrder α where
+  isGLB_csInf_of_directed _ _ non bdd := isGLB_csInf non bdd
+  isLUB_csSup_of_directed _ _ non bdd := isLUB_csSup non bdd
 
 theorem subset_Icc_csInf_csSup (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Icc (sInf s) (sSup s) :=
   fun _ hx => ⟨csInf_le hb hx, le_csSup ha hx⟩
@@ -310,16 +302,6 @@ theorem exists_between_of_forall_le (sne : s.Nonempty) (tne : t.Nonempty)
     (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : (upperBounds s ∩ lowerBounds t).Nonempty :=
   ⟨sInf t, fun x hx => le_csInf tne <| hst x hx, fun _ hy => csInf_le (sne.mono hst) hy⟩
 
-/-- The supremum of a singleton is the element of the singleton -/
-@[simp]
-theorem csSup_singleton (a : α) : sSup {a} = a :=
-  isGreatest_singleton.csSup_eq
-
-/-- The infimum of a singleton is the element of the singleton -/
-@[simp]
-theorem csInf_singleton (a : α) : sInf {a} = a :=
-  isLeast_singleton.csInf_eq
-
 theorem csSup_pair (a b : α) : sSup {a, b} = a ⊔ b :=
   (@isLUB_pair _ _ a b).csSup_eq (insert_nonempty _ _)
 
@@ -367,18 +349,6 @@ nonempty and bounded below. -/
 theorem csInf_insert (hs : BddBelow s) (sne : s.Nonempty) : sInf (insert a s) = a ⊓ sInf s :=
   csSup_insert (α := αᵒᵈ) hs sne
 
-@[simp]
-theorem csInf_Icc (h : a ≤ b) : sInf (Icc a b) = a :=
-  (isGLB_Icc h).csInf_eq (nonempty_Icc.2 h)
-
-@[simp]
-theorem csInf_Ici : sInf (Ici a) = a :=
-  isLeast_Ici.csInf_eq
-
-@[simp]
-theorem csInf_Ico (h : a < b) : sInf (Ico a b) = a :=
-  (isGLB_Ico h).csInf_eq (nonempty_Ico.2 h)
-
 @[simp]
 theorem csInf_Ioc [DenselyOrdered α] (h : a < b) : sInf (Ioc a b) = a :=
   (isGLB_Ioc h).csInf_eq (nonempty_Ioc.2 h)
@@ -392,27 +362,15 @@ theorem csInf_Ioi [NoMaxOrder α] [DenselyOrdered α] : sInf (Ioi a) = a :=
 theorem csInf_Ioo [DenselyOrdered α] (h : a < b) : sInf (Ioo a b) = a :=
   (isGLB_Ioo h).csInf_eq (nonempty_Ioo.2 h)
 
-@[simp]
-theorem csSup_Icc (h : a ≤ b) : sSup (Icc a b) = b :=
-  (isLUB_Icc h).csSup_eq (nonempty_Icc.2 h)
-
 @[simp]
 theorem csSup_Ico [DenselyOrdered α] (h : a < b) : sSup (Ico a b) = b :=
   (isLUB_Ico h).csSup_eq (nonempty_Ico.2 h)
 
-@[simp]
-theorem csSup_Iic : sSup (Iic a) = a :=
-  isGreatest_Iic.csSup_eq
-
 @[simp]
 theorem csSup_Iio [NoMinOrder α] [DenselyOrdered α] : sSup (Iio a) = a :=
   csSup_eq_of_forall_le_of_forall_lt_exists_gt nonempty_Iio (fun _ => le_of_lt) fun w hw => by
     simpa [and_comm] using exists_between hw
 
-@[simp]
-theorem csSup_Ioc (h : a < b) : sSup (Ioc a b) = b :=
-  (isLUB_Ioc h).csSup_eq (nonempty_Ioc.2 h)
-
 @[simp]
 theorem csSup_Ioo [DenselyOrdered α] (h : a < b) : sSup (Ioo a b) = b :=
   (isLUB_Ioo h).csSup_eq (nonempty_Ioo.2 h)
@@ -424,12 +382,6 @@ theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge (hs : s.Nonempty) (h_is_ub
     (h_b_le_ub : ∀ ub, (∀ a ∈ s, a ≤ ub) → b ≤ ub) : sSup s = b :=
   (csSup_le hs h_is_ub).antisymm ((h_b_le_ub _) fun _ => le_csSup ⟨b, h_is_ub⟩)
 
-lemma sup_eq_top_of_top_mem [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤ :=
-  top_unique <| le_csSup (OrderTop.bddAbove s) h
-
-lemma inf_eq_bot_of_bot_mem [OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥ :=
-  bot_unique <| csInf_le (OrderBot.bddBelow s) h
-
 end ConditionallyCompleteLattice
 
 instance Pi.conditionallyCompleteLattice {ι : Type*} {α : ι → Type*}
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
index d075eca456a24d..e6fb441f2ae436 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
@@ -6,6 +6,7 @@ Authors: Sébastian Gouëzel
 module
 
 public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 
 /-!
 # Indexed sup / inf in conditionally complete lattices
@@ -181,68 +182,6 @@ lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf
     ⨅ i, f i ≤ ⨆ i, f i :=
   (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)
 
-@[simp]
-theorem ciSup_const [hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a := by
-  rw [iSup, range_const, csSup_singleton]
-
-@[simp]
-theorem ciInf_const [Nonempty ι] {a : α} : ⨅ _ : ι, a = a :=
-  ciSup_const (α := αᵒᵈ)
-
-@[simp]
-theorem ciSup_unique [Unique ι] {s : ι → α} : ⨆ i, s i = s default := by
-  have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
-  simp only [this, ciSup_const]
-
-@[simp]
-theorem ciInf_unique [Unique ι] {s : ι → α} : ⨅ i, s i = s default :=
-  ciSup_unique (α := αᵒᵈ)
-
-theorem ciSup_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨆ i, s i = s i :=
-  @ciSup_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _
-
-theorem ciInf_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨅ i, s i = s i :=
-  @ciInf_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _
-
-theorem ciSup_pos {p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp := by
-  simp [hp]
-
-theorem ciInf_pos {p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp := by
-  simp [hp]
-
-lemma ciSup_neg {p : Prop} {f : p → α} (hp : ¬ p) :
-    ⨆ (h : p), f h = sSup (∅ : Set α) := by
-  rw [iSup]
-  congr
-  rwa [range_eq_empty_iff, isEmpty_Prop]
-
-lemma ciInf_neg {p : Prop} {f : p → α} (hp : ¬ p) :
-    ⨅ (h : p), f h = sInf (∅ : Set α) :=
-  ciSup_neg (α := αᵒᵈ) hp
-
-lemma ciSup_eq_ite {p : Prop} [Decidable p] {f : p → α} :
-    (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α) := by
-  by_cases H : p <;> simp [ciSup_neg, H]
-
-lemma ciInf_eq_ite {p : Prop} [Decidable p] {f : p → α} :
-    (⨅ h : p, f h) = if h : p then f h else sInf (∅ : Set α) :=
-  ciSup_eq_ite (α := αᵒᵈ)
-
-theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
-    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f := by
-  simp only [hp, ciSup_unique]
-  simp only [iSup]
-  congr
-  apply Subset.antisymm
-  · rintro - ⟨i, rfl⟩
-    simp
-  · rintro - ⟨i, rfl⟩
-    simp
-
-theorem cbiInf_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
-    ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f :=
-  cbiSup_eq_of_forall (α := αᵒᵈ) hp
-
 /-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
 is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
 See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
@@ -258,24 +197,6 @@ theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → 
     (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b :=
   ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂
 
-/-- **Nested intervals lemma**: if `f` is a monotone sequence, `g` is an antitone sequence, and
-`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
-theorem Monotone.ciSup_mem_iInter_Icc_of_antitone [SemilatticeSup β] {f g : β → α} (hf : Monotone f)
-    (hg : Antitone g) (h : f ≤ g) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) := by
-  refine mem_iInter.2 fun n => ?_
-  haveI : Nonempty β := ⟨n⟩
-  have : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
-  exact ⟨le_ciSup ⟨g <| n, forall_mem_range.2 this⟩ _, ciSup_le this⟩
-
-/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
-closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
-theorem ciSup_mem_iInter_Icc_of_antitone_Icc [SemilatticeSup β] {f g : β → α}
-    (h : Antitone fun n => Icc (f n) (g n)) (h' : ∀ n, f n ≤ g n) :
-    (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
-  Monotone.ciSup_mem_iInter_Icc_of_antitone
-    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
-    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'
-
 lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
     Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by
   ext
@@ -285,22 +206,6 @@ lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
     Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
   Iic_ciInf (α := αᵒᵈ) hf
 
-theorem ciSup_Iic [Preorder β] {f : β → α} (a : β) (hf : Monotone f) :
-    ⨆ x : Iic a, f x = f a := by
-  have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
-  apply (le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
-  rw [ciSup_le_iff H]
-  rintro ⟨a, h⟩
-  exact hf h
-
-theorem ciInf_Ici [Preorder β] {f : β → α} (a : β) (hf : Monotone f) :
-    ⨅ x : Ici a, f x = f a := by
-  have H : BddBelow (range fun x : Ici a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
-  apply (ciInf_le H (⟨a, le_refl a⟩ : Ici a)).antisymm
-  rw [le_ciInf_iff H]
-  rintro ⟨a, h⟩
-  exact hf h
-
 theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
     (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
     iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
diff --git a/Mathlib/Order/ConditionallyCompletePartialOrder/Basic.lean b/Mathlib/Order/ConditionallyCompletePartialOrder/Basic.lean
new file mode 100644
index 00000000000000..754ad72fe9ac02
--- /dev/null
+++ b/Mathlib/Order/ConditionallyCompletePartialOrder/Basic.lean
@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Order.CompleteLattice.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
+
+import Mathlib.Data.Set.Lattice
+
+/-! # Basic results on conditionally complete partial orders
+
+This file contains some basic results on conditionally complete partial orders, and is intended
+to parallel the API for conditionally complete lattices where possible. For the reason, the
+theorems here are mostly protected within the `DirectedOn` namespace, unless such an assumption is
+unnecessary. Otherwise the names here share the same names as their counterparts in
+`Mathlib/Order/ConditionallyCompleteLattice/Basic.lean`.
+
+-/
+@[expose] public section
+
+-- Guard against import creep
+assert_not_exists Multiset
+
+open Function OrderDual Set
+
+variable {α β γ : Type*} {ι : Sort*}
+
+namespace OrderDual
+
+instance [ConditionallyCompletePartialOrderSup α] :
+    ConditionallyCompletePartialOrderInf αᵒᵈ where
+  isGLB_csInf_of_directed _ h_dir h_non h_bdd := h_dir.isLUB_csSup (α := α) h_non h_bdd
+
+instance [ConditionallyCompletePartialOrderInf α] :
+    ConditionallyCompletePartialOrderSup αᵒᵈ where
+  isLUB_csSup_of_directed _ h_dir h_non h_bdd := h_dir.isGLB_csInf (α := α) h_non h_bdd
+
+instance [ConditionallyCompletePartialOrder α] :
+    ConditionallyCompletePartialOrder αᵒᵈ where
+
+end OrderDual
+
+section ConditionallyCompletePartialOrderSup
+
+variable [ConditionallyCompletePartialOrderSup α] {s t : Set α} {a b : α}
+
+@[to_dual csInf_le_of_le]
+protected theorem DirectedOn.le_csSup_of_le (hd : DirectedOn (· ≤ ·) s)
+    (hs : BddAbove s) (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s :=
+  le_trans h (hd.le_csSup hs hb)
+
+@[to_dual (attr := gcongr low)]
+protected theorem DirectedOn.csSup_le_csSup (hds : DirectedOn (· ≤ ·) s)
+    (hdt : DirectedOn (· ≤ ·) t) (ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) :
+    sSup s ≤ sSup t :=
+  hds.csSup_le hs fun _ ha => hdt.le_csSup ht (h ha)
+
+@[to_dual csInf_le_iff]
+protected theorem DirectedOn.le_csSup_iff (hd : DirectedOn (· ≤ ·) s) (h : BddAbove s)
+    (hs : s.Nonempty) : a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b :=
+  ⟨fun h _ hb => le_trans h (hd.csSup_le hs hb), fun hb => hb _ fun _ => hd.le_csSup h⟩
+
+@[to_dual]
+theorem IsGreatest.directedOn (H : IsGreatest s a) : DirectedOn (· ≤ ·) s :=
+  fun _ h₁ _ h₂ ↦ ⟨a, H.1, H.2 h₁, H.2 h₂⟩
+
+/-- A greatest element of a set is the supremum of this set. -/
+@[to_dual /-- A least element of a set is the infimum of this set. -/]
+theorem IsGreatest.csSup_eq (H : IsGreatest s a) : sSup s = a :=
+  H.directedOn.isLUB_csSup H.nonempty ⟨a, H.2⟩ |>.unique H.isLUB
+
+@[to_dual]
+theorem IsGreatest.csSup_mem (H : IsGreatest s a) : sSup s ∈ s :=
+  H.csSup_eq.symm ▸ H.1
+
+@[to_dual le_csInf_iff]
+protected theorem DirectedOn.csSup_le_iff (hd : DirectedOn (· ≤ ·) s)
+    (hb : BddAbove s) (hs : s.Nonempty) : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a :=
+  isLUB_le_iff (hd.isLUB_csSup hs hb)
+
+@[to_dual notMem_of_lt_csInf]
+protected theorem DirectedOn.notMem_of_csSup_lt {x : α} {s : Set α} (hd : DirectedOn (· ≤ ·) s)
+    (h : sSup s < x) (hs : BddAbove s) : x ∉ s :=
+  fun hx ↦ lt_irrefl _ <| (hd.le_csSup hs hx).trans_lt h
+
+/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
+is larger than all elements of `s`, and that this is not the case of any `w<b`.
+See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
+@[to_dual DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt
+/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
+is smaller than all elements of `s`, and that this is not the case of any `w>b`.
+See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/ ]
+protected theorem DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt
+    (hd : DirectedOn (· ≤ ·) s) (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b)
+    (H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b :=
+  (eq_of_le_of_not_lt (hd.csSup_le hs H)) fun hb =>
+    let ⟨_, ha, ha'⟩ := H' _ hb
+    lt_irrefl _ <| ha'.trans_le <| hd.le_csSup ⟨b, H⟩ ha
+
+/-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
+This is essentially an iff, except that the assumptions for the two implications are
+slightly different (one needs boundedness above for one direction, nonemptiness and linear
+order for the other one), so we formulate separately the two implications, contrary to
+the `CompleteLattice` case. -/
+@[to_dual DirectedOn.csInf_lt_of_lt
+/-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when `s` is bounded below.
+This is essentially an iff, except that the assumptions for the two implications are
+slightly different (one needs boundedness below for one direction, nonemptiness and linear
+order for the other one), so we formulate separately the two implications, contrary to
+the `CompleteLattice` case. -/ ]
+protected theorem DirectedOn.lt_csSup_of_lt (hd : DirectedOn (· ≤ ·) s) (hs : BddAbove s)
+    (ha : a ∈ s) (h : b < a) : b < sSup s :=
+  lt_of_lt_of_le h (hd.le_csSup hs ha)
+
+/-- The supremum of a singleton is the element of the singleton -/
+@[to_dual (attr := simp)]
+theorem csSup_singleton (a : α) : sSup {a} = a :=
+  isGreatest_singleton.csSup_eq
+
+@[simp]
+theorem csInf_Ici {α : Type*} [ConditionallyCompletePartialOrderInf α] {a : α} :
+    sInf (Ici a) = a :=
+  isLeast_Ici.csInf_eq
+
+@[simp]
+theorem csInf_Ico {α : Type*} [ConditionallyCompletePartialOrderInf α] {a b : α} (h : a < b) :
+    sInf (Ico a b) = a :=
+  (isLeast_Ico h).csInf_eq
+
+@[simp]
+theorem csInf_Icc {α : Type*} [ConditionallyCompletePartialOrderInf α] {a b : α}
+    (h : a ≤ b) : sInf (Icc a b) = a :=
+  (isLeast_Icc h).csInf_eq
+
+@[to_dual existing, simp]
+theorem csSup_Iic : sSup (Iic a) = a :=
+  isGreatest_Iic.csSup_eq
+
+@[to_dual existing, simp]
+theorem csSup_Ioc (h : a < b) : sSup (Ioc a b) = b :=
+  (isGreatest_Ioc h).csSup_eq
+
+@[simp]
+theorem csSup_Icc {a b : α} (h : a ≤ b) : sSup (Icc a b) = b :=
+  (isGreatest_Icc h).csSup_eq
+
+@[to_dual]
+lemma sup_eq_top_of_top_mem [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤ :=
+  IsGreatest.csSup_eq ⟨h, fun _ _ ↦ le_top⟩
+
+end ConditionallyCompletePartialOrderSup
+
+section ConditionallyCompletePartialOrder
+
+variable [ConditionallyCompletePartialOrder α] {s t : Set α} {a b : α}
+
+protected theorem DirectedOn.subset_Icc_csInf_csSup (hdb : DirectedOn (· ≥ ·) s)
+    (hda : DirectedOn (· ≤ ·) s) (hb : BddBelow s) (ha : BddAbove s) :
+    s ⊆ Icc (sInf s) (sSup s) :=
+  fun _ hx => ⟨hdb.csInf_le hb hx, hda.le_csSup ha hx⟩
+
+/-- If a set is bounded below and above, and nonempty, its infimum is less than or equal to
+its supremum. -/
+protected theorem DirectedOn.csInf_le_csSup (hdb : DirectedOn (· ≥ ·) s)
+    (hda : DirectedOn (· ≤ ·) s) (hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) :
+    sInf s ≤ sSup s :=
+  isGLB_le_isLUB (hdb.isGLB_csInf ne hb) (hda.isLUB_csSup ne ha) ne
+
+end ConditionallyCompletePartialOrder
diff --git a/Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean b/Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean
new file mode 100644
index 00000000000000..3edc2423172fa3
--- /dev/null
+++ b/Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean
@@ -0,0 +1,294 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
+public import Mathlib.Order.GaloisConnection.Basic
+
+/-!
+# Indexed sup / inf in conditionally complete lattices
+
+This file proves lemmas about `iSup` and `iInf` for functions valued in a conditionally complete
+partial order, as opposed to a conditionally complete lattice.
+
+## TODO
+
++ Use `@[to_dual]` in the `GaloisConnection` and `OrderIso` sections.
+
+-/
+
+public section
+
+-- Guard against import creep
+assert_not_exists Multiset
+
+open Function OrderDual Set
+
+variable {α β γ : Type*} {ι : Sort*}
+
+section ConditionallyCompletePartialOrderSup
+
+variable [ConditionallyCompletePartialOrderSup α] {a b : α}
+
+@[to_dual]
+theorem Directed.isLUB_ciSup [Nonempty ι] {f : ι → α} (hd : Directed (· ≤ ·) f)
+    (H : BddAbove (range f)) : IsLUB (range f) (⨆ i, f i) :=
+  hd.directedOn_range.isLUB_csSup (range_nonempty f) H
+
+@[to_dual]
+theorem DirectedOn.isLUB_ciSup_set {f : β → α} {s : Set β} (hd : DirectedOn (· ≤ ·) (f '' s))
+    (H : BddAbove (f '' s)) (Hne : s.Nonempty) :
+    IsLUB (f '' s) (⨆ i : s, f i) := by
+  rw [← sSup_image']
+  exact hd.isLUB_csSup (Hne.image _) H
+
+@[to_dual Directed.le_ciInf_iff]
+theorem Directed.ciSup_le_iff [Nonempty ι] {f : ι → α} {a : α}
+    (hd : Directed (· ≤ ·) f) (hf : BddAbove (range f)) :
+    iSup f ≤ a ↔ ∀ i, f i ≤ a :=
+  (isLUB_le_iff <| hd.isLUB_ciSup hf).trans forall_mem_range
+
+@[to_dual DirectedOn.le_ciInf_set_iff]
+theorem DirectedOn.ciSup_set_le_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
+    (hd : DirectedOn (· ≤ ·) (f '' s)) (hf : BddAbove (f '' s)) :
+    ⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a :=
+  (isLUB_le_iff <| hd.isLUB_ciSup_set hf hs).trans forall_mem_image
+
+@[to_dual Directed.ciInf_le_of_le]
+theorem Directed.le_ciSup_of_le {f : ι → α} (hd : Directed (· ≤ ·) f)
+    (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f :=
+  le_trans h (hd.le_ciSup H c)
+
+/-- The indexed suprema of two functions are comparable if the functions are pointwise comparable -/
+@[to_dual (attr := gcongr low)
+/-- The indexed infimum of two functions are comparable if the functions are pointwise
+comparable -/]
+theorem Directed.ciSup_mono {f g : ι → α} (hdf : Directed (· ≤ ·) f)
+    (hdg : Directed (· ≤ ·) g) (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) :
+    iSup f ≤ iSup g := by
+  cases isEmpty_or_nonempty ι
+  · rw [iSup_of_empty', iSup_of_empty']
+  · exact hdf.ciSup_le fun x ↦ hdg.le_ciSup_of_le B x (H x)
+
+@[to_dual DirectedOn.ciInf_set_le]
+theorem DirectedOn.le_ciSup_set {f : β → α} {s : Set β} (hd : DirectedOn (· ≤ ·) (f '' s))
+    (H : BddAbove (f '' s)) {c : β} (hc : c ∈ s) : f c ≤ ⨆ i : s, f i :=
+  (hd.le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image'
+
+@[to_dual (attr := simp)]
+theorem ciSup_const [hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a := by
+  rw [iSup, range_const, csSup_singleton]
+
+@[to_dual (attr := simp)]
+theorem ciSup_unique [Unique ι] {s : ι → α} : ⨆ i, s i = s default := by
+  have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
+  simp only [this, ciSup_const]
+
+@[to_dual]
+theorem ciSup_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨆ i, s i = s i :=
+  @ciSup_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _
+
+@[to_dual]
+theorem ciSup_pos {p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp := by
+  simp [hp]
+
+@[to_dual]
+lemma ciSup_neg {p : Prop} {f : p → α} (hp : ¬ p) :
+    ⨆ (h : p), f h = sSup (∅ : Set α) := by
+  rw [iSup]
+  congr
+  rwa [range_eq_empty_iff, isEmpty_Prop]
+
+@[to_dual]
+lemma ciSup_eq_ite {p : Prop} [Decidable p] {f : p → α} :
+    (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α) := by
+  by_cases H : p <;> simp [ciSup_neg, H]
+
+@[to_dual]
+theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
+    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f := by
+  simp only [hp, ciSup_unique]
+  simp only [iSup]
+  congr
+  apply Subset.antisymm
+  · rintro - ⟨i, rfl⟩
+    simp
+  · rintro - ⟨i, rfl⟩
+    simp
+
+/-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
+is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
+See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
+@[to_dual Directed.ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
+/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b`
+is smaller than `f i` for all `i`, and that this is not the case of any `w>b`.
+See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/]
+theorem Directed.ciSup_eq_of_forall_le_of_forall_lt_exists_gt [Nonempty ι] {f : ι → α}
+    (hd : Directed (· ≤ ·) f) (h₁ : ∀ i, f i ≤ b) (h₂ : ∀ w, w < b → ∃ i, w < f i) :
+    ⨆ i : ι, f i = b :=
+  hd.directedOn_range.csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f)
+    (forall_mem_range.mpr h₁) fun w hw => exists_range_iff.mpr <| h₂ w hw
+
+/-- **Nested intervals lemma**: if `f` is a monotone sequence, `g` is an antitone sequence, and
+`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
+theorem Monotone.ciSup_mem_iInter_Icc_of_antitone [Preorder β] [IsDirectedOrder β]
+    {f g : β → α} (hf : Monotone f) (hg : Antitone g) (h : f ≤ g) :
+    (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) := by
+  refine mem_iInter.2 fun n => ?_
+  haveI : Nonempty β := ⟨n⟩
+  have h₁ : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
+  have h₂ : Directed (· ≤ ·) f := hf.directed_le
+  exact ⟨h₂.le_ciSup ⟨g <| n, forall_mem_range.2 h₁⟩ _, h₂.ciSup_le h₁⟩
+
+/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
+closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
+theorem ciSup_mem_iInter_Icc_of_antitone_Icc [Preorder β] [IsDirectedOrder β] {f g : β → α}
+    (h : Antitone fun n => Icc (f n) (g n)) (h' : ∀ n, f n ≤ g n) :
+    (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
+  Monotone.ciSup_mem_iInter_Icc_of_antitone
+    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
+    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'
+
+@[to_dual]
+lemma Directed.Ici_ciSup [Nonempty ι] {f : ι → α} (hd : Directed (· ≤ ·) f)
+    (hf : BddAbove (range f)) : Ici (⨆ i, f i) = ⋂ i, Ici (f i) := by
+  ext
+  simpa using hd.ciSup_le_iff hf
+
+@[to_dual]
+theorem ciSup_Iic [Preorder β] {f : β → α} (a : β) (hf : Monotone f) :
+    ⨆ x : Iic a, f x = f a := by
+  have hd : Directed (· ≤ ·) (fun x : Iic a ↦ f x) := fun x y ↦ ⟨⟨a, le_refl a⟩, ⟨hf x.2, hf y.2⟩⟩
+  have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
+  apply (hd.le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
+  rw [hd.ciSup_le_iff H]
+  rintro ⟨a, h⟩
+  exact hf h
+
+end ConditionallyCompletePartialOrderSup
+
+lemma Directed.ciInf_le_ciSup [ConditionallyCompletePartialOrder α] [Nonempty ι] {f : ι → α}
+    (hd : Directed (· ≥ ·) f) (hf : BddBelow (range f))
+    (hd' : Directed (· ≤ ·) f) (hf' : BddAbove (range f)) :
+    ⨅ i, f i ≤ ⨆ i, f i :=
+  (hd.ciInf_le hf (Classical.arbitrary _)).trans <| hd'.le_ciSup hf' (Classical.arbitrary _)
+
+namespace GaloisConnection
+
+section Sup
+
+variable [ConditionallyCompletePartialOrderSup α] [ConditionallyCompletePartialOrderSup β]
+    [Nonempty ι] {l : α → β} {u : β → α}
+
+theorem l_csSup_of_directedOn' (gc : GaloisConnection l u) {s : Set α}
+    (hd : DirectedOn (· ≤ ·) s) (hne : s.Nonempty) (hbdd : BddAbove s) :
+    l (sSup s) = sSup (l '' s) :=
+  gc.isLUB_l_image (hd.isLUB_csSup hne hbdd) |>.unique <|
+    (hd.mono_comp gc.monotone_l).isLUB_csSup (hne.image l) (gc.monotone_l.map_bddAbove hbdd)
+
+theorem l_csSup_of_directedOn (gc : GaloisConnection l u) {s : Set α} (hd : DirectedOn (· ≤ ·) s)
+    (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = ⨆ x : s, l x := by
+  simpa only [← comp_def, ← sSup_range, range_comp, Subtype.range_coe_subtype, setOf_mem_eq]
+    using gc.l_csSup_of_directedOn' hd hne hbdd
+
+theorem l_ciSup_of_directed (gc : GaloisConnection l u) {f : ι → α} (hd : Directed (· ≤ ·) f)
+    (hf : BddAbove (range f)) : l (⨆ i, f i) = ⨆ i, l (f i) := by
+  rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']
+
+theorem l_ciSup_set_of_directedOn (gc : GaloisConnection l u) {s : Set γ} {f : γ → α}
+    (hd : DirectedOn (· ≤ ·) (f '' s)) (hf : BddAbove (f '' s))
+    (hne : s.Nonempty) : l (⨆ i : s, f i) = ⨆ i : s, l (f i) := by
+  haveI := hne.to_subtype
+  rw [image_eq_range] at hf
+  refine gc.l_ciSup_of_directed ?_ hf
+  simpa [directedOn_range, ← comp_def, range_comp]
+
+end Sup
+
+section Inf
+
+variable [ConditionallyCompletePartialOrderInf α] [ConditionallyCompletePartialOrderInf β]
+    [Nonempty ι] {l : α → β} {u : β → α}
+
+theorem u_csInf_of_directedOn (gc : GaloisConnection l u) {s : Set β} (hd : DirectedOn (· ≥ ·) s)
+    (hne : s.Nonempty) (hbdd : BddBelow s) :
+    u (sInf s) = ⨅ x : s, u x :=
+  gc.dual.l_csSup_of_directedOn hd hne hbdd
+
+theorem u_csInf_of_directedOn' (gc : GaloisConnection l u) {s : Set β} (hd : DirectedOn (· ≥ ·) s)
+    (hne : s.Nonempty) (hbdd : BddBelow s) :
+    u (sInf s) = sInf (u '' s) :=
+  gc.dual.l_csSup_of_directedOn' hd hne hbdd
+
+theorem u_ciInf_of_directed (gc : GaloisConnection l u) {f : ι → β} (hd : Directed (· ≥ ·) f)
+    (hf : BddBelow (range f)) :
+    u (⨅ i, f i) = ⨅ i, u (f i) :=
+  gc.dual.l_ciSup_of_directed hd hf
+
+theorem u_ciInf_set_of_directedOn (gc : GaloisConnection l u) {s : Set γ} {f : γ → β}
+    (hd : DirectedOn (· ≥ ·) (f '' s)) (hf : BddBelow (f '' s))
+    (hne : s.Nonempty) : u (⨅ i : s, f i) = ⨅ i : s, u (f i) :=
+  gc.dual.l_ciSup_set_of_directedOn hd hf hne
+
+end Inf
+
+end GaloisConnection
+
+namespace OrderIso
+
+section Sup
+
+variable [ConditionallyCompletePartialOrderSup α] [ConditionallyCompletePartialOrderSup β]
+  [Nonempty ι]
+
+-- these need to have `directed` in their names.
+theorem map_csSup_of_directedOn (e : α ≃o β) {s : Set α} (hd : DirectedOn (· ≤ ·) s)
+    (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = ⨆ x : s, e x :=
+  e.to_galoisConnection.l_csSup_of_directedOn hd hne hbdd
+
+theorem map_csSup_of_directedOn' (e : α ≃o β) {s : Set α} (hd : DirectedOn (· ≤ ·) s)
+    (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = sSup (e '' s) :=
+  e.to_galoisConnection.l_csSup_of_directedOn' hd hne hbdd
+
+theorem map_ciSup_of_directed (e : α ≃o β) {f : ι → α} (hd : Directed (· ≤ ·) f)
+    (hf : BddAbove (range f)) : e (⨆ i, f i) = ⨆ i, e (f i) :=
+  e.to_galoisConnection.l_ciSup_of_directed hd hf
+
+theorem map_ciSup_set_of_directedOn (e : α ≃o β) {s : Set γ} {f : γ → α}
+    (hd : DirectedOn (· ≤ ·) (f '' s)) (hf : BddAbove (f '' s)) (hne : s.Nonempty) :
+    e (⨆ i : s, f i) = ⨆ i : s, e (f i) :=
+  e.to_galoisConnection.l_ciSup_set_of_directedOn hd hf hne
+
+end Sup
+
+section Inf
+
+variable [ConditionallyCompletePartialOrderInf α] [ConditionallyCompletePartialOrderInf β]
+  [Nonempty ι]
+
+theorem map_csInf_of_directedOn (e : α ≃o β) {s : Set α} (hd : DirectedOn (· ≥ ·) s)
+    (hne : s.Nonempty) (hbdd : BddBelow s) :
+    e (sInf s) = ⨅ x : s, e x :=
+  e.dual.map_csSup_of_directedOn hd hne hbdd
+
+theorem map_csInf_of_directedOn' (e : α ≃o β) {s : Set α} (hd : DirectedOn (· ≥ ·) s)
+    (hne : s.Nonempty) (hbdd : BddBelow s) :
+    e (sInf s) = sInf (e '' s) :=
+  e.dual.map_csSup_of_directedOn' hd hne hbdd
+
+theorem map_ciInf_of_directed (e : α ≃o β) {f : ι → α} (hd : Directed (· ≥ ·) f)
+    (hf : BddBelow (range f)) :
+    e (⨅ i, f i) = ⨅ i, e (f i) :=
+  e.dual.map_ciSup_of_directed hd hf
+
+theorem map_ciInf_set_of_directedOn (e : α ≃o β) {s : Set γ} {f : γ → α}
+    (hd : DirectedOn (· ≥ ·) (f '' s)) (hf : BddBelow (f '' s))
+    (hne : s.Nonempty) : e (⨅ i : s, f i) = ⨅ i : s, e (f i) :=
+  e.dual.map_ciSup_set_of_directedOn hd hf hne
+
+end Inf
+
+end OrderIso
diff --git a/Mathlib/Order/Directed.lean b/Mathlib/Order/Directed.lean
index c49c856dd5164a..0943f0a9ff3b9c 100644
--- a/Mathlib/Order/Directed.lean
+++ b/Mathlib/Order/Directed.lean
@@ -207,6 +207,15 @@ theorem Antitone.directed_le [Preorder α] [IsCodirectedOrder α] [Preorder β]
     (hf : Antitone f) : Directed (· ≤ ·) f :=
   directed_of_isDirected_ge hf
 
+@[to_dual]
+lemma directedOn_iff_isDirectedOrder [LE α] {s : Set α} :
+    DirectedOn (· ≤ ·) s ↔ IsDirectedOrder s := by
+  rw [directedOn_iff_directed, IsDirectedOrder]
+  exact ⟨fun h ↦ ⟨h⟩, fun ⟨h⟩ ↦ h⟩
+
+@[to_dual]
+alias ⟨DirectedOn.isDirectedOrder, DirectedOn.of_isDirectedOrder⟩ := directedOn_iff_isDirectedOrder
+
 section Reflexive
 
 protected theorem DirectedOn.insert (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s)
@@ -256,6 +265,15 @@ theorem isTop_or_exists_gt [IsDirectedOrder α] (a : α) : IsTop a ∨ ∃ b, a
 theorem isTop_iff_isMax [IsDirectedOrder α] : IsTop a ↔ IsMax a :=
   ⟨IsTop.isMax, IsMax.isTop⟩
 
+/-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`. -/
+theorem Monotone.forall_le_of_antitone [IsDirectedOrder α] [Preorder β] {f g : α → β}
+    (hf : Monotone f) (hg : Antitone g) (h : f ≤ g) (m n : α) : f m ≤ g n := by
+  obtain ⟨k, hkm, hkn⟩ := exists_ge_ge m n
+  calc
+    f m ≤ f k := hf hkm
+    _ ≤ g k := h _
+    _ ≤ g n := hg hkn
+
 end Preorder
 
 section PartialOrder
@@ -295,8 +313,8 @@ variable [Preorder α] {f : α → β} {s : Set α}
 /-- If `f` is monotone and antitone on a directed order, then `f` is constant. -/
 lemma constant_of_monotone_antitone [IsDirectedOrder α] (hf : Monotone f) (hf' : Antitone f)
     (a b : α) : f a = f b := by
-  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
-  exact le_antisymm ((hf hac).trans <| hf' hbc) ((hf hbc).trans <| hf' hac)
+  have := hf.forall_le_of_antitone hf' le_rfl
+  exact le_antisymm (this a b) (this b a)
 
 /-- If `f` is monotone and antitone on a directed set `s`, then `f` is constant on `s`. -/
 lemma constant_of_monotoneOn_antitoneOn (hf : MonotoneOn f s) (hf' : AntitoneOn f s)
diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean
index 827043af06cf6d..4de43ab1e60b44 100644
--- a/Mathlib/Order/Lattice.lean
+++ b/Mathlib/Order/Lattice.lean
@@ -300,14 +300,6 @@ theorem Ne.lt_sup_or_lt_sup (hab : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b :=
 theorem ite_le_sup (a b : α) (P : Prop) [Decidable P] : ite P a b ≤ a ⊔ b :=
   if h : P then (if_pos h).trans_le le_sup_left else (if_neg h).trans_le le_sup_right
 
-/-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`. -/
-theorem Monotone.forall_le_of_antitone {β : Type*} [Preorder β] {f g : α → β} (hf : Monotone f)
-    (hg : Antitone g) (h : f ≤ g) (m n : α) : f m ≤ g n :=
-  calc
-    f m ≤ f (m ⊔ n) := hf le_sup_left
-    _ ≤ g (m ⊔ n) := h _
-    _ ≤ g n := hg le_sup_right
-
 -- `to_dual` cannot yet reorder arguments of arguments
 theorem SemilatticeSup.ext_sup {α} {A B : SemilatticeSup α}
     (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y)