diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
index fecde492ec8170..5fb107636440e2 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
@@ -46,6 +46,7 @@ Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot
 variable [Preorder α]
 
 open Classical in
+@[to_dual]
 noncomputable instance WithTop.instSupSet [SupSet α] :
     SupSet (WithTop α) :=
   ⟨fun S =>
@@ -53,16 +54,10 @@ noncomputable instance WithTop.instSupSet [SupSet α] :
       ↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩
 
 open Classical in
+@[to_dual]
 noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) :=
   ⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩
 
-noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) :=
-  ⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩
-
-noncomputable instance WithBot.instInfSet [InfSet α] :
-    InfSet (WithBot α) :=
-  ⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩
-
 theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)
     (hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
   (if_neg hs).trans <| if_pos hs'
@@ -79,10 +74,11 @@ theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥})
     sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
   WithTop.sInf_eq (α := αᵒᵈ) hs h's
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
   if_pos <| by simp
 
+@[to_dual (attr := norm_cast)]
 theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
     ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
   classical
@@ -95,6 +91,7 @@ theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddB
   · rw [preimage_image_eq]
     exact Option.some_injective _
 
+@[to_dual (attr := norm_cast)]
 theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
     ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
   classical
@@ -103,24 +100,10 @@ theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
   · exact Option.some_injective _
   · rintro ⟨x, _, ⟨⟩⟩
 
-@[simp]
-theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
-  WithTop.sInf_empty (α := αᵒᵈ)
-
 theorem WithBot.sInf_empty (α : Type*) [CompleteLattice α] : (sInf ∅ : WithBot α) = ⊤ := by
   rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
     WithBot.coe_top]
 
-@[norm_cast]
-theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
-    ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
-  WithTop.coe_sInf' (α := αᵒᵈ) hs h's
-
-@[norm_cast]
-theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) :
-    ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
-  WithTop.coe_sSup' (α := αᵒᵈ) hs
-
 end
 
 instance ConditionallyCompleteLinearOrder.toLinearOrder [h : ConditionallyCompleteLinearOrder α] :
@@ -253,35 +236,29 @@ theorem notMem_of_csSup_lt {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove
 /-- 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 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. -/]
 theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt (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 (csSup_le hs H)) fun hb =>
     let ⟨_, ha, ha'⟩ := H' _ hb
     lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha
 
-/-- 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. -/
-theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt :
-    s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
-  csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ)
-
 /-- `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 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. -/]
 theorem lt_csSup_of_lt (hs : BddAbove s) (ha : a ∈ s) (h : b < a) : b < sSup s :=
   lt_of_lt_of_le h (le_csSup hs ha)
 
-/-- `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. -/
-theorem csInf_lt_of_lt : BddBelow s → a ∈ s → a < b → sInf s < b :=
-  lt_csSup_of_lt (α := αᵒᵈ)
-
 /-- If all elements of a nonempty set `s` are less than or equal to all elements
 of a nonempty set `t`, then there exists an element between these sets. -/
 theorem exists_between_of_forall_le (sne : s.Nonempty) (tne : t.Nonempty)
