diff --git a/Mathlib.lean b/Mathlib.lean
index dd909bcc0de0bc..f6d86aedd3e6ff 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6807,6 +6807,7 @@ public import Mathlib.Tactic.Translate.Core
 public import Mathlib.Tactic.Translate.GuessName
 public import Mathlib.Tactic.Translate.ToAdditive
 public import Mathlib.Tactic.Translate.ToDual
+public import Mathlib.Tactic.Translate.UnfoldBoundary
 public import Mathlib.Tactic.TryThis
 public import Mathlib.Tactic.TypeCheck
 public import Mathlib.Tactic.TypeStar
diff --git a/Mathlib/Combinatorics/Quiver/Basic.lean b/Mathlib/Combinatorics/Quiver/Basic.lean
index 1a1f7865a08666..a9162552dc0042 100644
--- a/Mathlib/Combinatorics/Quiver/Basic.lean
+++ b/Mathlib/Combinatorics/Quiver/Basic.lean
@@ -83,10 +83,10 @@ instance emptyQuiver (V : Type u) : Quiver.{u} (Empty V) := ⟨fun _ _ => PEmpty
 theorem empty_arrow {V : Type u} (a b : Empty V) : (a ⟶ b) = PEmpty := rfl
 
 /-- A quiver is thin if it has no parallel arrows. -/