@@ -390,49 +367,38 @@ variable [ConditionallyCompleteLinearOrder α] {f : ι → α} {s : Set α} {a b
 
 /-- When `b < sSup s`, there is an element `a` in `s` with `b < a`, if `s` is nonempty and the order
 is a linear order. -/
+@[to_dual exists_lt_of_csInf_lt /-- When `sInf s < b`, there is an element `a` in `s` with `a < b`,
+if `s` is nonempty and the order is a linear order. -/]
 theorem exists_lt_of_lt_csSup (hs : s.Nonempty) (hb : b < sSup s) : ∃ a ∈ s, b < a := by
   contrapose! hb
   exact csSup_le hs hb
 
-/-- When `sInf s < b`, there is an element `a` in `s` with `a < b`, if `s` is nonempty and the order
-is a linear order. -/
-theorem exists_lt_of_csInf_lt (hs : s.Nonempty) (hb : sInf s < b) : ∃ a ∈ s, a < b :=
-  exists_lt_of_lt_csSup (α := αᵒᵈ) hs hb
-
+@[to_dual csInf_lt_iff]
 theorem lt_csSup_iff (hb : BddAbove s) (hs : s.Nonempty) : a < sSup s ↔ ∃ b ∈ s, a < b :=
   lt_isLUB_iff <| isLUB_csSup hs hb
 
-theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b ∈ s, b < a :=
-  isGLB_lt_iff <| isGLB_csInf hs hb
-
-@[simp] lemma csSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup ∅ :=
+@[to_dual (attr := simp)]
+lemma csSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup ∅ :=
   ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove s hs
 
-@[simp] lemma ciSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup ∅ :=
+@[to_dual (attr := simp)]
+lemma ciSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup ∅ :=
   csSup_of_not_bddAbove hf
 
+@[to_dual]
 lemma csSup_eq_univ_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup univ := by
   rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
   contrapose hs
   exact hs.mono (subset_univ _)
 
+@[to_dual]
 lemma ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ :=
   csSup_eq_univ_of_not_bddAbove hf
 
-@[simp] lemma csInf_of_not_bddBelow (hs : ¬BddBelow s) : sInf s = sInf ∅ :=
-  ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow s hs
-
-@[simp] lemma ciInf_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf ∅ :=
-  csInf_of_not_bddBelow hf
-
-lemma csInf_eq_univ_of_not_bddBelow (hs : ¬BddBelow s) : sInf s = sInf univ :=
-  csSup_eq_univ_of_not_bddAbove (α := αᵒᵈ) hs
-
-lemma ciInf_eq_univ_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf univ :=
-  csInf_eq_univ_of_not_bddBelow hf
-
 /-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
 `s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded. -/
+@[to_dual /-- When every element of a set `s` is bounded by an element of a set `t`, and conversely,
+then `s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/]
 theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
     (hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
     sSup s = sSup t := by
@@ -464,13 +430,6 @@ theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
       exact hyx.trans (le_csSup Bs xs)
   · simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]
 
-/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
-`s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/
-theorem csInf_eq_csInf_of_forall_exists_le {s t : Set α}
-    (hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
-    sInf s = sInf t :=
-  csSup_eq_csSup_of_forall_exists_le (α := αᵒᵈ) hs ht
-
 theorem csSup_union_le (s t : Set α) : sSup (s ∪ t) ≤ sSup s ⊔ sSup t := by
   rcases s.eq_empty_or_nonempty with (rfl | hs)
   · simp
@@ -489,12 +448,10 @@ lemma sSup_iUnion_Iic (f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i,
 lemma sInf_iUnion_Ici (f : ι → α) : sInf (⋃ (i : ι), Ici (f i)) = ⨅ i, f i :=
   sSup_iUnion_Iic (α := αᵒᵈ) f
 
+@[to_dual]
 theorem csInf_eq_bot_of_bot_mem [OrderBot α] {s : Set α} (hs : ⊥ ∈ s) : sInf s = ⊥ :=
   eq_bot_iff.2 <| csInf_le (OrderBot.bddBelow s) hs
 
-theorem csSup_eq_top_of_top_mem [OrderTop α] {s : Set α} (hs : ⊤ ∈ s) : sSup s = ⊤ :=
-  csInf_eq_bot_of_bot_mem (α := αᵒᵈ) hs
-
 open Function
 
 variable [WellFoundedLT α]
@@ -619,6 +576,8 @@ variable [ConditionallyCompleteLinearOrderBot α]
 
 /-- The `sSup` of a non-empty set is its least upper bound for a conditionally
 complete lattice with a top. -/
+@[to_dual /-- The `sInf` of a non-empty set is its greatest lower bound for a conditionally
+complete lattice with a bottom. -/]
 theorem isLUB_sSup' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
     (hs : s.Nonempty) : IsLUB s (sSup s) := by
   classical
@@ -661,6 +620,8 @@ theorem isLUB_sSup (s : Set (WithTop α)) : IsLUB s (sSup s) := by
 
 /-- The `sInf` of a bounded-below set is its greatest lower bound for a conditionally
 complete lattice with a top. -/
+@[to_dual /-- The `sSup` of a bounded-above set is its lowest upper bound for a conditionally
+complete lattice with a bottom. -/]
 theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
     (hs : BddBelow s) : IsGLB s (sInf s) := by
   classical
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Defs.lean b/Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
index d6858e8a17a9bf..3a1c9191bccc3a 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
@@ -81,6 +81,8 @@ class ConditionallyCompleteLinearOrder (α : Type*)
   compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by
     compareOfLessAndEq_rfl
 
+attribute [to_dual existing] ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove
+
 /-- A conditionally complete linear order with `Bot` is a linear order with least element, in which
 every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily
 bounded below) has an infimum.  A typical example is the natural numbers.
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
index 65502dab75bcbf..db7baa5804342c 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
@@ -33,29 +33,21 @@ Extension of `iSup` and `iInf` from a preorder `α` to `WithTop α` and `WithBot
 
 variable [Preorder α]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) :
     ⨅ i, f i = ⊤ := by rw [iInf, range_eq_empty, WithTop.sInf_empty]
 
-@[norm_cast]
+@[to_dual (attr := norm_cast)]
 theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) :
     ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) := by
   rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]
 
-@[norm_cast]
+@[to_dual (attr := norm_cast)]
 theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
     ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by
   rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
 
-@[simp]
-theorem WithBot.ciSup_empty [IsEmpty ι] [SupSet α] (f : ι → WithBot α) :
-    ⨆ i, f i = ⊥ :=
-  WithTop.iInf_empty (α := αᵒᵈ) _
-
-@[norm_cast]
-theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) :
-    ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) :=
-  WithTop.coe_iInf (α := αᵒᵈ) hf
+@[deprecated (since := "2026-05-04")] alias WithBot.ciSup_empty := WithBot.iSup_empty
 
 theorem WithBot.coe_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty)
     {α : Type*} [CompleteLattice α] (f : ι → α) :
@@ -69,10 +61,11 @@ theorem WithBot.coe_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty)
   · simpa only [iSup_pos h] using by apply le_biSup _ h
   · simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)
 
-@[norm_cast]
-theorem WithBot.coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) :
-    ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) :=
-  WithTop.coe_iSup (α := αᵒᵈ) _ h
+@[to_dual existing]
+theorem WithTop.coe_biInf {ι : Type*} {s : Set ι} (hs : s.Nonempty)
+    {α : Type*} [CompleteLattice α] (f : ι → α) :
+    ⨅ i ∈ s, f i = ⨅ i ∈ s, (f i : WithTop α) :=
+  WithBot.coe_biSup (α := αᵒᵈ) hs f
 
 theorem WithBot.coe_biInf {ι : Type*} {s : Set ι} {α : Type*} [CompleteLattice α] (f : ι → α) :
     ⨅ i ∈ s, f i = ⨅ i ∈ s, (f i : WithBot α) := by
@@ -82,71 +75,65 @@ theorem WithBot.coe_biInf {ι : Type*} {s : Set ι} {α : Type*} [CompleteLattic
   · simpa only [iInf_pos h] using by apply biInf_le _ h
   · simp [iInf_neg h]
 
+@[to_dual existing]
+theorem WithTop.coe_biSup {ι : Type*} {s : Set ι} {α : Type*} [CompleteLattice α] (f : ι → α) :
+    ⨆ i ∈ s, f i = ⨆ i ∈ s, (f i : WithTop α) :=
+  WithBot.coe_biInf (α := αᵒᵈ) f
+
 end
 
 section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice α] {a b : α}
 
+@[to_dual]
 theorem isLUB_ciSup [Nonempty ι] {f : ι → α} (H : BddAbove (range f)) :
     IsLUB (range f) (⨆ i, f i) :=
   isLUB_csSup (range_nonempty f) H
 
+@[to_dual]
 theorem isLUB_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) :
     IsLUB (f '' s) (⨆ i : s, f i) := by
   rw [← sSup_image']
   exact isLUB_csSup (Hne.image _) H
 
-theorem isGLB_ciInf [Nonempty ι] {f : ι → α} (H : BddBelow (range f)) :
-    IsGLB (range f) (⨅ i, f i) :=
-  isGLB_csInf (range_nonempty f) H
-
-theorem isGLB_ciInf_set {f : β → α} {s : Set β} (H : BddBelow (f '' s)) (Hne : s.Nonempty) :
-    IsGLB (f '' s) (⨅ i : s, f i) :=
-  isLUB_ciSup_set (α := αᵒᵈ) H Hne
-
+@[to_dual le_ciInf_iff]
 theorem ciSup_le_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddAbove (range f)) :
     iSup f ≤ a ↔ ∀ i, f i ≤ a :=
   (isLUB_le_iff <| isLUB_ciSup hf).trans forall_mem_range
 