-@[to_dual IsThin' /-- `isThin'` is equivalent to `IsThin`.
-It is used by `@[to_dual]` to be able to translate `IsThin`. -/]
 abbrev IsThin (V : Type u) [Quiver V] : Prop := ∀ a b : V, Subsingleton (a ⟶ b)
 
+to_dual_insert_cast_fun IsThin := fun inst a b ↦ inst b a, fun inst a b ↦ inst b a
+
 
 section
 
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index ca68303a0abfce..d4c88404b97858 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -930,11 +930,9 @@ instance preorder [Preorder α] (p : α → Prop) : Preorder (Subtype p) :=
 instance partialOrder [PartialOrder α] (p : α → Prop) : PartialOrder (Subtype p) :=
   PartialOrder.lift (fun (a : Subtype p) ↦ (a : α)) Subtype.coe_injective
 
-@[to_dual decidableLE']
 instance decidableLE [Preorder α] [h : DecidableLE α] {p : α → Prop} :
     DecidableLE (Subtype p) := fun a b ↦ h a b
 
-@[to_dual decidableLT']
 instance decidableLT [Preorder α] [h : DecidableLT α] {p : α → Prop} :
     DecidableLT (Subtype p) := fun a b ↦ h a b
 
diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean
index 08c2e96687253f..9e0edd103d8d20 100644
--- a/Mathlib/Order/Cover.lean
+++ b/Mathlib/Order/Cover.lean
@@ -38,6 +38,7 @@ section Preorder
 
 variable [Preorder α] [Preorder β] {a b c : α}
 
+@[to_dual self]
 theorem WCovBy.le (h : a ⩿ b) : a ≤ b :=
   h.1
 
@@ -46,20 +47,25 @@ theorem WCovBy.refl (a : α) : a ⩿ a :=
 
 @[simp] lemma WCovBy.rfl : a ⩿ a := WCovBy.refl a
 
+@[to_dual wcovBy']
 protected theorem Eq.wcovBy (h : a = b) : a ⩿ b :=
   h ▸ WCovBy.rfl
 
+@[to_dual self]
 theorem wcovBy_of_le_of_le (h1 : a ≤ b) (h2 : b ≤ a) : a ⩿ b :=
   ⟨h1, fun _ hac hcb => (hac.trans hcb).not_ge h2⟩
 
+@[to_dual self]
 alias LE.le.wcovBy_of_le := wcovBy_of_le_of_le
 
 theorem AntisymmRel.wcovBy (h : AntisymmRel (· ≤ ·) a b) : a ⩿ b :=
   wcovBy_of_le_of_le h.1 h.2
 
+@[to_dual self]
 theorem WCovBy.wcovBy_iff_le (hab : a ⩿ b) : b ⩿ a ↔ b ≤ a :=
   ⟨fun h => h.le, fun h => h.wcovBy_of_le hab.le⟩
 
+@[to_dual wcovBy_of_eq_or_eq']
 theorem wcovBy_of_eq_or_eq (hab : a ≤ b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⩿ b :=
   ⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩
 
@@ -76,52 +82,59 @@ theorem wcovBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⩿ a ↔ c 
   ⟨fun h => h.trans_antisymm_rel hab, fun h => h.trans_antisymm_rel hab.symm⟩
 
 /-- If `a ≤ b`, then `b` does not cover `a` iff there's an element in between. -/
+@[to_dual not_wcovBy_iff']
 theorem not_wcovBy_iff (h : a ≤ b) : ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b := by
   simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
 
+@[to_dual stdRefl']
 instance WCovBy.stdRefl : @Std.Refl α (· ⩿ ·) :=
   ⟨WCovBy.refl⟩
 
+@[to_dual self]
 theorem WCovBy.Ioo_eq (h : a ⩿ b) : Ioo a b = ∅ :=
   eq_empty_iff_forall_notMem.2 fun _ hx => h.2 hx.1 hx.2
 
+@[to_dual self]
 theorem wcovBy_iff_Ioo_eq : a ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅ :=
   and_congr_right' <| by simp [eq_empty_iff_forall_notMem]
 
+@[to_dual of_le_of_le']
 lemma WCovBy.of_le_of_le (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : b ⩿ c :=
   ⟨hbc, fun _x hbx hxc ↦ hac.2 (hab.trans_lt hbx) hxc⟩
 
-lemma WCovBy.of_le_of_le' (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : a ⩿ b :=
-  ⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩
-
+@[to_dual self]
 theorem WCovBy.of_image (f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b :=
   ⟨f.le_iff_le.mp h.le, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩
 
+@[to_dual self]
 theorem WCovBy.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b := by
   refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
   obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
   rw [f.lt_iff_lt] at ha hb
   exact hab.2 ha hb
 
+@[to_dual self]
 theorem Set.OrdConnected.apply_wcovBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) :
     f a ⩿ f b ↔ a ⩿ b :=
   ⟨fun h2 => h2.of_image f, fun hab => hab.image f h⟩
 
-@[simp]
+@[simp, to_dual self]
 theorem apply_wcovBy_apply_iff {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
     e a ⩿ e b ↔ a ⩿ b :=
   (ordConnected_range (e : α ≃o β)).apply_wcovBy_apply_iff ((e : α ≃o β) : α ↪o β)
 
-@[simp]
+@[simp, to_dual self]
 theorem toDual_wcovBy_toDual_iff : toDual b ⩿ toDual a ↔ a ⩿ b :=
   and_congr_right' <| forall_congr' fun _ => forall_swap
 
-@[simp]
+@[simp, to_dual self]
 theorem ofDual_wcovBy_ofDual_iff {a b : αᵒᵈ} : ofDual a ⩿ ofDual b ↔ b ⩿ a :=
   and_congr_right' <| forall_congr' fun _ => forall_swap
 
+@[to_dual self]
 alias ⟨_, WCovBy.toDual⟩ := toDual_wcovBy_toDual_iff
 
+@[to_dual self]
 alias ⟨_, WCovBy.ofDual⟩ := ofDual_wcovBy_ofDual_iff
 
 @[deprecated (since := "2025-11-07")] alias OrderEmbedding.wcovBy_of_apply := WCovBy.of_image
diff --git a/Mathlib/Order/Defs/LinearOrder.lean b/Mathlib/Order/Defs/LinearOrder.lean
index 78728ccb080cb6..c35e28529e89cd 100644
--- a/Mathlib/Order/Defs/LinearOrder.lean
+++ b/Mathlib/Order/Defs/LinearOrder.lean
@@ -83,12 +83,6 @@ attribute [instance 900] LinearOrder.toDecidableLT
 attribute [instance 900] LinearOrder.toDecidableLE
 attribute [instance 900] LinearOrder.toDecidableEq
 
-@[to_dual existing toDecidableLT, inherit_doc toDecidableLT]
-def LinearOrder.toDecidableLT' : DecidableLT' α := fun a b => toDecidableLT b a
-
-@[to_dual existing toDecidableLE, inherit_doc toDecidableLE]
-def LinearOrder.toDecidableLE' : DecidableLE' α := fun a b => toDecidableLE b a
-
 instance : Std.IsLinearOrder α where
   le_total := LinearOrder.le_total
 
diff --git a/Mathlib/Order/Defs/PartialOrder.lean b/Mathlib/Order/Defs/PartialOrder.lean
index 830b1bf0795326..450a896843e7cb 100644
--- a/Mathlib/Order/Defs/PartialOrder.lean
+++ b/Mathlib/Order/Defs/PartialOrder.lean
@@ -132,12 +132,9 @@ instance instTransGTGE : @Trans α α α GT.gt GE.ge GT.gt := ⟨lt_of_lt_of_le'
 instance instTransGEGT : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'⟩
 
 /-- `<` is decidable if `≤` is. -/
-@[to_dual decidableLT'OfDecidableLE' /-- `<` is decidable if `≤` is. -/]
 def decidableLTOfDecidableLE [DecidableLE α] : DecidableLT α :=
   fun _ _ => decidable_of_iff _ lt_iff_le_not_ge.symm
 
-@[deprecated (since := "2025-12-09")] alias decidableGTOfDecidableGE := decidableLT'OfDecidableLE'
-
 /-- `WCovBy a b` means that `a = b` or `b` covers `a`.
 This means that `a ≤ b` and there is no element in between. This is denoted `a ⩿ b`.
 -/
@@ -145,6 +142,8 @@ This means that `a ≤ b` and there is no element in between. This is denoted `a
 def WCovBy (a b : α) : Prop :=
   a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
+to_dual_insert_cast WCovBy := by grind
+
 @[inherit_doc]
 infixl:50 " ⩿ " => WCovBy
 
@@ -154,6 +153,8 @@ between. This is denoted `a ⋖ b`. -/
 def CovBy {α : Type*} [LT α] (a b : α) : Prop :=
   a < b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
+to_dual_insert_cast CovBy := by grind
+
 @[inherit_doc]
 infixl:50 " ⋖ " => CovBy
 
@@ -197,16 +198,12 @@ lemma lt_of_le_of_ne : a ≤ b → a ≠ b → a < b := fun h₁ h₂ =>
   lt_of_le_not_ge h₁ <| mt (le_antisymm h₁) h₂
 
 /-- Equality is decidable if `≤` is. -/
-@[to_dual decidableEqOfDecidableLE' /-- Equality is decidable if `≤` is. -/]
 def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
   | a, b =>
     if hab : a ≤ b then
       if hba : b ≤ a then isTrue (le_antisymm hab hba) else isFalse fun heq => hba (heq ▸ le_refl _)
     else isFalse fun heq => hab (heq ▸ le_refl _)
 
-@[deprecated (since := "2025-12-09")] alias decidableEqofDecidableGE := decidableEqOfDecidableLE'
-@[deprecated (since := "2025-12-09")] alias decidableEqofDecidableLE' := decidableEqOfDecidableLE'
-
 -- See Note [decidable namespace]
 @[to_dual Decidable.lt_or_eq_of_le']
 protected lemma Decidable.lt_or_eq_of_le [DecidableLE α] (hab : a ≤ b) : a < b ∨ a = b :=
diff --git a/Mathlib/Order/GaloisConnection/Defs.lean b/Mathlib/Order/GaloisConnection/Defs.lean
index 2c17457a840a87..e20a06f10ceb4e 100644
--- a/Mathlib/Order/GaloisConnection/Defs.lean
+++ b/Mathlib/Order/GaloisConnection/Defs.lean
@@ -38,19 +38,24 @@ variable {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {κ : ι → So
 /-- A Galois connection is a pair of functions `l` and `u` satisfying
 `l a ≤ b ↔ a ≤ u b`. They are special cases of adjoint functors in category theory,
 but do not depend on the category theory library in mathlib. -/
+@[to_dual self (reorder := α β, 3 4, l u)]
 def GaloisConnection [Preorder α] [Preorder β] (l : α → β) (u : β → α) :=
   ∀ a b, l a ≤ b ↔ a ≤ u b
 
+to_dual_insert_cast GaloisConnection := by grind
+
 namespace GaloisConnection
 
 section
 
 variable [Preorder α] [Preorder β] {l : α → β} {u : β → α}
 
+@[to_dual self (reorder := α β, 3 4, l u, hu hl, hul hlu)]
 theorem monotone_intro (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a))
     (hlu : ∀ a, l (u a) ≤ a) : GaloisConnection l u := fun _ _ =>
   ⟨fun h => (hul _).trans (hu h), fun h => (hl h).trans (hlu _)⟩
 
+@[to_dual self]
 protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
     GaloisConnection (OrderDual.toDual ∘ u ∘ OrderDual.ofDual)
       (OrderDual.toDual ∘ l ∘ OrderDual.ofDual) :=
@@ -59,36 +64,29 @@ protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l
 variable (gc : GaloisConnection l u)
 include gc
 
+@[to_dual le_iff_le']
 theorem le_iff_le {a : α} {b : β} : l a ≤ b ↔ a ≤ u b :=
   gc _ _
 
+@[to_dual le_u]
 theorem l_le {a : α} {b : β} : a ≤ u b → l a ≤ b :=
   (gc _ _).mpr
 
-theorem le_u {a : α} {b : β} : l a ≤ b → a ≤ u b :=
-  (gc _ _).mp
-
+@[to_dual l_u_le]
 theorem le_u_l (a) : a ≤ u (l a) :=
   gc.le_u <| le_rfl
 
-theorem l_u_le (a) : l (u a) ≤ a :=
-  gc.l_le <| le_rfl
-
+@[to_dual]
 theorem monotone_u : Monotone u := fun a _ H => gc.le_u ((gc.l_u_le a).trans H)
 
-theorem monotone_l : Monotone l :=
-  gc.dual.monotone_u.dual
-
 /-- If `(l, u)` is a Galois connection, then the relation `x ≤ u (l y)` is a transitive relation.
 If `l` is a closure operator (`Submodule.span`, `Subgroup.closure`, ...) and `u` is the coercion to
 `Set`, this reads as "if `U` is in the closure of `V` and `V` is in the closure of `W` then `U` is
 in the closure of `W`". -/
+@[to_dual l_u_le_trans]
 theorem le_u_l_trans {x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z) :=
   hxy.trans (gc.monotone_u <| gc.l_le hyz)
 
-theorem l_u_le_trans {x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) : l (u x) ≤ z :=
-  (gc.monotone_l <| gc.le_u hxy).trans hyz
-
 end
 
 section PartialOrder
@@ -96,20 +94,25 @@ section PartialOrder
 variable [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)
 include gc
 
+@[to_dual]
 theorem u_l_u_eq_u (b : β) : u (l (u b)) = u b :=
   (gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _)
 
+@[to_dual]
 theorem u_l_u_eq_u' : u ∘ l ∘ u = u :=
   funext gc.u_l_u_eq_u
 
+@[to_dual]
 theorem u_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ a, l a = l' a)
     {b : β} : u b = u' b :=
   le_antisymm (gc'.le_u <| hl (u b) ▸ gc.l_u_le _) (gc.le_u <| (hl (u' b)).symm ▸ gc'.l_u_le _)
 
 /-- If there exists a `b` such that `a = u a`, then `b = l a` is one such element. -/
+@[to_dual /-- If there exists an `a` such that `b = l a`, then `a = u b` is one such element. -/]
 theorem exists_eq_u (a : α) : (∃ b : β, a = u b) ↔ a = u (l a) :=
   ⟨fun ⟨_, hS⟩ => hS.symm ▸ (gc.u_l_u_eq_u _).symm, fun HI => ⟨_, HI⟩⟩
 
+@[to_dual]
 theorem u_eq {z : α} {y : β} : u y = z ↔ ∀ x, x ≤ z ↔ l x ≤ y := by
   constructor
   · rintro rfl x
@@ -119,60 +122,29 @@ theorem u_eq {z : α} {y : β} : u y = z ↔ ∀ x, x ≤ z ↔ l x ≤ y := by
 
 end PartialOrder
 
-section PartialOrder
-
-variable [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)
-include gc
-
-theorem l_u_l_eq_l (a : α) : l (u (l a)) = l a := gc.dual.u_l_u_eq_u _
-
-theorem l_u_l_eq_l' : l ∘ u ∘ l = l := funext gc.l_u_l_eq_l
-
-theorem l_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hu : ∀ b, u b = u' b)
-    {a : α} : l a = l' a :=
-  gc.dual.u_unique gc'.dual hu
-
-/-- If there exists an `a` such that `b = l a`, then `a = u b` is one such element. -/
-theorem exists_eq_l (b : β) : (∃ a : α, b = l a) ↔ b = l (u b) := gc.dual.exists_eq_u _
-
-theorem l_eq {x : α} {z : β} : l x = z ↔ ∀ y, z ≤ y ↔ x ≤ u y := gc.dual.u_eq
-
-end PartialOrder
-
 section OrderTop
 
 variable [PartialOrder α] [Preorder β] [OrderTop α]
 
+@[to_dual]
 theorem u_eq_top {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : u x = ⊤ ↔ l ⊤ ≤ x :=
   top_le_iff.symm.trans gc.le_iff_le.symm
 
+@[to_dual]
 theorem u_top [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤ :=
   gc.u_eq_top.2 le_top
 
+@[to_dual]
 theorem u_l_top {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤ :=
   gc.u_eq_top.mpr le_rfl
 
 end OrderTop
 
-section OrderBot
-
-variable [Preorder α] [PartialOrder β] [OrderBot β]
-
-theorem l_eq_bot {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : l x = ⊥ ↔ x ≤ u ⊥ :=
-  gc.dual.u_eq_top
-
-theorem l_bot [OrderBot α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥ :=
-  gc.dual.u_top
-
-theorem l_u_bot {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l (u ⊥) = ⊥ :=
-  gc.l_eq_bot.mpr le_rfl
-
-end OrderBot
-
 section LinearOrder
 
 variable [LinearOrder α] [LinearOrder β] {l : α → β} {u : β → α}
 
+@[to_dual lt_iff_lt']
 theorem lt_iff_lt (gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a :=
   lt_iff_lt_of_le_iff_le (gc a b)
 
diff --git a/Mathlib/Order/Interval/Set/Defs.lean b/Mathlib/Order/Interval/Set/Defs.lean
index 34daa4956d3d48..d11c2f33a3c63f 100644
--- a/Mathlib/Order/Interval/Set/Defs.lean
+++ b/Mathlib/Order/Interval/Set/Defs.lean
@@ -32,52 +32,52 @@ namespace Set
 variable {α : Type*} [Preorder α] {a b x : α}
 
 /-- `Ioo a b` is the left-open right-open interval $(a, b)$. -/
+@[to_dual self (reorder := a b)]
 def Ioo (a b : α) := { x | a < x ∧ x < b }
 
-@[simp, grind =] theorem mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b := Iff.rfl
-theorem Ioo_def (a b : α) : { x | a < x ∧ x < b } = Ioo a b := rfl
+to_dual_insert_cast Ioo := by grind
+
+@[to_dual mem_Ioo', simp, grind =] theorem mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b := Iff.rfl
+@[to_dual Ioo_def'] theorem Ioo_def (a b : α) : { x | a < x ∧ x < b } = Ioo a b := rfl
 
 /-- `Ico a b` is the left-closed right-open interval $[a, b)$. -/
 def Ico (a b : α) := { x | a ≤ x ∧ x < b }
 
-@[simp, grind =] theorem mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b := Iff.rfl
-theorem Ico_def (a b : α) : { x | a ≤ x ∧ x < b } = Ico a b := rfl
+/-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
+@[to_dual existing (reorder := a b)]
+def Ioc (a b : α) := { x | a < x ∧ x ≤ b }
 
-/-- `Iio b` is the left-infinite right-open interval $(-∞, b)$. -/
-def Iio (b : α) := { x | x < b }
+to_dual_insert_cast Ico := by grind
+to_dual_insert_cast Ioc := by grind
 
-@[simp, grind =] theorem mem_Iio : x ∈ Iio b ↔ x < b := Iff.rfl
-theorem Iio_def (a : α) : { x | x < a } = Iio a := rfl
+@[to_dual mem_Ioc', simp, grind =] theorem mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b := Iff.rfl
+@[to_dual Ioc_def'] theorem Ico_def (a b : α) : { x | a ≤ x ∧ x < b } = Ico a b := rfl
+
+@[to_dual mem_Ico', simp, grind =] theorem mem_Ioc : x ∈ Ioc a b ↔ a < x ∧ x ≤ b := Iff.rfl
+@[to_dual Ico_def'] theorem Ioc_def (a b : α) : { x | a < x ∧ x ≤ b } = Ioc a b := rfl
 
 /-- `Icc a b` is the left-closed right-closed interval $[a, b]$. -/
+@[to_dual self (reorder := a b)]
 def Icc (a b : α) := { x | a ≤ x ∧ x ≤ b }
 
-@[simp, grind =] theorem mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b := Iff.rfl
-theorem Icc_def (a b : α) : { x | a ≤ x ∧ x ≤ b } = Icc a b := rfl
-
-/-- `Iic b` is the left-infinite right-closed interval $(-∞, b]$. -/
-def Iic (b : α) := { x | x ≤ b }
-
-@[simp, grind =] theorem mem_Iic : x ∈ Iic b ↔ x ≤ b := Iff.rfl
-theorem Iic_def (b : α) : { x | x ≤ b } = Iic b := rfl
+to_dual_insert_cast Icc := by grind
 
-/-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
-def Ioc (a b : α) := { x | a < x ∧ x ≤ b }
+@[to_dual mem_Icc', simp, grind =] theorem mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b := Iff.rfl
+@[to_dual Icc_def'] theorem Icc_def (a b : α) : { x | a ≤ x ∧ x ≤ b } = Icc a b := rfl
 
-@[simp, grind =] theorem mem_Ioc : x ∈ Ioc a b ↔ a < x ∧ x ≤ b := Iff.rfl
-theorem Ioc_def (a b : α) : { x | a < x ∧ x ≤ b } = Ioc a b := rfl
-
-/-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/
-def Ici (a : α) := { x | a ≤ x }
+/-- `Iio b` is the left-infinite right-open interval $(-∞, b)$. -/
+@[to_dual /-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/]
+def Iio (b : α) := { x | x < b }
 
-@[simp, grind =] theorem mem_Ici : x ∈ Ici a ↔ a ≤ x := Iff.rfl
-theorem Ici_def (a : α) : { x | a ≤ x } = Ici a := rfl
+@[to_dual (attr := simp, grind =)] theorem mem_Iio : x ∈ Iio b ↔ x < b := Iff.rfl
+@[to_dual] theorem Iio_def (a : α) : { x | x < a } = Iio a := rfl
 
-/-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/
-def Ioi (a : α) := { x | a < x }
+/-- `Iic b` is the left-infinite right-closed interval $(-∞, b]$. -/
+@[to_dual /-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/]
+def Iic (b : α) := { x | x ≤ b }
 
-@[simp, grind =] theorem mem_Ioi : x ∈ Ioi a ↔ a < x := Iff.rfl
-theorem Ioi_def (a : α) : { x | a < x } = Ioi a := rfl
+@[to_dual (attr := simp, grind =)] theorem mem_Iic : x ∈ Iic b ↔ x ≤ b := Iff.rfl
+@[to_dual] theorem Iic_def (b : α) : { x | x ≤ b } = Iic b := rfl
 
 /-- We say that a set `s : Set α` is `OrdConnected` if for all `x y ∈ s` it includes the
 interval `[[x, y]]`. If `α` is a `DenselyOrdered` `ConditionallyCompleteLinearOrder` with
@@ -87,4 +87,6 @@ class OrdConnected (s : Set α) : Prop where
   /-- `s : Set α` is `OrdConnected` if for all `x y ∈ s` it includes the interval `[[x, y]]`. -/
   out' ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : Icc x y ⊆ s
 
+attribute [to_dual self (reorder := x y, hx hy)] OrdConnected.out'
+
 end Set
diff --git a/Mathlib/Order/Monotone/Defs.lean b/Mathlib/Order/Monotone/Defs.lean
index 5e3e672555f466..a27f5712ec099b 100644
--- a/Mathlib/Order/Monotone/Defs.lean
+++ b/Mathlib/Order/Monotone/Defs.lean
@@ -63,36 +63,52 @@ variable [Preorder α] [Preorder β]
 def Monotone (f : α → β) : Prop :=
   ∀ ⦃a b⦄, a ≤ b → f a ≤ f b
 
+to_dual_insert_cast Monotone := by grind
+
 /-- A function `f` is antitone if `a ≤ b` implies `f b ≤ f a`. -/
 def Antitone (f : α → β) : Prop :=
   ∀ ⦃a b⦄, a ≤ b → f b ≤ f a
 
+to_dual_insert_cast Antitone := by grind
+
 /-- A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`. -/
 def MonotoneOn (f : α → β) (s : Set α) : Prop :=
   ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a ≤ b → f a ≤ f b
 
+to_dual_insert_cast MonotoneOn := by grind
+
 /-- A function `f` is antitone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a`. -/
 def AntitoneOn (f : α → β) (s : Set α) : Prop :=
   ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a ≤ b → f b ≤ f a
 
+to_dual_insert_cast AntitoneOn := by grind
+
 /-- A function `f` is strictly monotone if `a < b` implies `f a < f b`. -/
 def StrictMono (f : α → β) : Prop :=
   ∀ ⦃a b⦄, a < b → f a < f b
 
+to_dual_insert_cast StrictMono := by grind
+
 /-- A function `f` is strictly antitone if `a < b` implies `f b < f a`. -/
 def StrictAnti (f : α → β) : Prop :=
   ∀ ⦃a b⦄, a < b → f b < f a
 
+to_dual_insert_cast StrictAnti := by grind
+
 /-- A function `f` is strictly monotone on `s` if, for all `a, b ∈ s`, `a < b` implies
 `f a < f b`. -/
 def StrictMonoOn (f : α → β) (s : Set α) : Prop :=
   ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f a < f b
 
+to_dual_insert_cast StrictMonoOn := by grind
+
 /-- A function `f` is strictly antitone on `s` if, for all `a, b ∈ s`, `a < b` implies
 `f b < f a`. -/
 def StrictAntiOn (f : α → β) (s : Set α) : Prop :=
   ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f b < f a
 
+to_dual_insert_cast StrictAntiOn := by grind
+
 end MonotoneDef
 
 section Decidable
@@ -126,6 +142,7 @@ section Preorder
 
 variable [Preorder α]
 
+@[to_dual self]
 theorem Monotone.comp_le_comp_left
     [Preorder β] {f : β → α} {g h : γ → β} (hf : Monotone f) (le_gh : g ≤ h) :
     LE.le.{max w u} (f ∘ g) (f ∘ h) :=
@@ -167,16 +184,19 @@ when you do not want to apply a `Monotone` assumption (i.e. your goal is `a ≤
 However if you find yourself writing `hf.imp h`, then you should have written `hf h` instead.
 -/
 
-
+@[to_dual self]
 theorem Monotone.imp (hf : Monotone f) (h : a ≤ b) : f a ≤ f b :=
   hf h
 
+@[to_dual self]
 theorem Antitone.imp (hf : Antitone f) (h : a ≤ b) : f b ≤ f a :=
   hf h
 
+@[to_dual self]
 theorem StrictMono.imp (hf : StrictMono f) (h : a < b) : f a < f b :=
   hf h
 
+@[to_dual self]
 theorem StrictAnti.imp (hf : StrictAnti f) (h : a < b) : f b < f a :=
   hf h
 
@@ -224,19 +244,23 @@ section PartialOrder
 
 variable [PartialOrder α] [Preorder β] {f : α → β} {s : Set α}
 
+@[to_dual monotone_iff_forall_lt']
 theorem monotone_iff_forall_lt : Monotone f ↔ ∀ ⦃a b⦄, a < b → f a ≤ f b :=
   forall₂_congr fun _ _ ↦
     ⟨fun hf h ↦ hf h.le, fun hf h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) hf⟩
 
+@[to_dual antitone_iff_forall_lt']
 theorem antitone_iff_forall_lt : Antitone f ↔ ∀ ⦃a b⦄, a < b → f b ≤ f a :=
   forall₂_congr fun _ _ ↦
     ⟨fun hf h ↦ hf h.le, fun hf h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).ge) hf⟩
 
+@[to_dual monotoneOn_iff_forall_lt']
 theorem monotoneOn_iff_forall_lt :
     MonotoneOn f s ↔ ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f a ≤ f b :=
   ⟨fun hf _ ha _ hb h ↦ hf ha hb h.le,
    fun hf _ ha _ hb h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) (hf ha hb)⟩
 
+@[to_dual antitoneOn_iff_forall_lt']
 theorem antitoneOn_iff_forall_lt :
     AntitoneOn f s ↔ ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f b ≤ f a :=
   ⟨fun hf _ ha _ hb h ↦ hf ha hb h.le,
@@ -318,6 +342,7 @@ theorem strictAnti_of_le_iff_le [Preorder α] [Preorder β] {f : α → β}
     (h : ∀ x y, x ≤ y ↔ f y ≤ f x) : StrictAnti f :=
   fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1
 
+@[to_dual of_lt_imp_ne']
 theorem Function.Injective.of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
     Injective f := by
   grind [Injective]
@@ -444,16 +469,20 @@ variable [Preorder β] {f : α → β} {s : Set α}
 
 open Ordering
 
+@[to_dual self]
 theorem Monotone.reflect_lt (hf : Monotone f) {a b : α} (h : f a < f b) : a < b :=
   lt_of_not_ge fun h' ↦ h.not_ge (hf h')
 
+@[to_dual self]
 theorem Antitone.reflect_lt (hf : Antitone f) {a b : α} (h : f a < f b) : b < a :=
   lt_of_not_ge fun h' ↦ h.not_ge (hf h')
 
+@[to_dual self (reorder := a b, ha hb)]
 theorem MonotoneOn.reflect_lt (hf : MonotoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s)
     (h : f a < f b) : a < b :=
   lt_of_not_ge fun h' ↦ h.not_ge <| hf hb ha h'
 
+@[to_dual self (reorder := a b, ha hb)]
 theorem AntitoneOn.reflect_lt (hf : AntitoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s)
     (h : f a < f b) : b < a :=
   lt_of_not_ge fun h' ↦ h.not_ge <| hf ha hb h'
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 4c45aa1547271a..cf4d1d4f6d5e48 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -299,6 +299,7 @@ public import Mathlib.Tactic.Translate.Core
 public import Mathlib.Tactic.Translate.GuessName
 public import Mathlib.Tactic.Translate.ToAdditive
 public import Mathlib.Tactic.Translate.ToDual
+public import Mathlib.Tactic.Translate.UnfoldBoundary
 public import Mathlib.Tactic.TryThis
 public import Mathlib.Tactic.TypeCheck
 public import Mathlib.Tactic.TypeStar
diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean
index 15ef2fd9e98a74..26a9c4ff0f2e37 100644
--- a/Mathlib/Tactic/ToDual.lean
+++ b/Mathlib/Tactic/ToDual.lean
@@ -17,20 +17,8 @@ public meta section
 
 attribute [to_dual self (reorder := 3 4)] LE.le LT.lt GE.ge GT.gt
 
-/-
-`DecidableLT` is defined as `∀ a b : α, Decidable (a < b)`, which is dual to
-`∀ a b : α, Decidable (b < a)`. Translations given by `to_dual` need to satisfy the
-property that if `e₁` is defEq to `e₂`, then the dual of `e₁` needs to be defEq to
-the dual of `e₂`. Hence, the translation of `DecidableLT` needs to be defEq to
-`∀ a b : α, Decidable (b < a)`. So, we define `DecidableLT'` to be this.
-
-`DecidableLT'` is not definitionally the same as `DecidableLT`, but for type class search
-the two are identical. So although this is a bit annoying, it is not a big problem.
--/
-attribute [to_dual DecidableLT' /-- `DecidableLT'` is equivalent to `DecidableLT`.
-It is used by `@[to_dual]` in order to deal with `DecidableLT`. -/] DecidableLT
-attribute [to_dual DecidableLE' /-- `DecidableLE'` is equivalent to `DecidableLE`.
-It is used by `@[to_dual]` in order to deal with `DecidableLE`. -/] DecidableLE
+to_dual_insert_cast_fun DecidableLE := fun inst a b ↦ inst b a, fun inst a b ↦ inst b a
+to_dual_insert_cast_fun DecidableLT := fun inst a b ↦ inst b a, fun inst a b ↦ inst b a
 
 attribute [to_dual_do_translate] Empty PEmpty Unit PUnit
 
diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index 66bda9e7e950c0..a80063a23288be 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -20,6 +20,7 @@ public import Batteries.Tactic.Trans
 public import Mathlib.Tactic.Eqns
 public import Mathlib.Tactic.Simps.Basic
 public import Mathlib.Tactic.Translate.GuessName
+public import Mathlib.Tactic.Translate.UnfoldBoundary
 public meta import Mathlib.Util.MemoFix
 
 /-!
@@ -203,6 +204,11 @@ structure TranslateData : Type where
     translated thanks to this, you generally have to specify the translated name manually.
   -/
   doTranslateAttr : NameMapExtension Bool
+  /-- The `dont_unfold` attribute is used to create an abstraction boundary for the tagged constant
+  when translating it. For example, `Set.Icc`, `Monotone`, `DecidableLT`, `WCovBy` are all
+  morally self-dual, but their definition is not self-dual. So, in order to allow these constants
+  to be self-dual, we need to not unfold their definition in the proof term that we translate. -/
+  unfoldBoundaries? : Option UnfoldBoundary.UnfoldBoundaryExt := none
   /-- `translations` stores all of the constants that have been tagged with this attribute,
   and maps them to their translation. -/
   translations : NameMapExtension Name
@@ -549,11 +555,20 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
   let mut decl := srcDecl.updateName tgt
   if reorder.any (·.contains 0) then
     decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
-  decl := decl.updateType <| ← reorderForall reorder <| ← applyReplacementForall t dont <|
-    renameBinderNames t decl.type
-  if let some v := decl.value? (allowOpaque := true) then
-    decl := decl.updateValue <| ← reorderLambda reorder <| ← applyReplacementLambda t dont v
-  return decl
+  let mut value := decl.value! (allowOpaque := true)
+  if let some b := t.unfoldBoundaries? then
+    value ← b.cast (← b.insertBoundaries value t.attrName) decl.type t.attrName
+  value ← reorderLambda reorder <| ← applyReplacementLambda t dont value
+  if let some b := t.unfoldBoundaries? then
+    value ← b.unfoldInsertions value
+  decl := decl.updateValue value
+  let mut type := decl.type
+  if let some b := t.unfoldBoundaries? then
+    type ← b.insertBoundaries decl.type t.attrName
+  type ← reorderForall reorder <| ← applyReplacementForall t dont <| renameBinderNames t type
+  if let some b := t.unfoldBoundaries? then
+    type ← b.unfoldInsertions type
+  return decl.updateType type
 
 /--
 Find the argument of `nm` that appears in the first translatable (type-class) argument.
@@ -888,7 +903,10 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
   unless srcDecl.levelParams.length == tgtDecl.levelParams.length do
     throwError "`{t.attrName}` validation failed:\n  expected {srcDecl.levelParams.length} \
       universe levels, but '{tgt}' has {tgtDecl.levelParams.length} universe levels"
-  let srcType ← applyReplacementForall t cfg.dontTranslate srcDecl.type
+  let mut srcType := srcDecl.type
+  if let some b := t.unfoldBoundaries? then
+    srcType ← b.insertBoundaries srcType t.attrName
+  srcType ← applyReplacementForall t cfg.dontTranslate srcType
   let reorder' := guessReorder srcType tgtDecl.type
   trace[translate_detail] "The guessed reorder is {reorder'}"
   let reorder ←
@@ -910,12 +928,14 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
       Please remove the attribute, or provide an explicit `(reorder := ...)` argument.\n\
       If you need to give a hint to `{t.attrName}` to translate expressions involving `{src}`,\n\
       use `{t.attrName}_do_translate` instead"
-  let srcType ← reorderForall reorder srcType
+  srcType ← reorderForall reorder srcType
+  if let some b := t.unfoldBoundaries? then
+    srcType ← b.unfoldInsertions srcType
   if reorder.any (·.contains 0) then
     srcDecl := srcDecl.updateLevelParams srcDecl.levelParams.swapFirstTwo
   -- instantiate both types with the same universes. `instantiateLevelParams` does some
   -- normalization, so we apply it to both types.
-  let srcType := srcType.instantiateLevelParams
+  srcType := srcType.instantiateLevelParams
     srcDecl.levelParams (tgtDecl.levelParams.map mkLevelParam)
   let tgtType := tgtDecl.type.instantiateLevelParams
     tgtDecl.levelParams (tgtDecl.levelParams.map mkLevelParam)
diff --git a/Mathlib/Tactic/Translate/TagUnfoldBoundary.lean b/Mathlib/Tactic/Translate/TagUnfoldBoundary.lean
new file mode 100644
index 00000000000000..d5107dc16fc56e
--- /dev/null
+++ b/Mathlib/Tactic/Translate/TagUnfoldBoundary.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2025 Jovan Gerbscheid. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jovan Gerbscheid
+-/
+module
+
+public import Mathlib.Tactic.Translate.Core
+
+/-!
+# Tagging of unfold boundaries for translation attributes
+
+The file `Mathlib.Tactic.Translate.UnfoldBoundary` defines how to add unfold boundaries in terms.
+In this file, we define the infrastructure for tagging declaration to be used for that.
+This is in a separate file, because we needs to import `Mathlib.Tactic.Translate.Core` here.
+-/
+
+meta section
+
+namespace Mathlib.Tactic.Translate
+
+open Lean Meta Elab Command Term UnfoldBoundary
+
+inductive CastKind where
+  | eq | unfoldFun | refoldFun
+
+def CastKind.mkRel (lhs body : Expr) : CastKind → MetaM Expr
+  | .eq => mkEq lhs body
+  | .unfoldFun => return .forallE `_ lhs body .default
+  | .refoldFun => return .forallE `_ body lhs .default
+
+def CastKind.mkProof (lhs : Expr) : CastKind → MetaM Expr
+  | .eq => mkEqRefl lhs
+  | _ => return .lam `_ lhs (.bvar 0) .default
+
+def elabInsertCastAux (declName : Name) (castKind : CastKind) (stx : Term) (t : TranslateData) :
+    CommandElabM (Name × Name) :=
+  Command.liftTermElabM do withDeclNameForAuxNaming declName do withExporting do
+  let info ← getConstInfoDefn declName
+  lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+    let addDecl name type value : MetaM Unit := do
+      let type ← mkForallFVars xs type
+      let value ← mkLambdaFVars xs value
+      addDecl <| ←
+        if castKind matches .eq then
+          mkThmOrUnsafeDef { name, type, value, levelParams := info.levelParams }
+        else
+          .defnDecl <$> mkDefinitionValInferringUnsafe name info.levelParams type value .opaque
+    let lhs := mkAppN (.const info.name <| info.levelParams.map mkLevelParam) xs
+    let name ← mkAuxDeclName (t.attrName.appendAfter "_cast")
+    addDecl name (← castKind.mkRel lhs body) (← castKind.mkProof lhs)
+
+    let newLhs ← applyReplacementFun t lhs
+    let newBody ← applyReplacementFun t body
+    let newType ← castKind.mkRel newLhs newBody
+    -- Make the goal easier to prove by unfolding the new lhs
+    let newType' ← castKind.mkRel ((← unfoldDefinition? newLhs).getD newLhs) newBody
+    let newValue ← elabTermEnsuringType stx newType' <* synthesizeSyntheticMVarsNoPostponing
+    let newName ← mkAuxDeclName (t.attrName.appendAfter "_cast")
+    addDecl newName newType (← instantiateMVars newValue)
+
+    let relevantArg? := (t.argInfoAttr.find? (← getEnv) declName).map (·.relevantArg)
+    _ ← addTranslationAttr t name
+      { tgt := newName, existing := true, ref := .missing, relevantArg? }
+    return (name, newName)
+
+/-- The `insert_cast foo := ...` command should be used when the translation of some
+definition `foo` is not definitionally equal to the translation of its value.
+It requires a proof that these two are equal, which `by grind` can usually prove.
+
+The command internally generates an unfolding theorem for `foo`, and a dual of this theorem.
+When type checking a term requires the definition `foo` to be unfolded, then in order to translate
+that term, a `cast` is first inserted into the term using this unfolding theorem.
+As a result, type checking the term won't anymore require unfolding `foo`, so the term
+can be safely translated. -/
+public def elabInsertCast (declName : Ident) (valStx : Term) (t : TranslateData) :
+    CommandElabM Unit := do
+  let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
+  let (name, _) ← elabInsertCastAux declName .eq valStx t
+  let some { unfolds, .. } := t.unfoldBoundaries?
+    | throwError "{t.attrName} doesn't support unfold boundaries"
+  unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true }
+
+/-- The `insert_cast_fun foo := ..., ...` command should be used when the translation of some
+type `foo` is not definitionally equal to the translation of its value.
+It requires a dual of the function that unfolds `foo` and of the function that refolds `foo`.
+
+The command internally generates these unfold/refold functions for `foo`, and their duals.
+If type checking a term requires the definition `foo` to be unfolded, then before translating
+that term, the unfold/refold function is inserted into the term.
+As a result, type checking the term won't anymore require unfolding `foo`, so the term
+can be safely translated. After translating, the unfold/refold functions are again unfolded. -/
+public def elabInsertCastFun (declName : Ident) (valStx₁ valStx₂ : Term) (t : TranslateData) :
+    CommandElabM Unit := do
+  let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
+  let (name₁, dualName₁) ← elabInsertCastAux declName .unfoldFun valStx₁ t
+  let (name₂, dualName₂) ← elabInsertCastAux declName .refoldFun valStx₂ t
+  let some { casts, insertionFuns, .. } := t.unfoldBoundaries?
+    | throwError "{t.attrName} doesn't support unfold boundaries"
+  casts.add declName (name₁, name₂)
+  insertionFuns.add name₁ (); insertionFuns.add dualName₁ ()
+  insertionFuns.add name₂ (); insertionFuns.add dualName₂ ()
+
+end Mathlib.Tactic.Translate
diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index 5b25f5b99a2818..029c5c018b3dde 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -5,7 +5,7 @@ Authors: Jovan Gerbscheid, Bryan Gin-ge Chen
 -/
 module
 
-public import Mathlib.Tactic.Translate.Core
+public import Mathlib.Tactic.Translate.TagUnfoldBoundary
 
 /-!
 # The `@[to_dual]` attribute.
@@ -26,7 +26,7 @@ Known limitations:
 public meta section
 
 namespace Mathlib.Tactic.ToDual
-open Lean Meta Elab Command Std Translate
+open Lean Meta Elab Term Command Std Translate UnfoldBoundary
 
 @[inherit_doc TranslateData.ignoreArgsAttr]
 syntax (name := to_dual_ignore_args) "to_dual_ignore_args" (ppSpace num)* : attr
@@ -83,9 +83,19 @@ Use the `(attr := ...)` syntax to apply attributes to both the original and the
 @[to_dual (attr := simp)] lemma min_self (a : α) : min a a = a := sorry
 ```
 
-When troubleshooting, you can see what `to_dual` is doing by replacing it with `to_dual?` and/or
+Some definitions are dual to something other than the dual of their value. Some examples:
+- `Ico a b := { x | a ≤ x ∧ x < b }` is dual to `Ioc b a := { x | b < x ∧ x ≤ a }`.
+- `Monotone f := ∀ ⦃a b⦄, a ≤ b → f a ≤ f b` is dual to itself.
+- `DecidableLE α := ∀ a b : α, Decidable (a ≤ b)` is dual to itself.
+
+To be able to translate a term involfing such constants, `to_dual` needs to insert casts,
+so that the term's correctness doesn't rely on unfolding them.
+You can instruct `to_dual` to do this using the `to_dual_insert_cast` or `to_dual_insert_cast_fun`
+commands.
+
+When troubleshooting `to_dual`, you can see what it is doing by replacing it with `to_dual?` and/or
 by using `set_option trace.translate_detail true`.
- -/
+-/
 syntax (name := to_dual) "to_dual" "?"? attrArgs : attr
 
 @[inherit_doc to_dual]
@@ -103,6 +113,18 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
           | _ => throwUnsupportedSyntax
         return ids.toList }
 
+@[inherit_doc UnfoldBoundaryExt.unfolds]
+initialize unfolds : NameMapExtension SimpTheorem ← registerNameMapExtension _
+
+@[inherit_doc UnfoldBoundaryExt.casts]
+initialize casts : NameMapExtension (Name × Name) ← registerNameMapExtension _
+
+@[inherit_doc UnfoldBoundaryExt.insertionFuns]
+initialize insertionFuns : NameMapExtension Unit ← registerNameMapExtension _
+
+@[inherit_doc TranslateData.unfoldBoundaries?]
+def unfoldBoundaries? : Option UnfoldBoundaryExt := some { unfolds, casts, insertionFuns }
+
 @[inherit_doc TranslateData.argInfoAttr]
 initialize argInfoAttr : NameMapExtension ArgInfo ← registerNameMapExtension _
 
@@ -140,6 +162,14 @@ def nameDict : Std.HashMap String (List String) := .ofList [
   ("upper", ["Lower"]),
   ("succ", ["Pred"]),
   ("pred", ["Succ"]),
+  ("ico", ["Ioc"]),
+  ("ioc", ["Ico"]),
+  ("iio", ["Ioi"]),
+  ("ioi", ["Iio"]),
+  ("ici", ["Iic"]),
+  ("iic", ["Ici"]),
+  ("u", ["L"]),
+  ("l", ["U"]),
   ("disjoint", ["Codisjoint"]),
   ("codisjoint", ["Disjoint"]),
 
@@ -191,12 +221,20 @@ def abbreviationDict : Std.HashMap String String := .ofList [
 
 /-- The bundle of environment extensions for `to_dual` -/
 def data : TranslateData where
-  ignoreArgsAttr; argInfoAttr; doTranslateAttr; translations
+  ignoreArgsAttr; argInfoAttr; doTranslateAttr; unfoldBoundaries?; translations
   attrName := `to_dual
   changeNumeral := false
   isDual := true
   guessNameData := { nameDict, abbreviationDict }
 
+@[inherit_doc Translate.elabInsertCast]
+elab "to_dual_insert_cast" declName:ident " := " valStx:term : command =>
+  elabInsertCast declName valStx data
+
+@[inherit_doc elabInsertCastFun]
+elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command =>
+  elabInsertCastFun declName valStx₁ valStx₂ data
+
 initialize registerBuiltinAttribute {
     name := `to_dual
     descr := "Transport to dual"
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
new file mode 100644
index 00000000000000..4b0166fbfdaebd
--- /dev/null
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2025 Jovan Gerbscheid. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jovan Gerbscheid
+-/
+module
+
+public meta import Lean.Meta.Tactic.Delta
+public import Batteries.Lean.NameMapAttribute
+public import Mathlib.Init
+
+/-!
+# Modify proof terms so that they don't rely on unfolding certain constants
+
+This file defines a procedure for inserting casts into (proof) terms in order to make them
+well typed in a setting where certain constants aren't allowed to be unfolded.
+
+We make use of `withCanUnfoldPred` in order to modify which constants can and cannot be unfolded.
+This way, `whnf` and `isDefEq` do not unfold these constants.
+
+So, the procedure is to check that an expression is well typed, analogous to `Meta.check`,
+and at each type mismatch, we try to insert a cast.
+
+There are two kinds of casts:
+- Equality casts. This is for propositions and terms,
+  where it is possible to prove that one is equal to the other. For example `Monotone`.
+- Explicit casting functions, both for unfolding and refolding. This is for types, where we
+  cannot express their equivalence with an equality. For example `DecidableLE`.
+-/
+
+meta section
+
+namespace Mathlib.Tactic.UnfoldBoundary
+
+open Lean Meta
+
+structure UnfoldBoundaries where
+  /-- For propositions and terms of types, we store a rewrite theorem that unfolds it. -/
+  unfolds : NameMap SimpTheorem
+  /-- For types, we store a cast for translating from and to the type respectively. -/
+  casts : NameMap (Name × Name)
+  /-- The functions that we want to unfold again after the translation has happened. -/
+  insertionFuns : NameMap Unit
+
+/--
+Set up the monadic context:
+- Set the transparency to `.all`, just like is done in `Meta.check`.
+- Use `withCanUnfoldPred` to not allow unfolding the constants for which we want to insert casts.
+- Set up the `SimpM` context so that `Simp.simp` will unfold constants from `b.unfolds`.
+-/
+def run {α} (b : UnfoldBoundaries) (x : SimpM α) : MetaM α :=
+  withCanUnfoldPred (fun _ i => return !b.unfolds.contains i.name && !b.casts.contains i.name) do
+  withTransparency .all do
+  let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
+  x (Simp.Methods.toMethodsRef { pre }) ctx |>.run' {}
+where
+  pre (e : Expr) : SimpM Simp.Step := do
+    let .const c _ ← whnf e.getAppFn | return .continue
+    let some thm := b.unfolds.find? c | return .continue
+    let some r ← Simp.tryTheorem? e thm | return .continue
+    return .visit r
+
+/-- Given a term `e`, add casts to it to unfold constants appearing in it. -/
+partial def unfoldConsts (b : UnfoldBoundaries) (e : Expr) : SimpM Expr := do
+  let eType ← inferType e
+  let e ← do
+    let { expr, proof? := some proof } ← Simp.simp eType | pure e
+    trace[translate_detail] "unfoldConsts: added a cast from {eType} to {expr}"
+    mkAppOptM ``cast #[eType, expr, proof, e]
+  let eTypeWhnf ← whnf (← inferType e)
+  if let .const c us := eTypeWhnf.getAppFn then
+    if let some (cast, _) := b.casts.find? c then
+      let e := .app (mkAppN (.const cast us) eTypeWhnf.getAppArgs) e
+      trace[translate_detail] "unfoldConsts: created the cast {e} to unfold {.ofConstName c}"
+      return ← unfoldConsts b e
+  return e
+
+/-- Given a term `e` which we want to get to have type `expectedType`, return a term of type
+`expectedType` by adding cast to `e` that unfold constants in `expectedType`. -/
+partial def refoldConsts (b : UnfoldBoundaries) (e expectedType : Expr) : SimpM Expr := do
+  let goal ← mkFreshExprMVar expectedType
+  go e goal.mvarId!
+  instantiateMVars goal
+where
+  go (e : Expr) (goal : MVarId) : SimpM Unit := do
+    let goal ← do
+      let { expr, proof? := some proof } ← Simp.simp (← goal.getType) | pure goal
+      trace[translate_detail] "refoldConsts: added a cast from {← goal.getType} to {expr}"
+      goal.replaceTargetEq expr proof
+    forallTelescope (← goal.getType) fun xs tgt => do
+      let tgt ← whnf tgt
+      if let .const c us := tgt.getAppFn then
+        if let some (_, cast) := b.casts.find? c then
+          let cast := mkAppN (.const cast us) tgt.getAppArgs
+          trace[translate_detail] "refoldConsts: created the cast {cast} to unfold {.ofConstName c}"
+          let .forallE _ α _ _ ← inferType cast | throwError "refoldConsts: not a function\n{cast}"
+          let goal' ← mkFreshExprMVar α
+          go (e.beta xs) goal'.mvarId!
+          goal.assign <| ← mkLambdaFVars xs <| .app cast goal'
+          return
+      unless ← isDefEq (← goal.getType) (← inferType e) do
+        throwError "{e} : {← inferType e} does not have type {← goal.getType}."
+      goal.assign e
+
+/-- Given an expression `e` with expected type `expectedType`, if `e` doesn't have that type,
+use a cast to turn `e` into that type. -/
+def mkCast (b : UnfoldBoundaries) (e expectedType : Expr) : SimpM Expr := do
+  if ← isDefEq (← inferType e) expectedType then
+    return e
+  let e ← unfoldConsts b e
+  refoldConsts b e expectedType
+
+/-- Create the application `.app f a`, inserting some casts if necessary. -/
+def mkAppWithCast (b : UnfoldBoundaries) (f a : Expr) : SimpM Expr :=
+  try
+    checkApp f a
+    return f.app a
+  catch _ =>
+    let f ← unfoldConsts b f
+    let .forallE _ d _ _ ← whnf (← inferType f) | throwFunctionExpected f
+    return f.app (← mkCast b a d)
+
+/-- Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded. -/
+public structure UnfoldBoundaryExt where
+  /-- The `insert_cast` attribute is used to tag declarations `foo` that should not be unfolded in
+  a proof that is translated. Instead, a rewrite with an equality theorem is inserted.
+  This equality theorem can then be translated by the translation attribute. -/
+  unfolds : NameMapExtension SimpTheorem
+  /-- The `insert_cast_fun` attribute is used to tag types that should not be unfolded in a proof
+  that is translated. Instead, a casting function is inserted. This casting function then may be
+  translated by the translation attribute. -/
+  casts : NameMapExtension (Name × Name)
+  /-- `insertionFuns` stores the functions that may end up in an expression after inserting casts
+  and applying the translation. -/
+  insertionFuns : NameMapExtension Unit
+
+def UnfoldBoundaryExt.toUnfoldBoundaries (b : UnfoldBoundaryExt) : CoreM UnfoldBoundaries := do
+  let env ← getEnv
+  return {
+    unfolds := b.unfolds.getState env
+    casts := b.casts.getState env
+    insertionFuns := b.insertionFuns.getState env }
+
+/-- Modify `e` so that it has type `expectedType` if the constants in `b` cannot be unfolded. -/
+public def UnfoldBoundaryExt.cast (b : UnfoldBoundaryExt) (e expectedType : Expr) (attr : Name) :
+    MetaM Expr := do
+  let b ← b.toUnfoldBoundaries
+  run b <|
+  try
+    mkCast b e expectedType
+  catch ex =>
+    throwError "@[{attr}] failed to insert a cast to make `{e}` \
+      have type `{expectedType}`\n\n{ex.toMessageData}"
+
+/-- Modify `e` so that it is well typed if the constants in `b` cannot be unfolded.
+
+Note: it may be that `e` contains some constant whose type is not well typed in this setting.
+We don't make an effort to replace such constants.
+It seems that this approximation works well enough. -/
+public def UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Expr) (attr : Name) :
+    MetaM Expr := do
+  let b ← b.toUnfoldBoundaries
+  run b <| transform e (post := fun e ↦ e.withApp fun f args =>
+    try
+      return .done <| ← args.foldlM (mkAppWithCast b) f
+    catch ex =>
+      throwError "@[{attr}] failed to insert a cast to make `{f}` applied to `{args.toList}` \
+        well typed\n\n{ex.toMessageData}")
+
+/-- Unfold all of the auxiliary functions that were inserted as unfold boundaries. -/
+public def UnfoldBoundaryExt.unfoldInsertions (e : Expr) (b : UnfoldBoundaryExt) : CoreM Expr := do
+  let b ← b.toUnfoldBoundaries
+  -- This is the same as `Meta.deltaExpand`, but with an extra beta reduction.
+  Core.transform e fun e => do
+    if let some e ← delta? e b.insertionFuns.contains then
+      return .visit (headBetaBody e)
+    return .continue
+where
+  headBetaBody (e : Expr) : Expr :=
+    if let .lam _ d b bi := e then
+      e.updateLambda! bi d (headBetaBody b)
+    else
+      e.headBeta
+
+end Mathlib.Tactic.UnfoldBoundary
diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean
index 363579295ea289..8a4ed219e84f79 100644
--- a/MathlibTest/ToDual.lean
+++ b/MathlibTest/ToDual.lean
@@ -142,3 +142,77 @@ info: fun {α} [PartialOrder α] => of_eq_true (Eq.trans (forall_congr fun a =>
 run_meta
   Lean.logInfo (← Lean.getConstInfo ``lt_le_trans).value!
   Lean.logInfo (← Lean.getConstInfo ``le_refl').value!
+
+/-! Test the `to_dual_insert_cast` framework. -/
+
+@[to_dual lt_sum_eq_of_le']
+def lt_sum_eq_of_le [DecidableLE α] {a b : α} (hab : a ≤ b) :
+    a < b ⊕' a = b :=
+  if hba : b ≤ a then PSum.inr (le_antisymm hab hba) else PSum.inl (lt_of_le_not_ge hab hba)
+
+@[to_dual DecidableLE1_dual]
+def DecidableLE1 (h : ∀ a b : α, Decidable (a ≤ b)) : DecidableLE α := fun a b ↦ h a b
+
+@[to_dual DecidableLE2_dual]
+def DecidableLE2 (h : ∀ a b : α, Decidable (a ≤ b)) : DecidableLE α := id h
+
+-- Not yet supported because it probably won't show up in practice
+-- (though it wouldn't be too hard to fix `unfoldConsts` to support this)
+/--
+error: @[to_dual] failed to insert a cast to make `fun {α} [PartialOrder α] h =>
+  h` have type `{α : Type} → [inst : PartialOrder α] → DecidableLE α → (a b : α) → Decidable (a ≤ b)`
+
+fun {α} [PartialOrder α] h =>
+  h : {α : Type} →
+  [inst : PartialOrder α] →
+    DecidableLE α →
+      DecidableLE
+        α does not have type {α : Type} → [inst : PartialOrder α] → DecidableLE α → (a b : α) → Decidable (a ≤ b).
+-/
+#guard_msgs in
+@[to_dual DecidableLE3_dual]
+def DecidableLE3 (h : DecidableLE α) : ∀ a b : α, Decidable (a ≤ b) := h
+
+@[to_dual DecidableLE4_dual]
+def DecidableLE4 (h : DecidableLE α) (a b : α) : Decidable (a ≤ b) := h a b
+
+-- The arguments to `h` have been introduced, and swapped:
+/--
+info: fun {α} [PartialOrder α] h a b => h b a
+---
+info: fun {α} [PartialOrder α] h => id fun a b => h b a
+---
+info: fun {α} [PartialOrder α] h a b => h b a
+-/
+#guard_msgs in
+open Lean in
+run_meta
+  logInfo m!"{(← getConstInfo ``DecidableLE1_dual).value!}"
+  logInfo m!"{(← getConstInfo ``DecidableLE2_dual).value!}"
+  logInfo m!"{(← getConstInfo ``DecidableLE4_dual).value!}"
+
+-- The arguments to `inst✝` have been swapped:
+/--
+info: @dite (a < b ⊕' a = b) (b ≤ a) (inst✝ b a) (fun hba => PSum.inr ⋯) fun hba => PSum.inl ⋯
+---
+info: @dite (b < a ⊕' a = b) (a ≤ b) (inst✝ a b) (fun hba => PSum.inr ⋯) fun hba => PSum.inl ⋯
+-/
+#guard_msgs in
+open Lean Meta in
+run_meta
+  lambdaTelescope (← getConstInfo ``lt_sum_eq_of_le).value! fun _ => (logInfo m!"{·.setPPExplicit true}")
+  lambdaTelescope (← getConstInfo ``lt_sum_eq_of_le').value! fun _ => (logInfo m!"{·.setPPExplicit true}")
+
+/-- `Ico a b` is the left-closed right-open interval $[a, b)$. -/
+def Cov.Ico (a b : α) := fun x ↦ a ⩿ x ∧ x ⋖ b
+
+/-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
+@[to_dual existing (reorder := a b)]
+def Cov.Ioc (a b : α) := fun x ↦ a ⋖ x ∧ x ⩿ b
+
+to_dual_insert_cast Cov.Ico := by grind
+
+-- The dual theorems `mem_Ioc'` does not hold by reflexivity.
+-- To prove it, some rewrites have been added to the proof of `mem_Ico`.
+@[to_dual mem_Ioc']
+theorem mem_Ico {a b x : α} : Cov.Ico a b x ↔ (a ≤ x ∧ ∀ ⦃c⦄, a < c → ¬c < x) ∧ x ⋖ b := Iff.rfl