-theorem le_ciInf_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddBelow (range f)) :
-    a ≤ iInf f ↔ ∀ i, a ≤ f i :=
-  (le_isGLB_iff <| isGLB_ciInf hf).trans forall_mem_range
-
+@[to_dual le_ciInf_set_iff]
 theorem ciSup_set_le_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
     (hf : BddAbove (f '' s)) : ⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a :=
   (isLUB_le_iff <| isLUB_ciSup_set hf hs).trans forall_mem_image
 
-theorem le_ciInf_set_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
-    (hf : BddBelow (f '' s)) : (a ≤ ⨅ i : s, f i) ↔ ∀ i ∈ s, a ≤ f i :=
-  (le_isGLB_iff <| isGLB_ciInf_set hf hs).trans forall_mem_image
-
+@[to_dual]
 theorem IsLUB.ciSup_eq [Nonempty ι] {f : ι → α} (H : IsLUB (range f) a) : ⨆ i, f i = a :=
   H.csSup_eq (range_nonempty f)
 
+@[to_dual]
 theorem IsLUB.ciSup_set_eq {s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) :
     ⨆ i : s, f i = a :=
   IsLUB.csSup_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)
 
-theorem IsGLB.ciInf_eq [Nonempty ι] {f : ι → α} (H : IsGLB (range f) a) : ⨅ i, f i = a :=
-  H.csInf_eq (range_nonempty f)
-
-theorem IsGLB.ciInf_set_eq {s : Set β} {f : β → α} (H : IsGLB (f '' s) a) (Hne : s.Nonempty) :
-    ⨅ i : s, f i = a :=
-  IsGLB.csInf_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)
-
 /-- The indexed supremum of a function is bounded above by a uniform bound -/
+@[to_dual le_ciInf /-- The indexed infimum of a function is bounded below by a uniform bound -/]
 theorem ciSup_le [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c :=
   csSup_le (range_nonempty f) (by rwa [forall_mem_range])
 
 /-- The indexed supremum of a function is bounded below by the value taken at one point -/
+@[to_dual ciInf_le /-- The indexed infimum of a function is bounded above by the value taken at one
+point -/]
 theorem le_ciSup {f : ι → α} (H : BddAbove (range f)) (c : ι) : f c ≤ iSup f :=
   le_csSup H (mem_range_self _)
 
+@[to_dual ciInf_le_of_le]
 theorem le_ciSup_of_le {f : ι → α} (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f :=
   le_trans h (le_ciSup H c)
 
 /-- If the set of all `f i j` is bounded above, then so is the set of the supremums of every row -/
+@[to_dual /-- If the set of all `f i j` is bounded below, then so is the set of the infimums of
+every row -/]
 theorem BddAbove.range_iSup_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i → α}
     (H : BddAbove <| ⋃ i, range (f i)) : BddAbove <| range fun i ↦ ⨆ j, f i j := by
   have ⟨a, h⟩ := H
@@ -155,19 +142,22 @@ theorem BddAbove.range_iSup_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i
   · exact iSup_of_empty' (f i) ▸ le_sup_right
   exact ciSup_le fun j ↦ le_sup_of_le_left <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩
 
+@[to_dual ciInf₂_le]
 theorem le_ciSup₂ {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddAbove <| ⋃ i, range (f i)) (i : ι)
     (j : κ i) : f i j ≤ ⨆ (i) (j), f i j :=
   le_ciSup_of_le H.range_iSup_of_iUnion_range i <|
     le_ciSup (H.mono <| subset_iUnion (range <| f ·) i) j
 
 /-- The indexed suprema of two functions are comparable if the functions are pointwise comparable -/
-@[gcongr low]
+@[to_dual (attr := gcongr low) /-- The indexed infimum of two functions are comparable if the
+functions are pointwise comparable -/]
 theorem ciSup_mono {f 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 ciSup_le fun x => le_ciSup_of_le B x (H x)
 
+@[to_dual]
 theorem ciSup_sup_eq {f g : ι → α} (Hf : BddAbove <| range f) (Hg : BddAbove <| range g) :
     ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ (⨆ x, g x) := by
   cases isEmpty_or_nonempty ι
@@ -176,60 +166,22 @@ theorem ciSup_sup_eq {f g : ι → α} (Hf : BddAbove <| range f) (Hg : BddAbove
   have := bbdAbove_range_sup Hf Hg
   exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)
 
+@[to_dual ciInf_set_le]
 theorem le_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c ∈ s) :
     f c ≤ ⨆ i : s, f i :=
   (le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image'
 
-/-- The indexed infimum of two functions are comparable if the functions are pointwise comparable -/
-@[gcongr low]
-theorem ciInf_mono {f g : ι → α} (B : BddBelow (range f)) (H : ∀ x, f x ≤ g x) : iInf f ≤ iInf g :=
-  ciSup_mono (α := αᵒᵈ) B H
-
-theorem ciInf_inf_eq {f g : ι → α} (Hf : BddBelow <| range f) (Hg : BddBelow <| range g) :
-    ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ (⨅ x, g x) :=
-  ciSup_sup_eq (α := αᵒᵈ) Hf Hg
-
-/-- The indexed minimum of a function is bounded below by a uniform lower bound -/
-theorem le_ciInf [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f :=
-  ciSup_le (α := αᵒᵈ) H
-
-/-- The indexed infimum of a function is bounded above by the value taken at one point -/
-theorem ciInf_le {f : ι → α} (H : BddBelow (range f)) (c : ι) : iInf f ≤ f c :=
-  le_ciSup (α := αᵒᵈ) H c
-
-theorem ciInf_le_of_le {f : ι → α} (H : BddBelow (range f)) (c : ι) (h : f c ≤ a) : iInf f ≤ a :=
-  le_ciSup_of_le (α := αᵒᵈ) H c h
-
+@[to_dual]
 theorem ciSup_mono_of_forall_exists {ι'} [Nonempty ι] {f : ι → α} {g : ι' → α}
     (hg : BddAbove <| range g) (h : ∀ i, ∃ i', f i ≤ g i') : ⨆ i, f i ≤ ⨆ i', g i' :=
   ciSup_le fun i ↦ h i |>.elim <| le_ciSup_of_le hg
 
-theorem ciInf_mono_of_forall_exists {ι'} [Nonempty ι'] {f : ι → α} {g : ι' → α}
-    (hf : BddBelow <| range f) (h : ∀ i', ∃ i, f i ≤ g i') : ⨅ i, f i ≤ ⨅ i', g i' :=
-  ciSup_mono_of_forall_exists (α := αᵒᵈ) hf h
-
-/-- If the set of all `f i j` is bounded below, then so is the set of the infimums of every row -/
-theorem BddBelow.range_iInf_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i → α}
-    (H : BddBelow <| ⋃ i, range (f i)) : BddBelow <| range fun i ↦ ⨅ j, f i j := by
-  have ⟨a, h⟩ := H
-  refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
-  cases isEmpty_or_nonempty <| κ i
-  · exact iInf_of_isEmpty (f i) ▸ inf_le_right
-  exact le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩
-
-theorem ciInf₂_le {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddBelow <| ⋃ i, range (f i)) (i : ι)
-    (j : κ i) : ⨅ (i) (j), f i j ≤ f i j :=
-  ciInf_le_of_le H.range_iInf_of_iUnion_range i <|
-    ciInf_le (H.mono <| subset_iUnion (range <| f ·) i) j
-
-theorem ciInf_set_le {f : β → α} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c ∈ s) :
-    ⨅ i : s, f i ≤ f c :=
-  le_ciSup_set (α := αᵒᵈ) H hc
-
+@[to_dual self (reorder := hf hf')]
 lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf' : BddAbove (range f)) :
     ⨅ i, f i ≤ ⨆ i, f i :=
   (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)
 
+@[to_dual]
 lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) :
     ⨆ p, f p = ⨆ b, ⨆ c, f (b, c) := by
   rcases isEmpty_or_nonempty β
@@ -251,34 +203,25 @@ lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) :
   conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]
   simp [Prod.forall]
 
-lemma ciInf_prod {f : β × γ → α} (hf : BddBelow (Set.range f)) :
-    ⨅ p, f p = ⨅ b, ⨅ c, f (b, c) :=
-  ciSup_prod (α := αᵒᵈ) hf
-
 /-- 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 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 ciSup_eq_of_forall_le_of_forall_lt_exists_gt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, f i ≤ b)
     (h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b :=
   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
 
-/-- 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 ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i)
-    (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b :=
-  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂
-
+@[to_dual]
 lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
     Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by
   ext
   simpa using le_ciInf_iff hf
 
-lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
-    Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
-  Iic_ciInf (α := αᵒᵈ) hf
-
+@[to_dual]
 theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α}
     (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
     iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
@@ -300,11 +243,7 @@ theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α}
     · exact le_ciSup hf ?_
     · exact hf'
 
-theorem ciInf_subtype {p : ι → Prop} {f : Subtype p → α}
-    (hf : BddBelow (Set.range f)) (hf' : iInf f ≤ sInf ∅) :
-    iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
-  ciSup_subtype (α := αᵒᵈ) hf hf'
-
+@[to_dual]
 theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α}
     (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop)))
     (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) :
@@ -313,14 +252,9 @@ theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α}
 
 @[deprecated (since := "2026-04-04")] alias ciSup_subtype' := cbiSup_eq_ciSup_subtype
 
-theorem cbiInf_eq_ciInf_subtype {p : ι → Prop} {f : ∀ i, p i → α}
-    (hf : BddBelow (Set.range (fun i : Subtype p ↦ f i i.prop)))
-    (hf' : ⨅ (i : Subtype p), f i i.prop ≤ sInf ∅) :
-    ⨅ (i) (h), f i h = ⨅ x : Subtype p, f x x.property :=
-  (ciInf_subtype (f := fun x => f x.val x.property) hf hf').symm
-
 @[deprecated (since := "2026-04-04")] alias ciInf_subtype' := cbiInf_eq_ciInf_subtype
 
+@[to_dual]
 theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α}
     (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
     ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
@@ -328,33 +262,21 @@ theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α}
 
 @[deprecated (since := "2026-04-04")] alias ciSup_subtype'' := ciSup_subtype_fun
 
-theorem ciInf_subtype_fun {ι} {s : Set ι} {f : ι → α}
-    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
-    ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
-  ciInf_subtype hf hf'
-
 @[deprecated (since := "2026-04-04")] alias ciInf_subtype'' := ciInf_subtype_fun
 
+@[to_dual]
 theorem csSup_image {s : Set β} {f : β → α}
     (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
     sSup (f '' s) = ⨆ a ∈ s, f a := by
   rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]
 
-theorem csInf_image {s : Set β} {f : β → α}
-    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
-    sInf (f '' s) = ⨅ a ∈ s, f a :=
-  csSup_image (α := αᵒᵈ) hf hf'
-
+@[to_dual]
 theorem cbiSup_id {s : Set α} (hs : BddAbove s) (h : sSup ∅ ≤ sSup s) : ⨆ i ∈ s, i = sSup s := by
   rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']
   · convert! h
     rw [← sSup_range, Subtype.range_coe]
 
-theorem cbiInf_id {s : Set α} (hs : BddBelow s) (h : sInf s ≤ sInf ∅) : ⨅ i ∈ s, i = sInf s := by
-  rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']
-  · convert! h
-    rw [← sInf_range, Subtype.range_coe]
-
+@[to_dual]
 lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α}
     (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
     ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x) := by
@@ -375,13 +297,9 @@ lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α
     simpa [bddAbove_def] using hf
   rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
 
-lemma ciInf_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α}
-    (hf : BddBelow (Set.range fun i : s ↦ g (f i))) (hg' : ⨅ i : s, g (f i) ≤ sInf ∅) :
-    ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
-  ciSup_image (α := αᵒᵈ) hf hg'
-
 /-- Note that equality need not hold: consider `ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1`,
 then the LHS is `-1` but the RHS is `-1 ⊔ sSup ∅ = -1 ⊔ 0 = 0`. -/
+@[to_dual le_ciInf_exists]
 theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih ≤ ⨆ (i) (h), f ⟨i, h⟩ := by
   by_cases! h : Exists p
   · have : Nonempty <| Exists p := ⟨h⟩
@@ -391,21 +309,17 @@ theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih 
   · cases isEmpty_or_nonempty ι <;>
       simp [h, iSup_of_empty', ciSup_const]
 
-theorem le_ciInf_exists {p : ι → Prop} {f : Exists p → α} : ⨅ (i) (h), f ⟨i, h⟩ ≤ ⨅ ih, f ih :=
-  ciSup_exists_le (α := αᵒᵈ)
-
+@[to_dual]
 theorem ciSup_and {p q : Prop} {f : p ∧ q → α} : ⨆ ih, f ih = ⨆ (h₁) (h₂), f ⟨h₁, h₂⟩ := by
   by_cases hp : p <;> by_cases hq : q <;> simp [hp, hq, iSup_of_empty']
 
-theorem ciInf_and {p q : Prop} {f : p ∧ q → α} : ⨅ ih, f ih = ⨅ (h₁) (h₂), f ⟨h₁, h₂⟩ :=
-  ciSup_and (α := αᵒᵈ)
-
 end ConditionallyCompleteLattice
 
 section ConditionallyCompleteLinearOrder
 
 variable [ConditionallyCompleteLinearOrder α] {a b : α}
 
+@[to_dual]
 theorem ciSup_sup_le {f g : ι → α} : ⨆ x, f x ⊔ g x ≤ (⨆ x, f x) ⊔ (⨆ x, g x) := by
   by_cases! hf : ¬BddAbove (range f)
   · rw [ciSup_of_not_bddAbove hf, ciSup_of_not_bddAbove <| mt bbdAbove_range_left_of_sup hf]
@@ -415,40 +329,27 @@ theorem ciSup_sup_le {f g : ι → α} : ⨆ x, f x ⊔ g x ≤ (⨆ x, f x) ⊔
     exact le_sup_right
   exact ciSup_sup_eq hf hg |>.le
 
-theorem ciInf_inf_le {f g : ι → α} : (⨅ x, f x) ⊓ (⨅ x, g x) ≤ ⨅ x, f x ⊓ g x :=
-  ciSup_sup_le (α := αᵒᵈ)
-
 /-- Indexed version of `exists_lt_of_lt_csSup`.
 When `b < iSup f`, there is an element `i` such that `b < f i`.
 -/
+@[to_dual exists_lt_of_ciInf_lt /-- Indexed version of `exists_lt_of_csInf_lt`.
+When `iInf f < a`, there is an element `i` such that `f i < a`. -/]
 theorem exists_lt_of_lt_ciSup [Nonempty ι] {f : ι → α} (h : b < iSup f) : ∃ i, b < f i :=
   let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_csSup (range_nonempty f) h
   ⟨i, h⟩
 
-/-- Indexed version of `exists_lt_of_csInf_lt`.
-When `iInf f < a`, there is an element `i` such that `f i < a`.
--/
-theorem exists_lt_of_ciInf_lt [Nonempty ι] {f : ι → α} (h : iInf f < a) : ∃ i, f i < a :=
-  exists_lt_of_lt_ciSup (α := αᵒᵈ) h
-
+@[to_dual ciInf_lt_iff]
 theorem lt_ciSup_iff [Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) :
     a < iSup f ↔ ∃ i, a < f i := by
   simpa only [mem_range, exists_exists_eq_and] using! lt_csSup_iff hb (range_nonempty _)
 
-theorem ciInf_lt_iff [Nonempty ι] {f : ι → α} (hb : BddBelow (range f)) :
-    iInf f < a ↔ ∃ i, f i < a := by
-  simpa only [mem_range, exists_exists_eq_and] using! csInf_lt_iff hb (range_nonempty _)
-
+@[to_dual]
 theorem cbiSup_of_not_bddAbove {p : ι → Prop} {f : ∀ i, p i → α}
     (h : ¬BddAbove (range fun i : Subtype p ↦ f i i.prop)) :
     ⨆ (i : ι), ⨆ (h : p i), f i h = sSup ∅ :=
   ciSup_of_not_bddAbove fun ⟨u, hu⟩ ↦ h ⟨u, fun _ ⟨x, hx⟩ ↦ hx ▸ hu ⟨x, ciSup_pos x.prop⟩⟩
 
-theorem cbiInf_of_not_bddBelow {p : ι → Prop} {f : ∀ i, p i → α}
-    (h : ¬BddBelow (range fun i : Subtype p ↦ f i i.prop)) :
-    ⨅ (i : ι), ⨅ (h : p i), f i h = sInf ∅ :=
-  ciInf_of_not_bddBelow fun ⟨u, hu⟩ ↦ h ⟨u, fun _ ⟨x, hx⟩ ↦ hx ▸ hu ⟨x, ciInf_pos x.prop⟩⟩
-
+@[to_dual]
 theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
     ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅ := by
   rcases le_or_gt (sSup ∅) (iSup f) with le | gt
@@ -466,13 +367,7 @@ theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : 
     · exact (ciSup_neg hj).le
   · exact fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩
 
-theorem cbiInf_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
-    ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f ⊓ sInf ∅ :=
-  cbiSup_eq_of_not_forall (α := αᵒᵈ) hp
-
-theorem ciInf_eq_bot_of_bot_mem [OrderBot α] {f : ι → α} (hs : ⊥ ∈ range f) : iInf f = ⊥ :=
-  csInf_eq_bot_of_bot_mem hs
-
+@[to_dual]
 theorem ciSup_eq_top_of_top_mem [OrderTop α] {f : ι → α} (hs : ⊤ ∈ range f) : iSup f = ⊤ :=
   csSup_eq_top_of_top_mem hs
 
@@ -566,38 +461,26 @@ namespace GaloisConnection
 variable [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β}
   {u : β → α}
 
+@[to_dual]
 theorem l_csSup (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     l (sSup s) = ⨆ x : s, l x :=
   Eq.symm <| IsLUB.ciSup_set_eq (gc.isLUB_l_image <| isLUB_csSup hne hbdd) hne
 
+@[to_dual]
 theorem l_csSup' (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     l (sSup s) = sSup (l '' s) := by rw [gc.l_csSup hne hbdd, sSup_image']
 
+@[to_dual]
 theorem l_ciSup (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) :
     l (⨆ i, f i) = ⨆ i, l (f i) := by rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']
 
+@[to_dual]
 theorem l_ciSup_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (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
   exact gc.l_ciSup hf
 
-theorem u_csInf (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    u (sInf s) = ⨅ x : s, u x :=
-  gc.dual.l_csSup hne hbdd
-
-theorem u_csInf' (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    u (sInf s) = sInf (u '' s) :=
-  gc.dual.l_csSup' hne hbdd
-
-theorem u_ciInf (gc : GaloisConnection l u) {f : ι → β} (hf : BddBelow (range f)) :
-    u (⨅ i, f i) = ⨅ i, u (f i) :=
-  gc.dual.l_ciSup hf
-
-theorem u_ciInf_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → β} (hf : BddBelow (f '' s))
-    (hne : s.Nonempty) : u (⨅ i : s, f i) = ⨅ i : s, u (f i) :=
-  gc.dual.l_ciSup_set hf hne
-
 end GaloisConnection
 
 namespace OrderIso
@@ -605,38 +488,26 @@ namespace OrderIso
 section ConditionallyCompleteLattice
 variable [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι]
 
+@[to_dual]
 theorem map_csSup (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     e (sSup s) = ⨆ x : s, e x :=
   e.to_galoisConnection.l_csSup hne hbdd
 
+@[to_dual]
 theorem map_csSup' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     e (sSup s) = sSup (e '' s) :=
   e.to_galoisConnection.l_csSup' hne hbdd
 
+@[to_dual]
 theorem map_ciSup (e : α ≃o β) {f : ι → α} (hf : BddAbove (range f)) :
     e (⨆ i, f i) = ⨆ i, e (f i) :=
   e.to_galoisConnection.l_ciSup hf
 
+@[to_dual]
 theorem map_ciSup_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s))
     (hne : s.Nonempty) : e (⨆ i : s, f i) = ⨆ i : s, e (f i) :=
   e.to_galoisConnection.l_ciSup_set hf hne
 
-theorem map_csInf (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    e (sInf s) = ⨅ x : s, e x :=
-  e.dual.map_csSup hne hbdd
-
-theorem map_csInf' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    e (sInf s) = sInf (e '' s) :=
-  e.dual.map_csSup' hne hbdd
-
-theorem map_ciInf (e : α ≃o β) {f : ι → α} (hf : BddBelow (range f)) :
-    e (⨅ i, f i) = ⨅ i, e (f i) :=
-  e.dual.map_ciSup hf
-
-theorem map_ciInf_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s))
-    (hne : s.Nonempty) : e (⨅ i : s, f i) = ⨅ i : s, e (f i) :=
-  e.dual.map_ciSup_set hf hne
-
 end ConditionallyCompleteLattice
 
 section ConditionallyCompleteLinearOrderBot