From 2f3869ee05bfa63c532b8fb095256222ac9c59c0 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Thu, 4 Dec 2025 19:13:31 +0000
Subject: [PATCH 01/26] feat: unfold-boundaries in `to_dual`

---
 Mathlib/Order/Basic.lean                     |   4 +-
 Mathlib/Order/Cover.lean                     |   6 +
 Mathlib/Order/Defs/LinearOrder.lean          |   7 +-
 Mathlib/Order/Defs/PartialOrder.lean         |  40 ++++-
 Mathlib/Order/Interval/Set/Defs.lean         |   9 +-
 Mathlib/Tactic/ToDual.lean                   |   6 +-
 Mathlib/Tactic/Translate/Core.lean           |  16 +-
 Mathlib/Tactic/Translate/ToDual.lean         |  40 ++++-
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 168 +++++++++++++++++++
 9 files changed, 272 insertions(+), 24 deletions(-)
 create mode 100644 Mathlib/Tactic/Translate/UnfoldBoundary.lean

diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index 0d7e1384fc51d8..668d38234a87d0 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -960,11 +960,11 @@ 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']
+@[to_dual self]
 instance decidableLE [Preorder α] [h : DecidableLE α] {p : α → Prop} :
     DecidableLE (Subtype p) := fun a b ↦ h a b
 
-@[to_dual decidableLT']
+@[to_dual self]
 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 27fabe39a35964..33d6351de4af63 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⟩
 
diff --git a/Mathlib/Order/Defs/LinearOrder.lean b/Mathlib/Order/Defs/LinearOrder.lean
index 016b642f0070bb..dfae076e589b7e 100644
--- a/Mathlib/Order/Defs/LinearOrder.lean
+++ b/Mathlib/Order/Defs/LinearOrder.lean
@@ -76,6 +76,7 @@ class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α w
     compareOfLessAndEq_rfl
 
 attribute [to_dual existing] LinearOrder.toMax
+attribute [to_dual self] LinearOrder.toDecidableLT LinearOrder.toDecidableLE
 
 variable [LinearOrder α] {a b c : α}
 
@@ -83,12 +84,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 674cf1e0d58c98..ec7c3803b73a1b 100644
--- a/Mathlib/Order/Defs/PartialOrder.lean
+++ b/Mathlib/Order/Defs/PartialOrder.lean
@@ -142,30 +142,64 @@ instance instTransGTGE : @Trans α α α GT.gt GE.ge GT.gt := ⟨lt_of_lt_of_le'
 @[to_dual existing instTransLELT]
 instance instTransGEGT : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'⟩
 
+namespace Mathlib.Tactic.UnfoldBoundary
+
+variable {α : Type*}
+
+@[to_dual_cast]
+def DecidableLE.identification [LE α] :
+  Identification (DecidableLE α) (DecidableRel fun x y : α ↦ x ≤ y) := .Id
+
+@[to_dual existing identification]
+def DecidableLE.dual_identification [LE α] :
+    Identification (DecidableLE α) (DecidableRel fun x y : α ↦ y ≤ x) where
+  toFun h x y := h y x
+  invFun h x y := h y x
+
+@[to_dual_cast]
+def DecidableLT.identification [LT α] :
+  Identification (DecidableLT α) (DecidableRel fun x y : α ↦ x < y) := .Id
+
+@[to_dual existing identification]
+def DecidableLT.dual_identification [LT α] :
+    Identification (DecidableLT α) (DecidableRel fun x y : α ↦ y < x) where
+  toFun h x y := h y x
+  invFun h x y := h y x
+
+end Mathlib.Tactic.UnfoldBoundary
+
 /-- `<` 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
 
 /-- `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`.
 -/
-@[to_dual self (reorder := 3 4)]
+@[to_dual self (reorder := 3 4), to_dual_dont_unfold]
 def WCovBy (a b : α) : Prop :=
   a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
 @[inherit_doc]
 infixl:50 " ⩿ " => WCovBy
 
+@[to_dual existing eq_def]
+theorem WCovBy.eq_def_dual : (b ⩿ a) = (b ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c) := by
+  simp [WCovBy, ← not_and, and_comm]
+
 /-- `CovBy a b` means that `b` covers `a`. This means that `a < b` and there is no element in
 between. This is denoted `a ⋖ b`. -/
-@[to_dual self (reorder := 3 4)]
+@[to_dual self (reorder := 3 4), to_dual_dont_unfold]
 def CovBy {α : Type*} [LT α] (a b : α) : Prop :=
   a < b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
 @[inherit_doc]
 infixl:50 " ⋖ " => CovBy
 
+@[to_dual existing eq_def]
+theorem CovBy.eq_def_dual {α : Type*} [LT α] (a b : α) :
+    (b ⋖ a) = (b < a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c) := by
+  simp [CovBy, ← not_and, and_comm]
+
 end Preorder
 
 section PartialOrder
diff --git a/Mathlib/Order/Interval/Set/Defs.lean b/Mathlib/Order/Interval/Set/Defs.lean
index 34daa4956d3d48..ca8541f6f6f177 100644
--- a/Mathlib/Order/Interval/Set/Defs.lean
+++ b/Mathlib/Order/Interval/Set/Defs.lean
@@ -32,10 +32,15 @@ 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), to_dual_dont_unfold]
 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 existing Ioo.eq_def]
+theorem Ioo.eq_def_dual (a b : α) : Ioo b a = { x | x < a ∧ b < x } :=
+  Set.ext fun _ ↦ And.comm
+
+@[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 }
diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean
index 750c39d6ba34c5..bab19af6f9c314 100644
--- a/Mathlib/Tactic/ToDual.lean
+++ b/Mathlib/Tactic/ToDual.lean
@@ -5,7 +5,7 @@ Authors: Jovan Gerbscheid
 -/
 module
 
-public meta import Mathlib.Tactic.Translate.ToDual
+public import Mathlib.Tactic.Translate.ToDual
 import all Init.Core  -- TODO: for accessing proofs
 
 
@@ -27,10 +27,6 @@ the dual of `e₂`. Hence, the translation of `DecidableLT` needs to be defEq to
 `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
 
 attribute [to_dual_do_translate] Empty PEmpty Unit PUnit
 
diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index 18020f1bfacfb2..c3fc776064de60 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -19,6 +19,7 @@ public meta import Mathlib.Lean.Name
 public meta import Mathlib.Tactic.Eqns -- just to copy the attribute
 public meta import Mathlib.Tactic.Simps.Basic
 public meta import Mathlib.Tactic.Translate.GuessName
+public import Mathlib.Tactic.Translate.UnfoldBoundary
 public meta import Lean.Meta.CoeAttr
 
 /-!
@@ -175,6 +176,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
@@ -392,6 +398,7 @@ e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorder
 -/
 def applyReplacementFun (t : TranslateData) (e : Expr) (dontTranslate : Array FVarId := #[]) :
     MetaM Expr := do
+  let e ← t.unfoldBoundaries.elim (pure e) (·.insertBoundaries e)
   let e' := aux (← getEnv) (← getBoolOption `trace.translate_detail) (← expand t e)
   -- Make sure any new reserved names in the expr are realized; this needs to be done outside of
   -- `aux` as it is monadic.
@@ -554,13 +561,16 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
   let mut decl := srcDecl.updateName tgt
   if 0 ∈ reorder.flatten then
     decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
+  let type := decl.type
   decl := decl.updateType <| ← reorderForall reorder <| ← applyReplacementForall t dont <|
-    renameBinderNames t decl.type
+    renameBinderNames t type
   if let some v := decl.value? then
+    let v ← t.unfoldBoundaries.elim (pure v) (·.cast v type)
     decl := decl.updateValue <| ← reorderLambda reorder <| ← applyReplacementLambda t dont v
-  else if let .opaqueInfo info := decl then -- not covered by `value?`
+  else if let .opaqueInfo info@{ value := v, .. } := decl then -- not covered by `value?`
+    let v ← t.unfoldBoundaries.elim (pure v) (·.cast v type)
     decl := .opaqueInfo { info with
-      value := ← reorderLambda reorder <| ← applyReplacementLambda t dont info.value }
+      value := ← reorderLambda reorder <| ← applyReplacementLambda t dont v }
   return decl
 
 /-- Abstracts the nested proofs in the value of `decl` if it is a def.
diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index 976415c6f4a367..e067cea03cc409 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 meta import Mathlib.Tactic.Translate.Core
+public import Mathlib.Tactic.Translate.Core
 
 /-!
 # 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 Command Std Translate UnfoldBoundary
 
 @[inherit_doc TranslateData.ignoreArgsAttr]
 syntax (name := to_dual_ignore_args) "to_dual_ignore_args" (ppSpace num)* : attr
@@ -40,6 +40,12 @@ syntax (name := to_dual_do_translate) "to_dual_do_translate" : attr
 @[inherit_doc TranslateData.doTranslateAttr]
 syntax (name := to_dual_dont_translate) "to_dual_dont_translate" : attr
 
+@[inherit_doc UnfoldBoundaryExt.unfolds]
+syntax (name := to_dual_dont_unfold) "to_dual_dont_unfold" : attr
+
+@[inherit_doc UnfoldBoundaryExt.casts]
+syntax (name := to_dual_cast) "to_dual_cast" : attr
+
 /-- The attribute `to_dual` can be used to automatically transport theorems
 and definitions (but not inductive types and structures) to their dual version.
 It uses the same implementation as `to_additive`.
@@ -103,6 +109,34 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
           | _ => throwUnsupportedSyntax
         return ids.toList }
 
+@[inherit_doc UnfoldBoundaryExt.unfolds]
+initialize unfolds : NameMapExtension SimpTheorem ← registerNameMapExtension _
+initialize
+  registerBuiltinAttribute {
+    name := `to_dual_dont_unfold
+    descr := "The `to_dual_dont_unfold` attribute"
+    applicationTime := .afterCompilation
+    add := fun declName _ _ ↦ MetaM.run' do
+      let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+      let some name ← mkSimpleEqThm declName name |
+        throwError "No unfold theorem could be generated for `{declName}`"
+      executeReservedNameAction name
+      unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true } }
+
+@[inherit_doc UnfoldBoundaryExt.casts]
+initialize casts : NameMapExtension Name ← registerNameMapExtension _
+initialize
+  registerBuiltinAttribute {
+    name := `to_dual_cast
+    descr := "The `to_dual_cast` attribute"
+    add := fun cast _ _ ↦ MetaM.run' do
+      let_expr Identification α _ := (← getConstInfo cast).type.getForallBody |
+        throwError "expected an `Identification`, not {cast}"
+      let .const declName _ := α.getAppFn | throwError "expected {α} to be a constant application"
+      casts.add declName cast }
+
+def unfoldBoundaries : UnfoldBoundaryExt := { unfolds, casts }
+
 @[inherit_doc TranslateData.argInfoAttr]
 initialize argInfoAttr : NameMapExtension ArgInfo ← registerNameMapExtension _
 
@@ -185,7 +219,7 @@ 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
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
new file mode 100644
index 00000000000000..95b10a0ee503c2
--- /dev/null
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -0,0 +1,168 @@
+module
+
+public meta import Batteries.Lean.NameMapAttribute
+public import Mathlib.Init
+
+
+namespace Mathlib.Tactic.UnfoldBoundary
+
+public section identification
+
+universe u
+
+structure Identification (α β : Type u) : Type u where
+  toFun : α → β
+  invFun : β → α
+
+@[expose]
+def Identification.Id {α : Type u} : Identification α α where
+  toFun x := x
+  invFun x := x
+
+end identification
+
+meta section
+
+open Lean Meta
+
+structure UnfoldBoundaries where
+  unfolds : NameMap SimpTheorem
+  casts : NameMap Name
+
+def withBlockUnfolding {α} (boundaries : UnfoldBoundaries) (x : MetaM α) : MetaM α := do
+  withCanUnfoldPred (fun _ cinfo =>
+    return !boundaries.unfolds.contains cinfo.name && !boundaries.casts.contains cinfo.name) x
+
+def withoutBlockUnfolding {α} (x : MetaM α) : MetaM α := do
+  withReader ({· with canUnfold? := none }) x
+
+def unfold (e : Expr) (unfolds : NameMap SimpTheorem) : MetaM Simp.Result :=
+  withoutBlockUnfolding do
+  try
+    let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
+      (congrTheorems := (← getSimpCongrTheorems))
+    (·.1) <$> Simp.main e ctx (methods := { pre })
+  catch e =>
+    throwError "ohNOOOO\n{e.toMessageData}"
+where
+  pre (e : Expr) : SimpM Simp.Step := do
+    let .const c _ := e.getAppFn | return .continue
+    let some thm := unfolds.find? c | return .continue
+    let some r ← Simp.tryTheorem? e thm | return .continue
+    return .done r
+
+
+def refoldConsts (e expectedType : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
+  let goal ← mkFreshExprMVar expectedType
+  go e goal.mvarId!
+  instantiateMVars goal
+where
+  go (e : Expr) (goal : MVarId) : MetaM Unit := do
+    let r ← unfold (← goal.getType) boundaries.unfolds
+    let goal ← match r.proof? with
+      | some proof => goal.replaceTargetEq r.expr proof
+      | none => pure goal
+    let tgt ← goal.getType
+    if let .const c _ := (← whnf tgt.getForallBody).getAppFn then
+      if let some cast := boundaries.casts.find? c then
+        return ← forallTelescope tgt fun xs tgt => do
+          let cast ← mkConstWithFreshMVarLevels cast
+          let (mvars, _, type) ← forallMetaTelescope (← inferType cast)
+          let_expr f@Identification α β := type | throwError "expected Identification, not {type}"
+          if ← isDefEq tgt α then
+            let goal' ← mkFreshExprMVar (← instantiateMVars β)
+            go (mkAppN e xs) goal'.mvarId!
+            goal.assign <| ← mkLambdaFVars xs <|
+              mkApp4 (.const ``Identification.invFun f.constLevels!) α β (mkAppN cast mvars) goal'
+          else
+            throwError "identification `{cast}` could not be applied at {tgt}"
+    if ← isDefEq tgt (← inferType e) then
+      goal.assign e
+    else
+      throwError "could get {e} to have type {tgt}."
+
+def unfoldConsts (e : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
+  let eType ← inferType e
+  if let .const c _ := (← whnf eType).getAppFn then
+    if let some cast := boundaries.casts.find? c then
+      let cast ← mkConstWithFreshMVarLevels cast
+      let (mvars, _, type) ← forallMetaTelescope (← inferType cast)
+      let_expr f@Identification α β := type | throwError "expected Identification, not {type}"
+      if ← isDefEq eType α then
+        let e := mkApp4 (.const ``Identification.toFun f.constLevels!) α β (mkAppN cast mvars) e
+        return ← unfoldConsts e boundaries
+      else
+        throwError "identification `{cast}` could not be applied at {eType}"
+  let r ← unfold eType boundaries.unfolds
+  let some pf := r.proof? | return e
+  mkAppOptM ``cast #[eType, r.expr, pf, e]
+
+/-- Given an expression `e` with expected type `type`, if `e` doesn't have that type,
+use a cast to turn `e` into that type. -/
+def mkAppWithCast (f a : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr :=
+  try
+    checkApp f a
+    return f.app a
+  catch _ =>
+    let f ← unfoldConsts f boundaries
+    let .forallE _ d _ _ ← whnf (← inferType f) | throwFunctionExpected f
+    let a ← unfoldConsts a boundaries
+    let a ← refoldConsts a d boundaries
+    try
+      checkApp f a
+      return f.app a
+    catch _ =>
+      throwError "invalid application {f} applied to {a}"
+
+def mkCast (e expectedType : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
+  if ← isDefEq (← inferType e) expectedType then
+    return e
+  let e ← unfoldConsts e boundaries
+  let e ← refoldConsts e expectedType boundaries
+  if ← isDefEq (← inferType e) expectedType then
+    return e
+  else
+    throwError "{e} does not match the expected type {expectedType}"
+
+public section
+
+/-- Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded. -/
+structure UnfoldBoundaryExt where
+  /-- The `dont_unfold` attribute is used to tag declarations `foo` that should not be unfolded in
+  a proof that is translated. Instead, the unfold theorem `foo.eq_def` is inserted. -/
+  unfolds : NameMapExtension SimpTheorem
+  /-- The `cast` attribute is used to tag casting functions `foo.val` for declarations `foo` that
+  should not be unfolded in a proof that is translated. -/
+  casts : NameMapExtension Name
+
+def UnfoldBoundaryExt.cast (e expectedType : Expr) (boundaries : UnfoldBoundaryExt) :
+    MetaM Expr := do
+  let env ← getEnv
+  let boundaries := {
+    unfolds := boundaries.unfolds.getState env
+    casts := boundaries.casts.getState env }
+  withBlockUnfolding boundaries do withTransparency TransparencyMode.all do
+    mkCast e expectedType boundaries
+
+
+def UnfoldBoundaryExt.insertBoundaries (e : Expr) (boundaries : UnfoldBoundaryExt) :
+    MetaM Expr := do
+  let env ← getEnv
+  let boundaries := {
+    unfolds := boundaries.unfolds.getState env
+    casts := boundaries.casts.getState env }
+  withBlockUnfolding boundaries do withTransparency TransparencyMode.all do
+    instantiateMVars <| ← transform e (post := fun e ↦ e.withApp fun f args => do
+      let mut f := f
+      for arg in args do
+        try
+          f ← mkAppWithCast f arg boundaries
+        catch e =>
+          throwError "failed to deal with {f} applied to {arg}\n{e.toMessageData}"
+      return .done f)
+
+end
+
+end
+
+end Mathlib.Tactic.UnfoldBoundary

From 6850a5212e58643fa432720eb34c7a4015284083 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 5 Dec 2025 01:06:47 +0000
Subject: [PATCH 02/26] make linters happy

---
 Mathlib.lean                                 |  1 +
 Mathlib/Order/Defs/PartialOrder.lean         |  4 ++++
 Mathlib/Tactic.lean                          |  1 +
 Mathlib/Tactic/Translate/ToDual.lean         |  1 +
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 20 +++++++++++++-------
 5 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 708a9a5c7b6b3f..3e617ab6dc3106 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6699,6 +6699,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/Order/Defs/PartialOrder.lean b/Mathlib/Order/Defs/PartialOrder.lean
index ec7c3803b73a1b..87aae6a4780547 100644
--- a/Mathlib/Order/Defs/PartialOrder.lean
+++ b/Mathlib/Order/Defs/PartialOrder.lean
@@ -146,20 +146,24 @@ namespace Mathlib.Tactic.UnfoldBoundary
 
 variable {α : Type*}
 
+/-- The cast for `DecidableLE` inserted by `to_dual`. -/
 @[to_dual_cast]
 def DecidableLE.identification [LE α] :
   Identification (DecidableLE α) (DecidableRel fun x y : α ↦ x ≤ y) := .Id
 
+/-- The dual cast for `DecidableLE` inserted by `to_dual`. -/
 @[to_dual existing identification]
 def DecidableLE.dual_identification [LE α] :
     Identification (DecidableLE α) (DecidableRel fun x y : α ↦ y ≤ x) where
   toFun h x y := h y x
   invFun h x y := h y x
 
+/-- The cast for `DecidableLT` inserted by `to_dual`. -/
 @[to_dual_cast]
 def DecidableLT.identification [LT α] :
   Identification (DecidableLT α) (DecidableRel fun x y : α ↦ x < y) := .Id
 
+/-- The dual cast for `DecidableLT` inserted by `to_dual`. -/
 @[to_dual existing identification]
 def DecidableLT.dual_identification [LT α] :
     Identification (DecidableLT α) (DecidableRel fun x y : α ↦ y < x) where
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index af588cf786d5e1..5d29179941ba61 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/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index e067cea03cc409..dbcdddc9d7a09e 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -135,6 +135,7 @@ initialize
       let .const declName _ := α.getAppFn | throwError "expected {α} to be a constant application"
       casts.add declName cast }
 
+@[inherit_doc TranslateData.unfoldBoundaries]
 def unfoldBoundaries : UnfoldBoundaryExt := { unfolds, casts }
 
 @[inherit_doc TranslateData.argInfoAttr]
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 95b10a0ee503c2..bdb68a20604a87 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -1,8 +1,16 @@
+/-
+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 Batteries.Lean.NameMapAttribute
 public import Mathlib.Init
 
+/-!
+# Modify proof terms so that they don't rely on unfolding certain constants
+-/
 
 namespace Mathlib.Tactic.UnfoldBoundary
 
@@ -38,12 +46,9 @@ def withoutBlockUnfolding {α} (x : MetaM α) : MetaM α := do
 
 def unfold (e : Expr) (unfolds : NameMap SimpTheorem) : MetaM Simp.Result :=
   withoutBlockUnfolding do
-  try
-    let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
-      (congrTheorems := (← getSimpCongrTheorems))
-    (·.1) <$> Simp.main e ctx (methods := { pre })
-  catch e =>
-    throwError "ohNOOOO\n{e.toMessageData}"
+  let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
+    (congrTheorems := (← getSimpCongrTheorems))
+  (·.1) <$> Simp.main e ctx (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
     let .const c _ := e.getAppFn | return .continue
@@ -135,6 +140,7 @@ structure UnfoldBoundaryExt where
   should not be unfolded in a proof that is translated. -/
   casts : NameMapExtension Name
 
+/-- Modify `e` so that it has type `expectedType`. -/
 def UnfoldBoundaryExt.cast (e expectedType : Expr) (boundaries : UnfoldBoundaryExt) :
     MetaM Expr := do
   let env ← getEnv
@@ -144,7 +150,7 @@ def UnfoldBoundaryExt.cast (e expectedType : Expr) (boundaries : UnfoldBoundaryE
   withBlockUnfolding boundaries do withTransparency TransparencyMode.all do
     mkCast e expectedType boundaries
 
-
+/-- Modify `e` so that it is well typed if the constants in `boundaries` cannot be unfolded. -/
 def UnfoldBoundaryExt.insertBoundaries (e : Expr) (boundaries : UnfoldBoundaryExt) :
     MetaM Expr := do
   let env ← getEnv

From 70bb4a5aefc71b6faefebb9881c220799001dc0b Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 5 Dec 2025 13:42:11 +0000
Subject: [PATCH 03/26] some improvements

---
 Mathlib/Order/Cover.lean                     |  8 ++-
 Mathlib/Order/Interval/Set/Defs.lean         | 60 ++++++++++----------
 Mathlib/Order/Monotone/Defs.lean             | 28 ++++++++-
 Mathlib/Tactic/Translate/Core.lean           | 23 +++++---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 39 ++++++-------
 5 files changed, 96 insertions(+), 62 deletions(-)

diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean
index 33d6351de4af63..fb6d1157aedd66 100644
--- a/Mathlib/Order/Cover.lean
+++ b/Mathlib/Order/Cover.lean
@@ -82,24 +82,26 @@ 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 isRefl']
 instance WCovBy.isRefl : IsRefl α (· ⩿ ·) :=
   ⟨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⟩
-
 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)⟩
 
diff --git a/Mathlib/Order/Interval/Set/Defs.lean b/Mathlib/Order/Interval/Set/Defs.lean
index ca8541f6f6f177..9a76ae982e8889 100644
--- a/Mathlib/Order/Interval/Set/Defs.lean
+++ b/Mathlib/Order/Interval/Set/Defs.lean
@@ -35,54 +35,54 @@ variable {α : Type*} [Preorder α] {a b x : α}
 @[to_dual self (reorder := a b), to_dual_dont_unfold]
 def Ioo (a b : α) := { x | a < x ∧ x < b }
 
-@[to_dual existing Ioo.eq_def]
-theorem Ioo.eq_def_dual (a b : α) : Ioo b a = { x | x < a ∧ b < x } :=
-  Set.ext fun _ ↦ And.comm
+@[to_dual existing eq_def]
+theorem Ioo.eq_def_dual (a b : α) : Ioo b a = { x | x < a ∧ b < x } := Set.ext fun _ ↦ And.comm
 
 @[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)$. -/
+@[to_dual_dont_unfold]
 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) Ico, to_dual_dont_unfold]
+def Ioc (a b : α) := { x | a < x ∧ x ≤ b }
+
+@[to_dual existing eq_def]
+theorem Ico.eq_def_dual (a b : α) : Ico b a = { x | x < a ∧ b ≤ x } := Set.ext fun _ ↦ And.comm
+@[to_dual existing eq_def]
+theorem Ioc.eq_def_dual (a b : α) : Ioc b a = { x | x ≤ a ∧ b < x } := Set.ext fun _ ↦ And.comm
+
+@[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
 
 /-- `Iio b` is the left-infinite right-open interval $(-∞, b)$. -/
+@[to_dual Ioi /-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/]
 def Iio (b : α) := { x | x < b }
 
-@[simp, grind =] theorem mem_Iio : x ∈ Iio b ↔ x < b := Iff.rfl
-theorem Iio_def (a : α) : { x | x < a } = Iio a := rfl
+@[to_dual (attr := simp, grind =) mem_Ioi] theorem mem_Iio : x ∈ Iio b ↔ x < b := Iff.rfl
+@[to_dual Ioi_def] theorem Iio_def (a : α) : { x | x < a } = Iio a := rfl
 
 /-- `Icc a b` is the left-closed right-closed interval $[a, b]$. -/
+@[to_dual self (reorder := a b), to_dual_dont_unfold]
 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
+@[to_dual existing eq_def]
+theorem Icc.eq_def_dual (a b : α) : Icc b a = { x | x ≤ a ∧ b ≤ x } := Set.ext fun _ ↦ And.comm
+
+@[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
 
 /-- `Iic b` is the left-infinite right-closed interval $(-∞, b]$. -/
+@[to_dual Ici /-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/]
 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
-
-/-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
-def Ioc (a b : α) := { x | a < x ∧ x ≤ b }
-
-@[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 }
-
-@[simp, grind =] theorem mem_Ici : x ∈ Ici a ↔ a ≤ x := Iff.rfl
-theorem Ici_def (a : α) : { x | a ≤ x } = Ici a := rfl
-
-/-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/
-def Ioi (a : α) := { x | a < x }
-
-@[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 =) mem_Ici] theorem mem_Iic : x ∈ Iic b ↔ x ≤ b := Iff.rfl
+@[to_dual Ici_def] 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
@@ -92,4 +92,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 d2cb98a93a8b05..15cd199f8ebd6a 100644
--- a/Mathlib/Order/Monotone/Defs.lean
+++ b/Mathlib/Order/Monotone/Defs.lean
@@ -93,6 +93,19 @@ def StrictMonoOn (f : α → β) (s : Set α) : Prop :=
 def StrictAntiOn (f : α → β) (s : Set α) : Prop :=
   ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a < b → f b < f a
 
+attribute [to_dual_dont_unfold]
+  Monotone Antitone MonotoneOn AntitoneOn StrictMono StrictAnti StrictMonoOn StrictAntiOn
+
+set_option linter.style.longLine false
+@[to_dual existing eq_def] theorem Monotone.eq_def_dual (f : α → β) : Monotone f = ∀ ⦃a b⦄, b ≤ a → f b ≤ f a := by grind [Monotone.eq_def]
+@[to_dual existing eq_def] theorem Antitone.eq_def_dual (f : α → β) : Antitone f = ∀ ⦃a b⦄, b ≤ a → f a ≤ f b := by grind [Antitone.eq_def]
+@[to_dual existing eq_def] theorem MonotoneOn.eq_def_dual (f : α → β) (s : Set α) : MonotoneOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b ≤ a → f b ≤ f a := by grind [MonotoneOn.eq_def]
+@[to_dual existing eq_def] theorem AntitoneOn.eq_def_dual (f : α → β) (s : Set α) : AntitoneOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b ≤ a → f a ≤ f b := by grind [AntitoneOn.eq_def]
+@[to_dual existing eq_def] theorem StrictMono.eq_def_dual (f : α → β) : StrictMono f = ∀ ⦃a b⦄, b < a → f b < f a := by grind [StrictMono.eq_def]
+@[to_dual existing eq_def] theorem StrictAnti.eq_def_dual (f : α → β) : StrictAnti f = ∀ ⦃a b⦄, b < a → f a < f b := by grind [StrictAnti.eq_def]
+@[to_dual existing eq_def] theorem StrictMonoOn.eq_def_dual (f : α → β) (s : Set α) : StrictMonoOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b < a → f b < f a := by grind [StrictMonoOn.eq_def]
+@[to_dual existing eq_def] theorem StrictAntiOn.eq_def_dual (f : α → β) (s : Set α) : StrictAntiOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b < a → f a < f b := by grind [StrictAntiOn.eq_def]
+
 end MonotoneDef
 
 section Decidable
@@ -126,6 +139,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 +181,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 +241,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 +339,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 injective_of_lt_imp_ne']
 theorem injective_of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
     Injective f := by
   intro x y hf
@@ -440,16 +462,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/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index c3fc776064de60..c39c9172063733 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -398,7 +398,6 @@ e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorder
 -/
 def applyReplacementFun (t : TranslateData) (e : Expr) (dontTranslate : Array FVarId := #[]) :
     MetaM Expr := do
-  let e ← t.unfoldBoundaries.elim (pure e) (·.insertBoundaries e)
   let e' := aux (← getEnv) (← getBoolOption `trace.translate_detail) (← expand t e)
   -- Make sure any new reserved names in the expr are realized; this needs to be done outside of
   -- `aux` as it is monadic.
@@ -561,16 +560,21 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
   let mut decl := srcDecl.updateName tgt
   if 0 ∈ reorder.flatten then
     decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
-  let type := decl.type
+  let translateValue (v : Expr) : MetaM Expr := do
+    let v ← match t.unfoldBoundaries with
+      | some b => b.cast (← b.insertBoundaries v) decl.type
+      | none => pure v
+    reorderLambda reorder <| ← applyReplacementLambda t dont v
+  let type ← match t.unfoldBoundaries with
+    | some b => b.insertBoundaries decl.type
+    | none => pure decl.type
   decl := decl.updateType <| ← reorderForall reorder <| ← applyReplacementForall t dont <|
     renameBinderNames t type
   if let some v := decl.value? then
-    let v ← t.unfoldBoundaries.elim (pure v) (·.cast v type)
-    decl := decl.updateValue <| ← reorderLambda reorder <| ← applyReplacementLambda t dont v
-  else if let .opaqueInfo info@{ value := v, .. } := decl then -- not covered by `value?`
-    let v ← t.unfoldBoundaries.elim (pure v) (·.cast v type)
+    decl := decl.updateValue <| ← translateValue v
+  else if let .opaqueInfo info := decl then -- not covered by `value?`
     decl := .opaqueInfo { info with
-      value := ← reorderLambda reorder <| ← applyReplacementLambda t dont v }
+      value :=  ← translateValue info.value }
   return decl
 
 /-- Abstracts the nested proofs in the value of `decl` if it is a def.
@@ -899,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 srcType ← match t.unfoldBoundaries with
+    | some b => b.insertBoundaries srcDecl.type
+    | none => pure srcDecl.type
+  let srcType ← applyReplacementForall t cfg.dontTranslate srcType
   let reorder' := guessReorder srcType tgtDecl.type
   trace[translate_detail] "The guessed reorder is {reorder'}"
   let reorder ←
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index bdb68a20604a87..56c16db64b0283 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -18,10 +18,15 @@ public section identification
 
 universe u
 
+/-- `Identification` is used by translation attributes to insert abstraction boundaries in terms
+that need to be translated-/
 structure Identification (α β : Type u) : Type u where
+  /-- The unfolding function. -/
   toFun : α → β
+  /-- The refolding function. -/
   invFun : β → α
 
+/-- The identity `Identification`. -/
 @[expose]
 def Identification.Id {α : Type u} : Identification α α where
   toFun x := x
@@ -41,17 +46,13 @@ def withBlockUnfolding {α} (boundaries : UnfoldBoundaries) (x : MetaM α) : Met
   withCanUnfoldPred (fun _ cinfo =>
     return !boundaries.unfolds.contains cinfo.name && !boundaries.casts.contains cinfo.name) x
 
-def withoutBlockUnfolding {α} (x : MetaM α) : MetaM α := do
-  withReader ({· with canUnfold? := none }) x
-
-def unfold (e : Expr) (unfolds : NameMap SimpTheorem) : MetaM Simp.Result :=
-  withoutBlockUnfolding do
+def unfold (e : Expr) (unfolds : NameMap SimpTheorem) : MetaM Simp.Result := do
   let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
     (congrTheorems := (← getSimpCongrTheorems))
   (·.1) <$> Simp.main e ctx (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
-    let .const c _ := e.getAppFn | return .continue
+    let .const c _ ← whnf e.getAppFn | return .continue
     let some thm := unfolds.find? c | return .continue
     let some r ← Simp.tryTheorem? e thm | return .continue
     return .done r
@@ -67,24 +68,24 @@ where
     let goal ← match r.proof? with
       | some proof => goal.replaceTargetEq r.expr proof
       | none => pure goal
-    let tgt ← goal.getType
-    if let .const c _ := (← whnf tgt.getForallBody).getAppFn then
-      if let some cast := boundaries.casts.find? c then
-        return ← forallTelescope tgt fun xs tgt => do
+    forallTelescope (← goal.getType) fun xs tgt => do
+      if let .const c _ := (← whnf tgt).getAppFn then
+        if let some cast := boundaries.casts.find? c then
           let cast ← mkConstWithFreshMVarLevels cast
           let (mvars, _, type) ← forallMetaTelescope (← inferType cast)
-          let_expr f@Identification α β := type | throwError "expected Identification, not {type}"
+          let_expr f@Identification α β := type | throwError "expected `Identification`, not {type}"
           if ← isDefEq tgt α then
             let goal' ← mkFreshExprMVar (← instantiateMVars β)
             go (mkAppN e xs) goal'.mvarId!
             goal.assign <| ← mkLambdaFVars xs <|
               mkApp4 (.const ``Identification.invFun f.constLevels!) α β (mkAppN cast mvars) goal'
+            return
           else
             throwError "identification `{cast}` could not be applied at {tgt}"
-    if ← isDefEq tgt (← inferType e) then
-      goal.assign e
-    else
-      throwError "could get {e} to have type {tgt}."
+      if ← isDefEq (← goal.getType) (← inferType e) then
+        goal.assign e
+      else
+        throwError "Error: could not cast {e} into the type {← goal.getType}."
 
 def unfoldConsts (e : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
   let eType ← inferType e
@@ -97,7 +98,7 @@ def unfoldConsts (e : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
         let e := mkApp4 (.const ``Identification.toFun f.constLevels!) α β (mkAppN cast mvars) e
         return ← unfoldConsts e boundaries
       else
-        throwError "identification `{cast}` could not be applied at {eType}"
+        throwError "Error: identification `{cast}` could not be applied at {eType}"
   let r ← unfold eType boundaries.unfolds
   let some pf := r.proof? | return e
   mkAppOptM ``cast #[eType, r.expr, pf, e]
@@ -113,11 +114,7 @@ def mkAppWithCast (f a : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr :=
     let .forallE _ d _ _ ← whnf (← inferType f) | throwFunctionExpected f
     let a ← unfoldConsts a boundaries
     let a ← refoldConsts a d boundaries
-    try
-      checkApp f a
-      return f.app a
-    catch _ =>
-      throwError "invalid application {f} applied to {a}"
+    return f.app a
 
 def mkCast (e expectedType : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
   if ← isDefEq (← inferType e) expectedType then

From 94a72a1bb1055a51308106d35fd6af9f0a5cd1c0 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 5 Dec 2025 16:30:37 +0000
Subject: [PATCH 04/26] .

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 56c16db64b0283..325eeafefbbd5d 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -19,7 +19,7 @@ public section identification
 universe u
 
 /-- `Identification` is used by translation attributes to insert abstraction boundaries in terms
-that need to be translated-/
+that need to be translated. -/
 structure Identification (α β : Type u) : Type u where
   /-- The unfolding function. -/
   toFun : α → β

From 8d2fe983f6b0328c76ea95fe954a7ca9d346a288 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Mon, 15 Dec 2025 13:54:05 +0000
Subject: [PATCH 05/26] improved UI

---
 Mathlib/Order/Basic.lean                     |   2 -
 Mathlib/Order/Defs/LinearOrder.lean          |   1 -
 Mathlib/Order/Defs/PartialOrder.lean         |  48 +-----
 Mathlib/Tactic/ToDual.lean                   |  12 +-
 Mathlib/Tactic/Translate/Core.lean           |  41 +++--
 Mathlib/Tactic/Translate/ToDual.lean         | 119 +++++++++----
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 165 +++++++++----------
 7 files changed, 199 insertions(+), 189 deletions(-)

diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index 668d38234a87d0..7de0ae80e53c4b 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -960,11 +960,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 self]
 instance decidableLE [Preorder α] [h : DecidableLE α] {p : α → Prop} :
     DecidableLE (Subtype p) := fun a b ↦ h a b
 
-@[to_dual self]
 instance decidableLT [Preorder α] [h : DecidableLT α] {p : α → Prop} :
     DecidableLT (Subtype p) := fun a b ↦ h a b
 
diff --git a/Mathlib/Order/Defs/LinearOrder.lean b/Mathlib/Order/Defs/LinearOrder.lean
index dfae076e589b7e..caee7417ffdfe8 100644
--- a/Mathlib/Order/Defs/LinearOrder.lean
+++ b/Mathlib/Order/Defs/LinearOrder.lean
@@ -76,7 +76,6 @@ class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α w
     compareOfLessAndEq_rfl
 
 attribute [to_dual existing] LinearOrder.toMax
-attribute [to_dual self] LinearOrder.toDecidableLT LinearOrder.toDecidableLE
 
 variable [LinearOrder α] {a b c : α}
 
diff --git a/Mathlib/Order/Defs/PartialOrder.lean b/Mathlib/Order/Defs/PartialOrder.lean
index 87aae6a4780547..48aa81af735c23 100644
--- a/Mathlib/Order/Defs/PartialOrder.lean
+++ b/Mathlib/Order/Defs/PartialOrder.lean
@@ -142,36 +142,6 @@ instance instTransGTGE : @Trans α α α GT.gt GE.ge GT.gt := ⟨lt_of_lt_of_le'
 @[to_dual existing instTransLELT]
 instance instTransGEGT : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'⟩
 
-namespace Mathlib.Tactic.UnfoldBoundary
-
-variable {α : Type*}
-
-/-- The cast for `DecidableLE` inserted by `to_dual`. -/
-@[to_dual_cast]
-def DecidableLE.identification [LE α] :
-  Identification (DecidableLE α) (DecidableRel fun x y : α ↦ x ≤ y) := .Id
-
-/-- The dual cast for `DecidableLE` inserted by `to_dual`. -/
-@[to_dual existing identification]
-def DecidableLE.dual_identification [LE α] :
-    Identification (DecidableLE α) (DecidableRel fun x y : α ↦ y ≤ x) where
-  toFun h x y := h y x
-  invFun h x y := h y x
-
-/-- The cast for `DecidableLT` inserted by `to_dual`. -/
-@[to_dual_cast]
-def DecidableLT.identification [LT α] :
-  Identification (DecidableLT α) (DecidableRel fun x y : α ↦ x < y) := .Id
-
-/-- The dual cast for `DecidableLT` inserted by `to_dual`. -/
-@[to_dual existing identification]
-def DecidableLT.dual_identification [LT α] :
-    Identification (DecidableLT α) (DecidableRel fun x y : α ↦ y < x) where
-  toFun h x y := h y x
-  invFun h x y := h y x
-
-end Mathlib.Tactic.UnfoldBoundary
-
 /-- `<` is decidable if `≤` is. -/
 def decidableLTOfDecidableLE [DecidableLE α] : DecidableLT α :=
   fun _ _ => decidable_of_iff _ lt_iff_le_not_ge.symm
@@ -179,31 +149,26 @@ def decidableLTOfDecidableLE [DecidableLE α] : DecidableLT α :=
 /-- `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`.
 -/
-@[to_dual self (reorder := 3 4), to_dual_dont_unfold]
+@[to_dual self (reorder := 3 4)]
 def WCovBy (a b : α) : Prop :=
   a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b
 
+to_dual_insert_cast WCovBy := by grind
+
 @[inherit_doc]
 infixl:50 " ⩿ " => WCovBy
 
-@[to_dual existing eq_def]
-theorem WCovBy.eq_def_dual : (b ⩿ a) = (b ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c) := by
-  simp [WCovBy, ← not_and, and_comm]
-
 /-- `CovBy a b` means that `b` covers `a`. This means that `a < b` and there is no element in
 between. This is denoted `a ⋖ b`. -/
-@[to_dual self (reorder := 3 4), to_dual_dont_unfold]
+@[to_dual self (reorder := 3 4)]
 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
 
-@[to_dual existing eq_def]
-theorem CovBy.eq_def_dual {α : Type*} [LT α] (a b : α) :
-    (b ⋖ a) = (b < a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c) := by
-  simp [CovBy, ← not_and, and_comm]
-
 end Preorder
 
 section PartialOrder
@@ -240,7 +205,6 @@ 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
diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean
index bab19af6f9c314..2b5f365c7736f2 100644
--- a/Mathlib/Tactic/ToDual.lean
+++ b/Mathlib/Tactic/ToDual.lean
@@ -17,16 +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.
--/
+to_dual_insert_cast_fun DecidableLE := fun a b ↦ this b a, fun a b ↦ this b a
+to_dual_insert_cast_fun DecidableLT := fun a b ↦ this b a, fun a b ↦ this 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 c39c9172063733..72a5e2c0151355 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -560,16 +560,24 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
   let mut decl := srcDecl.updateName tgt
   if 0 ∈ reorder.flatten then
     decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
+
   let translateValue (v : Expr) : MetaM Expr := do
-    let v ← match t.unfoldBoundaries with
-      | some b => b.cast (← b.insertBoundaries v) decl.type
-      | none => pure v
-    reorderLambda reorder <| ← applyReplacementLambda t dont v
-  let type ← match t.unfoldBoundaries with
-    | some b => b.insertBoundaries decl.type
-    | none => pure decl.type
-  decl := decl.updateType <| ← reorderForall reorder <| ← applyReplacementForall t dont <|
-    renameBinderNames t type
+    let mut v := v
+    if let some b := t.unfoldBoundaries then
+      v ← b.cast (← b.insertBoundaries v) decl.type
+    v ← reorderLambda reorder <| ← applyReplacementLambda t dont v
+    if let some b := t.unfoldBoundaries then
+      v ← b.unfoldInsertions v
+    return v
+
+  let mut type := decl.type
+  if let some b := t.unfoldBoundaries then
+    type ← b.insertBoundaries decl.type
+  type ← reorderForall reorder <| ← applyReplacementForall t dont <| renameBinderNames t type
+  if let some b := t.unfoldBoundaries then
+    type ← b.unfoldInsertions type
+  decl := decl.updateType type
+
   if let some v := decl.value? then
     decl := decl.updateValue <| ← translateValue v
   else if let .opaqueInfo info := decl then -- not covered by `value?`
@@ -903,10 +911,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 ← match t.unfoldBoundaries with
-    | some b => b.insertBoundaries srcDecl.type
-    | none => pure srcDecl.type
-  let srcType ← applyReplacementForall t cfg.dontTranslate srcType
+  let mut srcType := srcDecl.type
+  if let some b := t.unfoldBoundaries then
+    srcType ← b.insertBoundaries srcType
+  srcType ← applyReplacementForall t cfg.dontTranslate srcType
   let reorder' := guessReorder srcType tgtDecl.type
   trace[translate_detail] "The guessed reorder is {reorder'}"
   let reorder ←
@@ -922,12 +930,15 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
       pure reorder
     else
       pure reorder'
-  let srcType ← reorderForall reorder srcType
+  srcType ← reorderForall reorder srcType
+  if let some b := t.unfoldBoundaries then
+    srcType ← b.unfoldInsertions srcType
+
   if 0 ∈ reorder.flatten 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/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index dbcdddc9d7a09e..610b350572d3d3 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -26,7 +26,7 @@ Known limitations:
 public meta section
 
 namespace Mathlib.Tactic.ToDual
-open Lean Meta Elab Command Std Translate UnfoldBoundary
+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
@@ -40,12 +40,6 @@ syntax (name := to_dual_do_translate) "to_dual_do_translate" : attr
 @[inherit_doc TranslateData.doTranslateAttr]
 syntax (name := to_dual_dont_translate) "to_dual_dont_translate" : attr
 
-@[inherit_doc UnfoldBoundaryExt.unfolds]
-syntax (name := to_dual_dont_unfold) "to_dual_dont_unfold" : attr
-
-@[inherit_doc UnfoldBoundaryExt.casts]
-syntax (name := to_dual_cast) "to_dual_cast" : attr
-
 /-- The attribute `to_dual` can be used to automatically transport theorems
 and definitions (but not inductive types and structures) to their dual version.
 It uses the same implementation as `to_additive`.
@@ -111,32 +105,15 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
 
 @[inherit_doc UnfoldBoundaryExt.unfolds]
 initialize unfolds : NameMapExtension SimpTheorem ← registerNameMapExtension _
-initialize
-  registerBuiltinAttribute {
-    name := `to_dual_dont_unfold
-    descr := "The `to_dual_dont_unfold` attribute"
-    applicationTime := .afterCompilation
-    add := fun declName _ _ ↦ MetaM.run' do
-      let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
-      let some name ← mkSimpleEqThm declName name |
-        throwError "No unfold theorem could be generated for `{declName}`"
-      executeReservedNameAction name
-      unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true } }
 
 @[inherit_doc UnfoldBoundaryExt.casts]
-initialize casts : NameMapExtension Name ← registerNameMapExtension _
-initialize
-  registerBuiltinAttribute {
-    name := `to_dual_cast
-    descr := "The `to_dual_cast` attribute"
-    add := fun cast _ _ ↦ MetaM.run' do
-      let_expr Identification α _ := (← getConstInfo cast).type.getForallBody |
-        throwError "expected an `Identification`, not {cast}"
-      let .const declName _ := α.getAppFn | throwError "expected {α} to be a constant application"
-      casts.add declName cast }
+initialize casts : NameMapExtension (Name × Name) ← registerNameMapExtension _
+
+@[inherit_doc UnfoldBoundaryExt.insertionFuns]
+initialize insertionFuns : NameMapExtension Unit ← registerNameMapExtension _
 
 @[inherit_doc TranslateData.unfoldBoundaries]
-def unfoldBoundaries : UnfoldBoundaryExt := { unfolds, casts }
+def unfoldBoundaries : UnfoldBoundaryExt := { unfolds, casts, insertionFuns }
 
 @[inherit_doc TranslateData.argInfoAttr]
 initialize argInfoAttr : NameMapExtension ArgInfo ← registerNameMapExtension _
@@ -234,4 +211,88 @@ initialize registerBuiltinAttribute {
     applicationTime := .afterCompilation
   }
 
+/-- This function is based on `Lean.Meta.mkSimpleEqThm`. -/
+private def mkSimpleEqThm (declName : Name) (name : Name) (isThm : Bool)
+    (mkTypeVal : Expr → Expr → MetaM (Expr × Expr)) : MetaM Unit := do
+  let .defnInfo info ← getConstInfo declName | throwError "`{declName}` is not a definition"
+  lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+    let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
+    let (type, val) ← mkTypeVal lhs body
+    let type ← mkForallFVars xs type
+    let value ← mkLambdaFVars xs val
+    addDecl <| ←
+      if isThm then mkThmOrUnsafeDef {
+        name, type, value
+        levelParams := info.levelParams }
+      else
+        .defnDecl <$> mkDefinitionValInferringUnsafe name info.levelParams type value (.regular 0)
+
+elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
+  let declName := declName.getId
+  withDeclNameForAuxNaming declName do
+  let name ← mkAuxDeclName `_to_dual_insert_cast
+  Command.liftTermElabM do
+    mkSimpleEqThm declName name true fun lhs body => return (← mkEq lhs body, ← mkEqRefl lhs)
+  let dualName ← mkAuxDeclName `_to_dual_insert_cast
+  Command.liftTermElabM do
+    unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true }
+    let cinfo ← getConstInfo name
+    let dualType ← applyReplacementFun data cinfo.type
+    let value ← forallTelescope dualType fun xs dualTypeBody => do
+      -- Make the goal easier to prove by unfolding the lhs of the equality, if possible
+      let dualTypeBody' ← (do
+        if let mkApp2 eq lhs body := dualTypeBody then
+          if let some lhs ← unfoldDefinition? lhs then
+            return mkApp2 eq lhs body
+        return dualTypeBody)
+      let value ← elabTermEnsuringType valStx dualTypeBody'
+      synthesizeSyntheticMVarsNoPostponing
+      mkLambdaFVars xs (← instantiateMVars value)
+    addDecl <| ← mkThmOrUnsafeDef {
+      name := dualName, type := dualType, value
+      levelParams := cinfo.levelParams }
+  elabCommand <| ← `(command|
+    attribute [to_dual existing $(mkIdent name):ident] $(mkIdent dualName))
+
+elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command => do
+  let declName := declName.getId
+  withDeclNameForAuxNaming declName do
+  let name₁ ← mkAuxDeclName `_to_dual_insert_cast_fun
+  Command.liftTermElabM do mkSimpleEqThm declName name₁ false fun lhs body =>
+      return (.forallE `this lhs body .default, .lam `this lhs (.bvar 0) .default)
+  let dualName₁ ← mkAuxDeclName `_to_dual_insert_cast_fun
+  Command.liftTermElabM do
+    let cinfo₁ ← getConstInfo name₁
+    let dualType₁ ← applyReplacementFun data cinfo₁.type
+    let value ← forallTelescope dualType₁ fun xs dualTypeBody => do
+      let value ← elabTermEnsuringType valStx₁ dualTypeBody
+      synthesizeSyntheticMVarsNoPostponing
+      mkLambdaFVars xs (← instantiateMVars value)
+    addDecl <| .defnDecl <|
+      ← mkDefinitionValInferringUnsafe dualName₁ cinfo₁.levelParams dualType₁ value (.regular 0)
+  elabCommand <| ← `(command|
+    attribute [to_dual existing $(mkIdent name₁):ident] $(mkIdent dualName₁))
+  insertionFuns.add name₁ ()
+  insertionFuns.add dualName₁ ()
+
+  let name₂ ← mkAuxDeclName `_to_dual_insert_cast_invFun
+  casts.add declName (name₁, name₂)
+  Command.liftTermElabM do
+    mkSimpleEqThm declName name₂ false fun lhs body =>
+      return (.forallE `this body lhs .default, .lam `this lhs (.bvar 0) .default)
+  let dualName₂ ← mkAuxDeclName `_to_dual_insert_cast_invFun
+  Command.liftTermElabM do
+    let cinfo₂ ← getConstInfo name₂
+    let dualType₂ ← applyReplacementFun data cinfo₂.type
+    let value ← forallTelescope dualType₂ fun xs dualTypeBody => do
+      let value ← elabTermEnsuringType valStx₂ dualTypeBody
+      synthesizeSyntheticMVarsNoPostponing
+      mkLambdaFVars xs (← instantiateMVars value)
+    addDecl <| .defnDecl <|
+      ← mkDefinitionValInferringUnsafe dualName₂ cinfo₂.levelParams dualType₂ value (.regular 0)
+  elabCommand <| ← `(command|
+    attribute [to_dual existing $(mkIdent name₂):ident] $(mkIdent dualName₂))
+  insertionFuns.add name₂ ()
+  insertionFuns.add dualName₂ ()
+
 end Mathlib.Tactic.ToDual
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 325eeafefbbd5d..94c7c2975776ec 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -5,6 +5,7 @@ Authors: Jovan Gerbscheid
 -/
 module
 
+public meta import Lean.Meta.Tactic.Delta
 public meta import Batteries.Lean.NameMapAttribute
 public import Mathlib.Init
 
@@ -12,43 +13,27 @@ public import Mathlib.Init
 # Modify proof terms so that they don't rely on unfolding certain constants
 -/
 
-namespace Mathlib.Tactic.UnfoldBoundary
-
-public section identification
-
-universe u
-
-/-- `Identification` is used by translation attributes to insert abstraction boundaries in terms
-that need to be translated. -/
-structure Identification (α β : Type u) : Type u where
-  /-- The unfolding function. -/
-  toFun : α → β
-  /-- The refolding function. -/
-  invFun : β → α
-
-/-- The identity `Identification`. -/
-@[expose]
-def Identification.Id {α : Type u} : Identification α α where
-  toFun x := x
-  invFun x := x
-
-end identification
-
 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
-  casts : NameMap Name
+  /-- 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
 
-def withBlockUnfolding {α} (boundaries : UnfoldBoundaries) (x : MetaM α) : MetaM α := do
+def withBlockUnfolding {α} (b : UnfoldBoundaries) (x : MetaM α) : MetaM α := do
   withCanUnfoldPred (fun _ cinfo =>
-    return !boundaries.unfolds.contains cinfo.name && !boundaries.casts.contains cinfo.name) x
+    return !b.unfolds.contains cinfo.name
+      && !b.casts.contains cinfo.name) x
 
 def unfold (e : Expr) (unfolds : NameMap SimpTheorem) : MetaM Simp.Result := do
   let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
-    (congrTheorems := (← getSimpCongrTheorems))
   (·.1) <$> Simp.main e ctx (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
@@ -58,114 +43,114 @@ where
     return .done r
 
 
-def refoldConsts (e expectedType : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
+def refoldConsts (e expectedType : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
   let goal ← mkFreshExprMVar expectedType
   go e goal.mvarId!
   instantiateMVars goal
 where
   go (e : Expr) (goal : MVarId) : MetaM Unit := do
-    let r ← unfold (← goal.getType) boundaries.unfolds
+    let r ← unfold (← goal.getType) b.unfolds
     let goal ← match r.proof? with
       | some proof => goal.replaceTargetEq r.expr proof
       | none => pure goal
     forallTelescope (← goal.getType) fun xs tgt => do
-      if let .const c _ := (← whnf tgt).getAppFn then
-        if let some cast := boundaries.casts.find? c then
-          let cast ← mkConstWithFreshMVarLevels cast
-          let (mvars, _, type) ← forallMetaTelescope (← inferType cast)
-          let_expr f@Identification α β := type | throwError "expected `Identification`, not {type}"
-          if ← isDefEq tgt α then
-            let goal' ← mkFreshExprMVar (← instantiateMVars β)
-            go (mkAppN e xs) goal'.mvarId!
-            goal.assign <| ← mkLambdaFVars xs <|
-              mkApp4 (.const ``Identification.invFun f.constLevels!) α β (mkAppN cast mvars) goal'
-            return
-          else
-            throwError "identification `{cast}` could not be applied at {tgt}"
+      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
+          let .forallE _ α _ _ ← inferType cast | throwError s!"{cast} is not of the right form"
+          let goal' ← mkFreshExprMVar α
+          go (mkAppN e xs) goal'.mvarId!
+          goal.assign <| ← mkLambdaFVars xs <| .app cast goal'
+          return
       if ← isDefEq (← goal.getType) (← inferType e) then
         goal.assign e
       else
         throwError "Error: could not cast {e} into the type {← goal.getType}."
 
-def unfoldConsts (e : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
+def unfoldConsts (e : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
   let eType ← inferType e
-  if let .const c _ := (← whnf eType).getAppFn then
-    if let some cast := boundaries.casts.find? c then
-      let cast ← mkConstWithFreshMVarLevels cast
-      let (mvars, _, type) ← forallMetaTelescope (← inferType cast)
-      let_expr f@Identification α β := type | throwError "expected Identification, not {type}"
-      if ← isDefEq eType α then
-        let e := mkApp4 (.const ``Identification.toFun f.constLevels!) α β (mkAppN cast mvars) e
-        return ← unfoldConsts e boundaries
-      else
-        throwError "Error: identification `{cast}` could not be applied at {eType}"
-  let r ← unfold eType boundaries.unfolds
+  let eTypeWhnf ← whnf eType
+  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
+      return ← unfoldConsts e b
+  let r ← unfold eType b.unfolds
   let some pf := r.proof? | return e
   mkAppOptM ``cast #[eType, r.expr, pf, e]
 
 /-- Given an expression `e` with expected type `type`, if `e` doesn't have that type,
 use a cast to turn `e` into that type. -/
-def mkAppWithCast (f a : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr :=
+def mkAppWithCast (f a : Expr) (b : UnfoldBoundaries) : MetaM Expr :=
   try
     checkApp f a
     return f.app a
   catch _ =>
-    let f ← unfoldConsts f boundaries
+    let f ← unfoldConsts f b
     let .forallE _ d _ _ ← whnf (← inferType f) | throwFunctionExpected f
-    let a ← unfoldConsts a boundaries
-    let a ← refoldConsts a d boundaries
+    let a ← unfoldConsts a b
+    let a ← refoldConsts a d b
     return f.app a
 
-def mkCast (e expectedType : Expr) (boundaries : UnfoldBoundaries) : MetaM Expr := do
+def mkCast (e expectedType : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
   if ← isDefEq (← inferType e) expectedType then
     return e
-  let e ← unfoldConsts e boundaries
-  let e ← refoldConsts e expectedType boundaries
+  let e ← unfoldConsts e b
+  let e ← refoldConsts e expectedType b
   if ← isDefEq (← inferType e) expectedType then
     return e
   else
     throwError "{e} does not match the expected type {expectedType}"
 
-public section
-
 /-- Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded. -/
-structure UnfoldBoundaryExt where
-  /-- The `dont_unfold` attribute is used to tag declarations `foo` that should not be unfolded in
-  a proof that is translated. Instead, the unfold theorem `foo.eq_def` is inserted. -/
+public structure UnfoldBoundaryExt where
+  /-- The `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 then may be translated by the translation attribute. -/
   unfolds : NameMapExtension SimpTheorem
-  /-- The `cast` attribute is used to tag casting functions `foo.val` for declarations `foo` that
-  should not be unfolded in a proof that is translated. -/
-  casts : NameMapExtension Name
+  /-- The `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`. -/
-def UnfoldBoundaryExt.cast (e expectedType : Expr) (boundaries : UnfoldBoundaryExt) :
-    MetaM Expr := do
-  let env ← getEnv
-  let boundaries := {
-    unfolds := boundaries.unfolds.getState env
-    casts := boundaries.casts.getState env }
-  withBlockUnfolding boundaries do withTransparency TransparencyMode.all do
-    mkCast e expectedType boundaries
-
-/-- Modify `e` so that it is well typed if the constants in `boundaries` cannot be unfolded. -/
-def UnfoldBoundaryExt.insertBoundaries (e : Expr) (boundaries : UnfoldBoundaryExt) :
-    MetaM Expr := do
-  let env ← getEnv
-  let boundaries := {
-    unfolds := boundaries.unfolds.getState env
-    casts := boundaries.casts.getState env }
-  withBlockUnfolding boundaries do withTransparency TransparencyMode.all do
-    instantiateMVars <| ← transform e (post := fun e ↦ e.withApp fun f args => do
+public def UnfoldBoundaryExt.cast (e expectedType : Expr) (b : UnfoldBoundaryExt) : MetaM Expr := do
+  let b ← b.toUnfoldBoundaries
+  withBlockUnfolding b do withTransparency TransparencyMode.all do
+    mkCast e expectedType b
+
+/-- 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 (e : Expr) (b : UnfoldBoundaryExt) : MetaM Expr := do
+  let b ← b.toUnfoldBoundaries
+  withBlockUnfolding b do withTransparency TransparencyMode.all do
+    transform e (post := fun e ↦ e.withApp fun f args => do
       let mut f := f
       for arg in args do
         try
-          f ← mkAppWithCast f arg boundaries
+          f ← mkAppWithCast f arg b
         catch e =>
           throwError "failed to deal with {f} applied to {arg}\n{e.toMessageData}"
       return .done f)
 
-end
-
-end
+/-- Unfold all of the auxiliary functions that were insertedy as unfold boundaries. -/
+public def UnfoldBoundaryExt.unfoldInsertions (e : Expr) (b : UnfoldBoundaryExt) :
+    CoreM Expr := do
+  let b ← b.toUnfoldBoundaries
+  Meta.deltaExpand e b.insertionFuns.contains
 
 end Mathlib.Tactic.UnfoldBoundary

From 58626423ce5772a1bdf8f70bc5220d1d09ef216d Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Mon, 15 Dec 2025 14:55:52 +0000
Subject: [PATCH 06/26] missing `partial`

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 94c7c2975776ec..2bd85dc2779913 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -42,8 +42,7 @@ where
     let some r ← Simp.tryTheorem? e thm | return .continue
     return .done r
 
-
-def refoldConsts (e expectedType : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
+partial def refoldConsts (e expectedType : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
   let goal ← mkFreshExprMVar expectedType
   go e goal.mvarId!
   instantiateMVars goal
@@ -68,7 +67,7 @@ where
       else
         throwError "Error: could not cast {e} into the type {← goal.getType}."
 
-def unfoldConsts (e : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
+partial def unfoldConsts (e : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
   let eType ← inferType e
   let eTypeWhnf ← whnf eType
   if let .const c us := eTypeWhnf.getAppFn then

From 4360943462bf2d7c78a83cff6f64a6069f704f14 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Mon, 15 Dec 2025 15:58:48 +0000
Subject: [PATCH 07/26] adaptations

---
 Mathlib/Order/Defs/PartialOrder.lean |  5 ----
 Mathlib/Order/Hom/Basic.lean         | 37 ++++++++++++++------------
 Mathlib/Order/Interval/Set/Defs.lean | 39 ++++++++++++----------------
 Mathlib/Order/Monotone/Defs.lean     | 27 ++++++++++---------
 Mathlib/Tactic/Translate/ToDual.lean | 10 +++++--
 5 files changed, 61 insertions(+), 57 deletions(-)

diff --git a/Mathlib/Order/Defs/PartialOrder.lean b/Mathlib/Order/Defs/PartialOrder.lean
index 55daadb52b5ab9..48aa81af735c23 100644
--- a/Mathlib/Order/Defs/PartialOrder.lean
+++ b/Mathlib/Order/Defs/PartialOrder.lean
@@ -146,8 +146,6 @@ instance instTransGEGT : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'
 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`.
 -/
@@ -213,9 +211,6 @@ def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
       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/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index bfc9060b46030b..b4c4369154f25f 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -92,6 +92,10 @@ This definition is an abbreviation of `RelEmbedding (≤) (≤)`. -/
 abbrev OrderEmbedding (α β : Type*) [LE α] [LE β] :=
   @RelEmbedding α β (· ≤ ·) (· ≤ ·)
 
+to_dual_insert_cast_fun OrderEmbedding :=
+  { this with map_rel_iff' := by grind [this.map_rel_iff']},
+  { this with map_rel_iff' := by grind [this.map_rel_iff']}
+
 /-- Notation for an `OrderEmbedding`. -/
 infixl:25 " ↪o " => OrderEmbedding
 
@@ -100,6 +104,10 @@ This definition is an abbreviation of `RelIso (≤) (≤)`. -/
 abbrev OrderIso (α β : Type*) [LE α] [LE β] :=
   @RelIso α β (· ≤ ·) (· ≤ ·)
 
+to_dual_insert_cast_fun OrderIso :=
+  { this with map_rel_iff' := by grind [this.map_rel_iff']},
+  { this with map_rel_iff' := by grind [this.map_rel_iff']}
+
 /-- Notation for an `OrderIso`. -/
 infixl:25 " ≃o " => OrderIso
 
@@ -109,6 +117,8 @@ section
 abbrev OrderHomClass (F : Type*) (α β : outParam Type*) [LE α] [LE β] [FunLike F α β] :=
   RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)
 
+to_dual_insert_cast OrderHomClass := by grind [RelHomClass]
+
 /-- `OrderIsoClass F α β` states that `F` is a type of order isomorphisms.
 
 You should extend this class when you extend `OrderIso`. -/
@@ -117,6 +127,8 @@ class OrderIsoClass (F : Type*) (α β : outParam Type*) [LE α] [LE β] [EquivL
   /-- An order isomorphism respects `≤`. -/
   map_le_map_iff (f : F) {a b : α} : f a ≤ f b ↔ a ≤ b
 
+attribute [to_dual self] OrderIsoClass.map_le_map_iff
+
 end
 
 export OrderIsoClass (map_le_map_iff)
@@ -170,28 +182,25 @@ section LE
 
 variable [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β]
 
-@[simp]
+@[to_dual (attr := simp) le_map_inv_iff]
 theorem map_inv_le_iff (f : F) {a : α} {b : β} : EquivLike.inv f b ≤ a ↔ b ≤ f a := by
   convert (map_le_map_iff f).symm
   exact (EquivLike.right_inv f _).symm
 
+@[to_dual self]
 theorem map_inv_le_map_inv_iff (f : F) {a b : β} :
     EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a := by
   simp
 
-@[simp]
-theorem le_map_inv_iff (f : F) {a : α} {b : β} : a ≤ EquivLike.inv f b ↔ f a ≤ b := by
-  convert (map_le_map_iff f).symm
-  exact (EquivLike.right_inv _ _).symm
-
 end LE
 
 variable [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β]
 
+@[to_dual self]
 theorem map_lt_map_iff (f : F) {a b : α} : f a < f b ↔ a < b :=
   lt_iff_lt_of_le_iff_le' (map_le_map_iff f) (map_le_map_iff f)
 
-@[simp]
+@[to_dual (attr := simp) lt_map_inv_iff]
 theorem map_inv_lt_iff (f : F) {a : α} {b : β} : EquivLike.inv f b < a ↔ b < f a := by
   rw [← map_lt_map_iff f]
   simp only [EquivLike.apply_inv_apply]
@@ -200,11 +209,6 @@ theorem map_inv_lt_map_inv_iff (f : F) {a b : β} :
     EquivLike.inv f b < EquivLike.inv f a ↔ b < a := by
   simp
 
-@[simp]
-theorem lt_map_inv_iff (f : F) {a : α} {b : β} : a < EquivLike.inv f b ↔ f a < b := by
-  rw [← map_lt_map_iff f]
-  simp only [EquivLike.apply_inv_apply]
-
 end OrderIsoClass
 
 namespace OrderHom
@@ -282,18 +286,19 @@ instance : Preorder (α →o β) :=
 instance {β : Type*} [PartialOrder β] : PartialOrder (α →o β) :=
   @PartialOrder.lift (α →o β) (α → β) _ toFun ext
 
+@[to_dual self]
 theorem le_def {f g : α →o β} : f ≤ g ↔ ∀ x, f x ≤ g x :=
   Iff.rfl
 
-@[simp, norm_cast]
+@[simp, norm_cast, to_dual self]
 theorem coe_le_coe {f g : α →o β} : (f : α → β) ≤ g ↔ f ≤ g :=
   Iff.rfl
 
-@[simp]
+@[simp, to_dual self]
 theorem mk_le_mk {f g : α → β} {hf hg} : mk f hf ≤ mk g hg ↔ f ≤ g :=
   Iff.rfl
 
-@[mono]
+@[mono, to_dual self]
 theorem apply_mono {f g : α →o β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y :=
   (h₁ x).trans <| g.mono h₂
 
@@ -317,7 +322,7 @@ theorem curry_symm_apply (f : α →o β →o γ) (x : α × β) : curry.symm f
 def comp (g : β →o γ) (f : α →o β) : α →o γ :=
   ⟨g ∘ f, g.mono.comp f.mono⟩
 
-@[mono]
+@[mono, to_dual self]
 theorem comp_mono ⦃g₁ g₂ : β →o γ⦄ (hg : g₁ ≤ g₂) ⦃f₁ f₂ : α →o β⦄ (hf : f₁ ≤ f₂) :
     g₁.comp f₁ ≤ g₂.comp f₂ := fun _ => (hg _).trans (g₂.mono <| hf _)
 
diff --git a/Mathlib/Order/Interval/Set/Defs.lean b/Mathlib/Order/Interval/Set/Defs.lean
index 9a76ae982e8889..d11c2f33a3c63f 100644
--- a/Mathlib/Order/Interval/Set/Defs.lean
+++ b/Mathlib/Order/Interval/Set/Defs.lean
@@ -32,27 +32,23 @@ 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), to_dual_dont_unfold]
+@[to_dual self (reorder := a b)]
 def Ioo (a b : α) := { x | a < x ∧ x < b }
 
-@[to_dual existing eq_def]
-theorem Ioo.eq_def_dual (a b : α) : Ioo b a = { x | x < a ∧ b < x } := Set.ext fun _ ↦ And.comm
+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)$. -/
-@[to_dual_dont_unfold]
 def Ico (a b : α) := { x | a ≤ x ∧ x < b }
 
 /-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
-@[to_dual existing (reorder := a b) Ico, to_dual_dont_unfold]
+@[to_dual existing (reorder := a b)]
 def Ioc (a b : α) := { x | a < x ∧ x ≤ b }
 
-@[to_dual existing eq_def]
-theorem Ico.eq_def_dual (a b : α) : Ico b a = { x | x < a ∧ b ≤ x } := Set.ext fun _ ↦ And.comm
-@[to_dual existing eq_def]
-theorem Ioc.eq_def_dual (a b : α) : Ioc b a = { x | x ≤ a ∧ b < x } := Set.ext fun _ ↦ And.comm
+to_dual_insert_cast Ico := by grind
+to_dual_insert_cast Ioc := by grind
 
 @[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
@@ -60,29 +56,28 @@ theorem Ioc.eq_def_dual (a b : α) : Ioc b a = { x | x ≤ a ∧ b < x } := Set.
 @[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
 
-/-- `Iio b` is the left-infinite right-open interval $(-∞, b)$. -/
-@[to_dual Ioi /-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/]
-def Iio (b : α) := { x | x < b }
-
-@[to_dual (attr := simp, grind =) mem_Ioi] theorem mem_Iio : x ∈ Iio b ↔ x < b := Iff.rfl
-@[to_dual Ioi_def] theorem Iio_def (a : α) : { x | x < a } = Iio a := rfl
-
 /-- `Icc a b` is the left-closed right-closed interval $[a, b]$. -/
-@[to_dual self (reorder := a b), to_dual_dont_unfold]
+@[to_dual self (reorder := a b)]
 def Icc (a b : α) := { x | a ≤ x ∧ x ≤ b }
 
-@[to_dual existing eq_def]
-theorem Icc.eq_def_dual (a b : α) : Icc b a = { x | x ≤ a ∧ b ≤ x } := Set.ext fun _ ↦ And.comm
+to_dual_insert_cast Icc := by grind
 
 @[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
 
+/-- `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 }
+
+@[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
+
 /-- `Iic b` is the left-infinite right-closed interval $(-∞, b]$. -/
-@[to_dual Ici /-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/]
+@[to_dual /-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/]
 def Iic (b : α) := { x | x ≤ b }
 
-@[to_dual (attr := simp, grind =) mem_Ici] theorem mem_Iic : x ∈ Iic b ↔ x ≤ b := Iff.rfl
-@[to_dual Ici_def] theorem Iic_def (b : α) : { x | x ≤ b } = Iic b := 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
diff --git a/Mathlib/Order/Monotone/Defs.lean b/Mathlib/Order/Monotone/Defs.lean
index 15cd199f8ebd6a..85041b628b8b1e 100644
--- a/Mathlib/Order/Monotone/Defs.lean
+++ b/Mathlib/Order/Monotone/Defs.lean
@@ -63,48 +63,51 @@ 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
 
-attribute [to_dual_dont_unfold]
-  Monotone Antitone MonotoneOn AntitoneOn StrictMono StrictAnti StrictMonoOn StrictAntiOn
-
-set_option linter.style.longLine false
-@[to_dual existing eq_def] theorem Monotone.eq_def_dual (f : α → β) : Monotone f = ∀ ⦃a b⦄, b ≤ a → f b ≤ f a := by grind [Monotone.eq_def]
-@[to_dual existing eq_def] theorem Antitone.eq_def_dual (f : α → β) : Antitone f = ∀ ⦃a b⦄, b ≤ a → f a ≤ f b := by grind [Antitone.eq_def]
-@[to_dual existing eq_def] theorem MonotoneOn.eq_def_dual (f : α → β) (s : Set α) : MonotoneOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b ≤ a → f b ≤ f a := by grind [MonotoneOn.eq_def]
-@[to_dual existing eq_def] theorem AntitoneOn.eq_def_dual (f : α → β) (s : Set α) : AntitoneOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b ≤ a → f a ≤ f b := by grind [AntitoneOn.eq_def]
-@[to_dual existing eq_def] theorem StrictMono.eq_def_dual (f : α → β) : StrictMono f = ∀ ⦃a b⦄, b < a → f b < f a := by grind [StrictMono.eq_def]
-@[to_dual existing eq_def] theorem StrictAnti.eq_def_dual (f : α → β) : StrictAnti f = ∀ ⦃a b⦄, b < a → f a < f b := by grind [StrictAnti.eq_def]
-@[to_dual existing eq_def] theorem StrictMonoOn.eq_def_dual (f : α → β) (s : Set α) : StrictMonoOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b < a → f b < f a := by grind [StrictMonoOn.eq_def]
-@[to_dual existing eq_def] theorem StrictAntiOn.eq_def_dual (f : α → β) (s : Set α) : StrictAntiOn f s = ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), b < a → f a < f b := by grind [StrictAntiOn.eq_def]
+to_dual_insert_cast StrictAntiOn := by grind
 
 end MonotoneDef
 
diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index 071eb2ce13b2d0..6bea2081591c8e 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -149,6 +149,12 @@ 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"]),
 
   ("epi", ["Mono"]),
   /- `mono` can also refer to monotone, so we don't translate it. -/
@@ -227,7 +233,7 @@ private def mkSimpleEqThm (declName : Name) (name : Name) (isThm : Bool)
         .defnDecl <$> mkDefinitionValInferringUnsafe name info.levelParams type value (.regular 0)
 
 elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
-  let declName := declName.getId
+  let declName ← Command.liftCoreM do realizeGlobalConstNoOverloadWithInfo declName
   withDeclNameForAuxNaming declName do
   let name ← mkAuxDeclName `_to_dual_insert_cast
   Command.liftTermElabM do
@@ -254,7 +260,7 @@ elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
     attribute [to_dual existing $(mkIdent name):ident] $(mkIdent dualName))
 
 elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command => do
-  let declName := declName.getId
+  let declName ← Command.liftCoreM do realizeGlobalConstNoOverloadWithInfo declName
   withDeclNameForAuxNaming declName do
   let name₁ ← mkAuxDeclName `_to_dual_insert_cast_fun
   Command.liftTermElabM do mkSimpleEqThm declName name₁ false fun lhs body =>

From 43dd223d65171354bef05ea696d1f44c35481e74 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Thu, 18 Dec 2025 13:22:52 +0100
Subject: [PATCH 08/26] fix the problem with OrderEmbedding

---
 Mathlib/Order/Cover.lean     |  9 ++++++---
 Mathlib/Order/Hom/Basic.lean | 12 ++++--------
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean
index fb6d1157aedd66..fb37c9f1662f50 100644
--- a/Mathlib/Order/Cover.lean
+++ b/Mathlib/Order/Cover.lean
@@ -102,29 +102,32 @@ theorem wcovBy_iff_Ioo_eq : a ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅ :=
 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⟩
 
+@[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
 
diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index b4c4369154f25f..289f72b4b75764 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -92,10 +92,6 @@ This definition is an abbreviation of `RelEmbedding (≤) (≤)`. -/
 abbrev OrderEmbedding (α β : Type*) [LE α] [LE β] :=
   @RelEmbedding α β (· ≤ ·) (· ≤ ·)
 
-to_dual_insert_cast_fun OrderEmbedding :=
-  { this with map_rel_iff' := by grind [this.map_rel_iff']},
-  { this with map_rel_iff' := by grind [this.map_rel_iff']}
-
 /-- Notation for an `OrderEmbedding`. -/
 infixl:25 " ↪o " => OrderEmbedding
 
@@ -104,13 +100,13 @@ This definition is an abbreviation of `RelIso (≤) (≤)`. -/
 abbrev OrderIso (α β : Type*) [LE α] [LE β] :=
   @RelIso α β (· ≤ ·) (· ≤ ·)
 
-to_dual_insert_cast_fun OrderIso :=
-  { this with map_rel_iff' := by grind [this.map_rel_iff']},
-  { this with map_rel_iff' := by grind [this.map_rel_iff']}
-
 /-- Notation for an `OrderIso`. -/
 infixl:25 " ≃o " => OrderIso
 
+-- These instances are here just to make `to_dual` work correctly
+instance (α β : Type*) [LE α] [LE β] : FunLike (α ↪o β) α β := RelEmbedding.instFunLike
+instance (α β : Type*) [LE α] [LE β] : FunLike (α ≃o β) α β := RelIso.instFunLike
+
 section
 
 /-- `OrderHomClass F α b` asserts that `F` is a type of `≤`-preserving morphisms. -/

From cc31e3929a1055042cbc365c1a965f9f53175f9c Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 19 Dec 2025 02:58:31 +0100
Subject: [PATCH 09/26] .

---
 Mathlib/Order/Cover.lean             | 2 ++
 Mathlib/Order/Hom/Basic.lean         | 2 --
 Mathlib/Tactic/ToDual.lean           | 2 +-
 Mathlib/Tactic/Translate/Core.lean   | 2 +-
 Mathlib/Tactic/Translate/ToDual.lean | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean
index fb37c9f1662f50..519dabd7d78385 100644
--- a/Mathlib/Order/Cover.lean
+++ b/Mathlib/Order/Cover.lean
@@ -131,8 +131,10 @@ theorem toDual_wcovBy_toDual_iff : toDual b ⩿ toDual a ↔ a ⩿ b :=
 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/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index 95d1402fcb6872..ba81c59ed4ce6e 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -113,8 +113,6 @@ section
 abbrev OrderHomClass (F : Type*) (α β : outParam Type*) [LE α] [LE β] [FunLike F α β] :=
   RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)
 
-to_dual_insert_cast OrderHomClass := by grind [RelHomClass]
-
 /-- `OrderIsoClass F α β` states that `F` is a type of order isomorphisms.
 
 You should extend this class when you extend `OrderIso`. -/
diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean
index 2b5f365c7736f2..0951366ad4d365 100644
--- a/Mathlib/Tactic/ToDual.lean
+++ b/Mathlib/Tactic/ToDual.lean
@@ -5,7 +5,7 @@ Authors: Jovan Gerbscheid
 -/
 module
 
-public import Mathlib.Tactic.Translate.ToDual
+public meta import Mathlib.Tactic.Translate.ToDual
 import all Init.Core  -- TODO: for accessing proofs
 
 
diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index b29b77fa3fcc8e..aea6a51c15eaaa 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -19,7 +19,7 @@ public meta import Mathlib.Lean.Name
 public meta import Mathlib.Tactic.Eqns -- just to copy the attribute
 public meta import Mathlib.Tactic.Simps.Basic
 public meta import Mathlib.Tactic.Translate.GuessName
-public import Mathlib.Tactic.Translate.UnfoldBoundary
+public meta import Mathlib.Tactic.Translate.UnfoldBoundary
 public meta import Lean.Meta.CoeAttr
 
 /-!
diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index 6bea2081591c8e..cf8cb85b06c211 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 meta import Mathlib.Tactic.Translate.Core
 
 /-!
 # The `@[to_dual]` attribute.

From d4ff223cff68b8f7a1ba7de0f4e4dc208c92c96f Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 19 Dec 2025 12:45:50 +0100
Subject: [PATCH 10/26] golf and docs

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 89 ++++++++++++--------
 1 file changed, 55 insertions(+), 34 deletions(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 2bd85dc2779913..00ef6800c03b1e 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -11,6 +11,21 @@ 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, using `isDefEq`, and whenever
+there is a 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 folding. This is for Types, where we
+  cannot express their equivalence with an equality. For example `DecidableLE`.
 -/
 
 meta section
@@ -27,29 +42,51 @@ structure UnfoldBoundaries where
   /-- The functions that we want to unfold again after the translation has happened. -/
   insertionFuns : NameMap Unit
 
+/-- Modify the `MetaM` context to not allow unfolding the constants for which we would like
+to insert explicit casts. -/
 def withBlockUnfolding {α} (b : UnfoldBoundaries) (x : MetaM α) : MetaM α := do
   withCanUnfoldPred (fun _ cinfo =>
     return !b.unfolds.contains cinfo.name
       && !b.casts.contains cinfo.name) x
 
-def unfold (e : Expr) (unfolds : NameMap SimpTheorem) : MetaM Simp.Result := do
+def run {α} (b : UnfoldBoundaries) (x : SimpM α) : MetaM α :=
+  withBlockUnfolding b do withTransparency TransparencyMode.all do
   let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
-  (·.1) <$> Simp.main e ctx (methods := { pre })
+  (·.1) <$> Simp.SimpM.run ctx {} (methods := { pre }) x
 where
   pre (e : Expr) : SimpM Simp.Step := do
     let .const c _ ← whnf e.getAppFn | return .continue
-    let some thm := unfolds.find? c | return .continue
+    let some thm := b.unfolds.find? c | return .continue
     let some r ← Simp.tryTheorem? e thm | return .continue
     return .done r
 
-partial def refoldConsts (e expectedType : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
+/-- 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 r ← Simp.simp eType
+    if let some pf := r.proof? then
+      mkAppOptM ``cast #[eType, r.expr, pf, e]
+    else
+      pure 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
+      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) : MetaM Unit := do
-    let r ← unfold (← goal.getType) b.unfolds
-    let goal ← match r.proof? with
+  go (e : Expr) (goal : MVarId) : SimpM Unit := do
+    let goal ← do
+      let r ← Simp.simp (← goal.getType)
+      match r.proof? with
       | some proof => goal.replaceTargetEq r.expr proof
       | none => pure goal
     forallTelescope (← goal.getType) fun xs tgt => do
@@ -65,41 +102,26 @@ where
       if ← isDefEq (← goal.getType) (← inferType e) then
         goal.assign e
       else
-        throwError "Error: could not cast {e} into the type {← goal.getType}."
-
-partial def unfoldConsts (e : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
-  let eType ← inferType e
-  let eTypeWhnf ← whnf eType
-  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
-      return ← unfoldConsts e b
-  let r ← unfold eType b.unfolds
-  let some pf := r.proof? | return e
-  mkAppOptM ``cast #[eType, r.expr, pf, e]
+        throwError "Failed to insert casts to make {e} have type {← goal.getType}."
 
 /-- Given an expression `e` with expected type `type`, if `e` doesn't have that type,
 use a cast to turn `e` into that type. -/
-def mkAppWithCast (f a : Expr) (b : UnfoldBoundaries) : MetaM Expr :=
+def mkAppWithCast (f a : Expr) (b : UnfoldBoundaries) : SimpM Expr :=
   try
     checkApp f a
     return f.app a
   catch _ =>
-    let f ← unfoldConsts f b
+    let f ← unfoldConsts b f
     let .forallE _ d _ _ ← whnf (← inferType f) | throwFunctionExpected f
-    let a ← unfoldConsts a b
-    let a ← refoldConsts a d b
+    let a ← unfoldConsts b a
+    let a ← refoldConsts b a d
     return f.app a
 
-def mkCast (e expectedType : Expr) (b : UnfoldBoundaries) : MetaM Expr := do
+def mkCast (e expectedType : Expr) (b : UnfoldBoundaries) : SimpM Expr := do
   if ← isDefEq (← inferType e) expectedType then
     return e
-  let e ← unfoldConsts e b
-  let e ← refoldConsts e expectedType b
-  if ← isDefEq (← inferType e) expectedType then
-    return e
-  else
-    throwError "{e} does not match the expected type {expectedType}"
+  let e ← unfoldConsts b e
+  refoldConsts b e expectedType
 
 /-- Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded. -/
 public structure UnfoldBoundaryExt where
@@ -126,7 +148,7 @@ def UnfoldBoundaryExt.toUnfoldBoundaries (b : UnfoldBoundaryExt) :
 /-- Modify `e` so that it has type `expectedType`. -/
 public def UnfoldBoundaryExt.cast (e expectedType : Expr) (b : UnfoldBoundaryExt) : MetaM Expr := do
   let b ← b.toUnfoldBoundaries
-  withBlockUnfolding b do withTransparency TransparencyMode.all do
+  run b do
     mkCast e expectedType b
 
 /-- Modify `e` so that it is well typed if the constants in `b` cannot be unfolded.
@@ -136,7 +158,7 @@ Note: it may be that `e` contains some constant whose type is not well typed in
   It seems that this approximation works well enough. -/
 public def UnfoldBoundaryExt.insertBoundaries (e : Expr) (b : UnfoldBoundaryExt) : MetaM Expr := do
   let b ← b.toUnfoldBoundaries
-  withBlockUnfolding b do withTransparency TransparencyMode.all do
+  run b do
     transform e (post := fun e ↦ e.withApp fun f args => do
       let mut f := f
       for arg in args do
@@ -147,8 +169,7 @@ public def UnfoldBoundaryExt.insertBoundaries (e : Expr) (b : UnfoldBoundaryExt)
       return .done f)
 
 /-- Unfold all of the auxiliary functions that were insertedy as unfold boundaries. -/
-public def UnfoldBoundaryExt.unfoldInsertions (e : Expr) (b : UnfoldBoundaryExt) :
-    CoreM Expr := do
+public def UnfoldBoundaryExt.unfoldInsertions (e : Expr) (b : UnfoldBoundaryExt) : CoreM Expr := do
   let b ← b.toUnfoldBoundaries
   Meta.deltaExpand e b.insertionFuns.contains
 

From 74a71e2d8545812c0c749f13227ab0b4f3918679 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 19 Dec 2025 21:36:03 +0100
Subject: [PATCH 11/26] fix

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 00ef6800c03b1e..e16d8ca3958321 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -52,13 +52,13 @@ def withBlockUnfolding {α} (b : UnfoldBoundaries) (x : MetaM α) : MetaM α :=
 def run {α} (b : UnfoldBoundaries) (x : SimpM α) : MetaM α :=
   withBlockUnfolding b do withTransparency TransparencyMode.all do
   let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
-  (·.1) <$> Simp.SimpM.run ctx {} (methods := { pre }) x
+  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 .done r
+    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

From 8c173d4a67bd3d9a25f64d0cbf23bca1ccfb2734 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 00:36:26 +0100
Subject: [PATCH 12/26] improvements

---
 Mathlib/Tactic/ToDual.lean                   |   4 +-
 Mathlib/Tactic/Translate/Core.lean           |   6 +-
 Mathlib/Tactic/Translate/ToDual.lean         | 122 +++++++------------
 Mathlib/Tactic/Translate/UnfoldBoundary.lean |  51 ++++----
 4 files changed, 78 insertions(+), 105 deletions(-)

diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean
index 0951366ad4d365..e51c25fe2db639 100644
--- a/Mathlib/Tactic/ToDual.lean
+++ b/Mathlib/Tactic/ToDual.lean
@@ -17,8 +17,8 @@ public meta section
 
 attribute [to_dual self (reorder := 3 4)] LE.le LT.lt GE.ge GT.gt
 
-to_dual_insert_cast_fun DecidableLE := fun a b ↦ this b a, fun a b ↦ this b a
-to_dual_insert_cast_fun DecidableLT := fun a b ↦ this b a, fun a b ↦ this b a
+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 aea6a51c15eaaa..6851c450081bea 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -540,7 +540,7 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
   let translateValue (v : Expr) : MetaM Expr := do
     let mut v := v
     if let some b := t.unfoldBoundaries then
-      v ← b.cast (← b.insertBoundaries v) decl.type
+      v ← b.cast (← b.insertBoundaries v t.attrName) decl.type t.attrName
     v ← reorderLambda reorder <| ← applyReplacementLambda t dont v
     if let some b := t.unfoldBoundaries then
       v ← b.unfoldInsertions v
@@ -548,7 +548,7 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
 
   let mut type := decl.type
   if let some b := t.unfoldBoundaries then
-    type ← b.insertBoundaries decl.type
+    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
@@ -882,7 +882,7 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
       universe levels, but '{tgt}' has {tgtDecl.levelParams.length} universe levels"
   let mut srcType := srcDecl.type
   if let some b := t.unfoldBoundaries then
-    srcType ← b.insertBoundaries srcType
+    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'}"
diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index cf8cb85b06c211..d3cc985c087793 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -216,88 +216,58 @@ initialize registerBuiltinAttribute {
     applicationTime := .afterCompilation
   }
 
-/-- This function is based on `Lean.Meta.mkSimpleEqThm`. -/
-private def mkSimpleEqThm (declName : Name) (name : Name) (isThm : Bool)
-    (mkTypeVal : Expr → Expr → MetaM (Expr × Expr)) : MetaM Unit := do
+private inductive CastKind where
+| eq | unfoldFun | refoldFun
+
+private 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
+
+private def CastKind.mkProof (lhs : Expr) : CastKind → MetaM Expr
+  | .eq => mkEqRefl lhs
+  | _ => return .lam `_ lhs (.bvar 0) .default
+
+private def elabInsertCast (declName : Name) (castKind : CastKind) (stx : Term) :
+    CommandElabM (Name × Name) :=
+  Command.liftTermElabM do withDeclNameForAuxNaming declName do
   let .defnInfo info ← getConstInfo declName | throwError "`{declName}` is not a definition"
   lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
-    let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
-    let (type, val) ← mkTypeVal lhs body
-    let type ← mkForallFVars xs type
-    let value ← mkLambdaFVars xs val
-    addDecl <| ←
-      if isThm then mkThmOrUnsafeDef {
-        name, type, value
-        levelParams := info.levelParams }
-      else
-        .defnDecl <$> mkDefinitionValInferringUnsafe name info.levelParams type value (.regular 0)
+    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 `_to_dual_cast
+    addDecl name (← castKind.mkRel lhs body) (← castKind.mkProof lhs)
+
+    let dualLhs ← applyReplacementFun data lhs
+    let dualBody ← applyReplacementFun data body
+    let dualType ← castKind.mkRel dualLhs dualBody
+    -- Make the goal easier to prove by unfolding the dual lhs
+    let dualType' ← castKind.mkRel ((← unfoldDefinition? dualLhs).getD dualLhs) dualBody
+    let dualValue ← elabTermEnsuringType stx dualType' <* synthesizeSyntheticMVarsNoPostponing
+    let dualName ← mkAuxDeclName
+    addDecl dualName dualType (← instantiateMVars dualValue)
+
+    _ ← addTranslationAttr data name { tgt := dualName, existing := true, ref := .missing }
+    return (name, dualName)
 
 elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
-  let declName ← Command.liftCoreM do realizeGlobalConstNoOverloadWithInfo declName
-  withDeclNameForAuxNaming declName do
-  let name ← mkAuxDeclName `_to_dual_insert_cast
-  Command.liftTermElabM do
-    mkSimpleEqThm declName name true fun lhs body => return (← mkEq lhs body, ← mkEqRefl lhs)
-  let dualName ← mkAuxDeclName `_to_dual_insert_cast
-  Command.liftTermElabM do
-    unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true }
-    let cinfo ← getConstInfo name
-    let dualType ← applyReplacementFun data cinfo.type
-    let value ← forallTelescope dualType fun xs dualTypeBody => do
-      -- Make the goal easier to prove by unfolding the lhs of the equality, if possible
-      let dualTypeBody' ← (do
-        if let mkApp2 eq lhs body := dualTypeBody then
-          if let some lhs ← unfoldDefinition? lhs then
-            return mkApp2 eq lhs body
-        return dualTypeBody)
-      let value ← elabTermEnsuringType valStx dualTypeBody'
-      synthesizeSyntheticMVarsNoPostponing
-      mkLambdaFVars xs (← instantiateMVars value)
-    addDecl <| ← mkThmOrUnsafeDef {
-      name := dualName, type := dualType, value
-      levelParams := cinfo.levelParams }
-  elabCommand <| ← `(command|
-    attribute [to_dual existing $(mkIdent name):ident] $(mkIdent dualName))
+  let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
+  let (name, _) ← elabInsertCast declName .eq valStx
+  unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true }
 
 elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command => do
-  let declName ← Command.liftCoreM do realizeGlobalConstNoOverloadWithInfo declName
-  withDeclNameForAuxNaming declName do
-  let name₁ ← mkAuxDeclName `_to_dual_insert_cast_fun
-  Command.liftTermElabM do mkSimpleEqThm declName name₁ false fun lhs body =>
-      return (.forallE `this lhs body .default, .lam `this lhs (.bvar 0) .default)
-  let dualName₁ ← mkAuxDeclName `_to_dual_insert_cast_fun
-  Command.liftTermElabM do
-    let cinfo₁ ← getConstInfo name₁
-    let dualType₁ ← applyReplacementFun data cinfo₁.type
-    let value ← forallTelescope dualType₁ fun xs dualTypeBody => do
-      let value ← elabTermEnsuringType valStx₁ dualTypeBody
-      synthesizeSyntheticMVarsNoPostponing
-      mkLambdaFVars xs (← instantiateMVars value)
-    addDecl <| .defnDecl <|
-      ← mkDefinitionValInferringUnsafe dualName₁ cinfo₁.levelParams dualType₁ value (.regular 0)
-  elabCommand <| ← `(command|
-    attribute [to_dual existing $(mkIdent name₁):ident] $(mkIdent dualName₁))
-  insertionFuns.add name₁ ()
-  insertionFuns.add dualName₁ ()
-
-  let name₂ ← mkAuxDeclName `_to_dual_insert_cast_invFun
+  let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
+  let (name₁, dualName₁) ← elabInsertCast declName .unfoldFun valStx₁
+  let (name₂, dualName₂) ← elabInsertCast declName .refoldFun valStx₂
   casts.add declName (name₁, name₂)
-  Command.liftTermElabM do
-    mkSimpleEqThm declName name₂ false fun lhs body =>
-      return (.forallE `this body lhs .default, .lam `this lhs (.bvar 0) .default)
-  let dualName₂ ← mkAuxDeclName `_to_dual_insert_cast_invFun
-  Command.liftTermElabM do
-    let cinfo₂ ← getConstInfo name₂
-    let dualType₂ ← applyReplacementFun data cinfo₂.type
-    let value ← forallTelescope dualType₂ fun xs dualTypeBody => do
-      let value ← elabTermEnsuringType valStx₂ dualTypeBody
-      synthesizeSyntheticMVarsNoPostponing
-      mkLambdaFVars xs (← instantiateMVars value)
-    addDecl <| .defnDecl <|
-      ← mkDefinitionValInferringUnsafe dualName₂ cinfo₂.levelParams dualType₂ value (.regular 0)
-  elabCommand <| ← `(command|
-    attribute [to_dual existing $(mkIdent name₂):ident] $(mkIdent dualName₂))
-  insertionFuns.add name₂ ()
-  insertionFuns.add dualName₂ ()
+  insertionFuns.add name₁ (); insertionFuns.add dualName₁ ()
+  insertionFuns.add name₂ (); insertionFuns.add dualName₂ ()
 
 end Mathlib.Tactic.ToDual
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index e16d8ca3958321..ab218aada33218 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -42,15 +42,15 @@ structure UnfoldBoundaries where
   /-- The functions that we want to unfold again after the translation has happened. -/
   insertionFuns : NameMap Unit
 
-/-- Modify the `MetaM` context to not allow unfolding the constants for which we would like
-to insert explicit casts. -/
-def withBlockUnfolding {α} (b : UnfoldBoundaries) (x : MetaM α) : MetaM α := do
-  withCanUnfoldPred (fun _ cinfo =>
-    return !b.unfolds.contains cinfo.name
-      && !b.casts.contains cinfo.name) x
-
+/--
+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 fro `b.unfolds`.
+-/
 def run {α} (b : UnfoldBoundaries) (x : SimpM α) : MetaM α :=
-  withBlockUnfolding b do withTransparency TransparencyMode.all do
+  withCanUnfoldPred (fun _ i => return !b.unfolds.contains i.name && !b.casts.contains i.name) do
+  withTransparency TransparencyMode.all do
   let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
   x (Simp.Methods.toMethodsRef { pre }) ctx |>.run' {}
 where
@@ -102,11 +102,11 @@ where
       if ← isDefEq (← goal.getType) (← inferType e) then
         goal.assign e
       else
-        throwError "Failed to insert casts to make {e} have type {← goal.getType}."
+        throwError "{e} : {← inferType e} does not have type {← goal.getType}."
 
 /-- Given an expression `e` with expected type `type`, if `e` doesn't have that type,
 use a cast to turn `e` into that type. -/
-def mkAppWithCast (f a : Expr) (b : UnfoldBoundaries) : SimpM Expr :=
+def mkAppWithCast (b : UnfoldBoundaries) (f a : Expr) : SimpM Expr :=
   try
     checkApp f a
     return f.app a
@@ -117,7 +117,7 @@ def mkAppWithCast (f a : Expr) (b : UnfoldBoundaries) : SimpM Expr :=
     let a ← refoldConsts b a d
     return f.app a
 
-def mkCast (e expectedType : Expr) (b : UnfoldBoundaries) : SimpM Expr := do
+def mkCast (b : UnfoldBoundaries) (e expectedType : Expr) : SimpM Expr := do
   if ← isDefEq (← inferType e) expectedType then
     return e
   let e ← unfoldConsts b e
@@ -146,27 +146,30 @@ def UnfoldBoundaryExt.toUnfoldBoundaries (b : UnfoldBoundaryExt) :
     insertionFuns := b.insertionFuns.getState env }
 
 /-- Modify `e` so that it has type `expectedType`. -/
-public def UnfoldBoundaryExt.cast (e expectedType : Expr) (b : UnfoldBoundaryExt) : MetaM Expr := do
+public def UnfoldBoundaryExt.cast (b : UnfoldBoundaryExt) (e expectedType : Expr) (attr : Name) :
+    MetaM Expr := do
   let b ← b.toUnfoldBoundaries
-  run b do
-    mkCast e expectedType b
+  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 (e : Expr) (b : UnfoldBoundaryExt) : MetaM Expr := do
+public def UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Expr) (attr : Name) :
+    MetaM Expr := do
   let b ← b.toUnfoldBoundaries
-  run b do
-    transform e (post := fun e ↦ e.withApp fun f args => do
-      let mut f := f
-      for arg in args do
-        try
-          f ← mkAppWithCast f arg b
-        catch e =>
-          throwError "failed to deal with {f} applied to {arg}\n{e.toMessageData}"
-      return .done f)
+  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 insertedy as unfold boundaries. -/
 public def UnfoldBoundaryExt.unfoldInsertions (e : Expr) (b : UnfoldBoundaryExt) : CoreM Expr := do

From e910c905975807246ecef5f6006396935abc7213 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 01:48:22 +0100
Subject: [PATCH 13/26] withExporting

---
 Mathlib/Tactic/Translate/ToDual.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index d3cc985c087793..862f98b2fd2677 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -230,7 +230,7 @@ private def CastKind.mkProof (lhs : Expr) : CastKind → MetaM Expr
 
 private def elabInsertCast (declName : Name) (castKind : CastKind) (stx : Term) :
     CommandElabM (Name × Name) :=
-  Command.liftTermElabM do withDeclNameForAuxNaming declName do
+  Command.liftTermElabM do withDeclNameForAuxNaming declName do withExporting do
   let .defnInfo info ← getConstInfo declName | throwError "`{declName}` is not a definition"
   lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let addDecl name type value : MetaM Unit := do
@@ -251,7 +251,7 @@ private def elabInsertCast (declName : Name) (castKind : CastKind) (stx : Term)
     -- Make the goal easier to prove by unfolding the dual lhs
     let dualType' ← castKind.mkRel ((← unfoldDefinition? dualLhs).getD dualLhs) dualBody
     let dualValue ← elabTermEnsuringType stx dualType' <* synthesizeSyntheticMVarsNoPostponing
-    let dualName ← mkAuxDeclName
+    let dualName ← mkAuxDeclName `_to_dual_cast
     addDecl dualName dualType (← instantiateMVars dualValue)
 
     _ ← addTranslationAttr data name { tgt := dualName, existing := true, ref := .missing }

From e31116b3910db5010a742b1c923ac0f2321f6974 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 02:01:23 +0100
Subject: [PATCH 14/26] add tracing

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index ab218aada33218..b448c6ccd3ff19 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -66,6 +66,7 @@ partial def unfoldConsts (b : UnfoldBoundaries) (e : Expr) : SimpM Expr := do
   let e ← do
     let r ← Simp.simp eType
     if let some pf := r.proof? then
+      trace[translate_detail] "unfoldConsts: added a cast from {eType} to {r.expr}"
       mkAppOptM ``cast #[eType, r.expr, pf, e]
     else
       pure e
@@ -73,6 +74,7 @@ partial def unfoldConsts (b : UnfoldBoundaries) (e : Expr) : SimpM Expr := do
   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
 
@@ -86,14 +88,17 @@ where
   go (e : Expr) (goal : MVarId) : SimpM Unit := do
     let goal ← do
       let r ← Simp.simp (← goal.getType)
-      match r.proof? with
-      | some proof => goal.replaceTargetEq r.expr proof
-      | none => pure goal
+      if let some proof := r.proof? then
+        trace[translate_detail] "refoldConsts: added a cast from {← goal.getType} to {r.expr}"
+        goal.replaceTargetEq r.expr proof
+      else
+        pure goal
     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 s!"{cast} is not of the right form"
           let goal' ← mkFreshExprMVar α
           go (mkAppN e xs) goal'.mvarId!

From 1baf799d6fe9daacb32142f1ec0ad788c24077f9 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 02:59:43 +0100
Subject: [PATCH 15/26] doc-string

---
 Mathlib/Tactic/Translate/Core.lean   | 15 +++++++--------
 Mathlib/Tactic/Translate/ToDual.lean | 28 ++++++++++++++++++++++++----
 2 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index a85da7ddd5d7c4..800d99d52b2d28 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -180,7 +180,7 @@ structure TranslateData : Type where
   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
+  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
@@ -536,17 +536,17 @@ def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
     decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
   if let some value := decl.value? (allowOpaque := true) then
     let mut value := value
-    if let some b := t.unfoldBoundaries then
+    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
+    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
+  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
+  if let some b := t.unfoldBoundaries? then
     type ← b.unfoldInsertions type
   return decl.updateType type
 
@@ -867,7 +867,7 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
     throwError "`{t.attrName}` validation failed:\n  expected {srcDecl.levelParams.length} \
       universe levels, but '{tgt}' has {tgtDecl.levelParams.length} universe levels"
   let mut srcType := srcDecl.type
-  if let some b := t.unfoldBoundaries then
+  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
@@ -886,9 +886,8 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
     else
       pure reorder'
   srcType ← reorderForall reorder srcType
-  if let some b := t.unfoldBoundaries then
+  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
diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index 862f98b2fd2677..a46b76436cec5e 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -109,8 +109,8 @@ initialize casts : NameMapExtension (Name × Name) ← registerNameMapExtension
 @[inherit_doc UnfoldBoundaryExt.insertionFuns]
 initialize insertionFuns : NameMapExtension Unit ← registerNameMapExtension _
 
-@[inherit_doc TranslateData.unfoldBoundaries]
-def unfoldBoundaries : UnfoldBoundaryExt := { unfolds, casts, insertionFuns }
+@[inherit_doc TranslateData.unfoldBoundaries?]
+def unfoldBoundaries? : Option UnfoldBoundaryExt := some { unfolds, casts, insertionFuns }
 
 @[inherit_doc TranslateData.argInfoAttr]
 initialize argInfoAttr : NameMapExtension ArgInfo ← registerNameMapExtension _
@@ -202,7 +202,7 @@ def abbreviationDict : Std.HashMap String String := .ofList [
 
 /-- The bundle of environment extensions for `to_dual` -/
 def data : TranslateData where
-  ignoreArgsAttr; argInfoAttr; doTranslateAttr; unfoldBoundaries; translations
+  ignoreArgsAttr; argInfoAttr; doTranslateAttr; unfoldBoundaries?; translations
   attrName := `to_dual
   changeNumeral := false
   isDual := true
@@ -254,14 +254,34 @@ private def elabInsertCast (declName : Name) (castKind : CastKind) (stx : Term)
     let dualName ← mkAuxDeclName `_to_dual_cast
     addDecl dualName dualType (← instantiateMVars dualValue)
 
-    _ ← addTranslationAttr data name { tgt := dualName, existing := true, ref := .missing }
+    let relevantArg? := (argInfoAttr.find? (← getEnv) declName).map (·.relevantArg)
+    _ ← addTranslationAttr data name
+      { tgt := dualName, existing := true, ref := .missing, relevantArg? }
     return (name, dualName)
 
+/-- The `to_dual_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.
+If type checking a term requires the definition `foo` to be unfolded, then before translating
+that term, a `cast` is 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. -/
 elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
   let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
   let (name, _) ← elabInsertCast declName .eq valStx
   unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true }
 
+/-- The `to_dual_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 a duals of these.
+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. At the end, the remaining unfold/refold functions are unfolded. -/
 elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command => do
   let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
   let (name₁, dualName₁) ← elabInsertCast declName .unfoldFun valStx₁

From a70ee1a29f25bd3ab32a90218dd86df553476588 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 11:25:03 +0100
Subject: [PATCH 16/26] add tests

---
 MathlibTest/ToDual.lean | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean
index a0382c9c8f1bc7..a49083b7818b04 100644
--- a/MathlibTest/ToDual.lean
+++ b/MathlibTest/ToDual.lean
@@ -109,3 +109,41 @@ theorem not_lt_self {α : Type} [PartialOrder α] (a : α) : ¬ a < a := lt_irre
 -- Test that we do not translate numerals like we do in `@[to_additive]`
 @[to_dual self]
 theorem one_le_one {α : Type} [One α] [Preorder α] : (1 : α) ≤ 1 := le_rfl
+
+/-! Test the `to_dual_insert_cast` framework. -/
+
+section
+variable {α : Type} [PartialOrder α]
+
+@[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)
+
+-- 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
+
+end

From 9f1f93936b9c68712c0a5bbb65265290ff1e870c Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 11:43:50 +0100
Subject: [PATCH 17/26] apply to `IsThin`

---
 Mathlib/Combinatorics/Quiver/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
 

From e1da64ab57aaecb2dafad2e12a21b54e147c0454 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Sat, 20 Dec 2025 14:01:53 +0100
Subject: [PATCH 18/26] add more tests

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean |  2 +-
 MathlibTest/ToDual.lean                      | 41 ++++++++++++++++++++
 2 files changed, 42 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index b448c6ccd3ff19..14d9e3887dbcf1 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -101,7 +101,7 @@ where
           trace[translate_detail] "refoldConsts: created the cast {cast} to unfold {.ofConstName c}"
           let .forallE _ α _ _ ← inferType cast | throwError s!"{cast} is not of the right form"
           let goal' ← mkFreshExprMVar α
-          go (mkAppN e xs) goal'.mvarId!
+          go (e.beta xs) goal'.mvarId!
           goal.assign <| ← mkLambdaFVars xs <| .app cast goal'
           return
       if ← isDefEq (← goal.getType) (← inferType e) then
diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean
index a49083b7818b04..3add7707aaf92e 100644
--- a/MathlibTest/ToDual.lean
+++ b/MathlibTest/ToDual.lean
@@ -120,6 +120,47 @@ 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 α := h
+
+@[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) := id h
+
+-- 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 => id fun 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 ⋯

From cb0a6a7be5235f520677d6ef46fc979782fde42f Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Mon, 22 Dec 2025 01:10:26 +0100
Subject: [PATCH 19/26] clean up documentation

---
 Mathlib/Tactic/Translate/ToDual.lean         | 20 ++++--
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 69 +++++++++-----------
 2 files changed, 45 insertions(+), 44 deletions(-)

diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index a46b76436cec5e..5e285ab95117e4 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -82,7 +82,17 @@ 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
 ```
- -/
+
+Some definitions are dual to something other than the dual of their value. Examples include
+- `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.
+-/
 syntax (name := to_dual) "to_dual" "?"? attrArgs : attr
 
 @[inherit_doc to_dual]
@@ -264,8 +274,8 @@ 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.
-If type checking a term requires the definition `foo` to be unfolded, then before translating
-that term, a `cast` is inserted into the term using this unfolding 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. -/
 elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
@@ -277,11 +287,11 @@ elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
 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 a duals of these.
+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. At the end, the remaining unfold/refold functions are unfolded. -/
+can be safely translated. After translating, the unfold/refold functions are again unfolded. -/
 elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command => do
   let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
   let (name₁, dualName₁) ← elabInsertCast declName .unfoldFun valStx₁
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 14d9e3887dbcf1..6a2979c69038ee 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -18,13 +18,13 @@ 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, using `isDefEq`, and whenever
-there is a type mismatch, we try to insert a cast.
+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 folding. This is for Types, where we
+- Explicit casting functions, both for unfolding and folding. This is for types, where we
   cannot express their equivalence with an equality. For example `DecidableLE`.
 -/
 
@@ -46,11 +46,11 @@ structure UnfoldBoundaries where
 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 fro `b.unfolds`.
+- 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 TransparencyMode.all do
+  withTransparency .all do
   let ctx ← Simp.mkContext { Simp.neutralConfig with implicitDefEqProofs := false }
   x (Simp.Methods.toMethodsRef { pre }) ctx |>.run' {}
 where
@@ -64,12 +64,9 @@ where
 partial def unfoldConsts (b : UnfoldBoundaries) (e : Expr) : SimpM Expr := do
   let eType ← inferType e
   let e ← do
-    let r ← Simp.simp eType
-    if let some pf := r.proof? then
-      trace[translate_detail] "unfoldConsts: added a cast from {eType} to {r.expr}"
-      mkAppOptM ``cast #[eType, r.expr, pf, e]
-    else
-      pure e
+    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
@@ -87,30 +84,33 @@ partial def refoldConsts (b : UnfoldBoundaries) (e expectedType : Expr) : SimpM
 where
   go (e : Expr) (goal : MVarId) : SimpM Unit := do
     let goal ← do
-      let r ← Simp.simp (← goal.getType)
-      if let some proof := r.proof? then
-        trace[translate_detail] "refoldConsts: added a cast from {← goal.getType} to {r.expr}"
-        goal.replaceTargetEq r.expr proof
-      else
-        pure goal
+      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 s!"{cast} is not of the right form"
+          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
-      if ← isDefEq (← goal.getType) (← inferType e) then
-        goal.assign e
-      else
+      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 `type`, if `e` doesn't have that type,
+/-- 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
@@ -118,39 +118,30 @@ def mkAppWithCast (b : UnfoldBoundaries) (f a : Expr) : SimpM Expr :=
   catch _ =>
     let f ← unfoldConsts b f
     let .forallE _ d _ _ ← whnf (← inferType f) | throwFunctionExpected f
-    let a ← unfoldConsts b a
-    let a ← refoldConsts b a d
-    return f.app a
-
-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
+    return f.app (← mkCast b a d)
 
 /-- Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded. -/
 public structure UnfoldBoundaryExt where
-  /-- The `cast` attribute is used to tag declarations `foo` that should not be unfolded in
+  /-- 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 then may be translated by the translation attribute. -/
+  This equality theorem can then be translated by the translation attribute. -/
   unfolds : NameMapExtension SimpTheorem
-  /-- The `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
+  /-- 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
+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`. -/
+/-- 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
@@ -176,7 +167,7 @@ public def UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Expr)
       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 insertedy as unfold boundaries. -/
+/-- 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
   Meta.deltaExpand e b.insertionFuns.contains

From 739fc74ea950fdaa15940a7e477a8e094bf4b8ce Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Tue, 23 Dec 2025 01:45:53 +0100
Subject: [PATCH 20/26] show that is also works for `GaloisConnection`

---
 Mathlib/Order/GaloisConnection/Defs.lean | 66 +++++++-----------------
 Mathlib/Tactic/Translate/ToDual.lean     |  2 +
 2 files changed, 21 insertions(+), 47 deletions(-)

diff --git a/Mathlib/Order/GaloisConnection/Defs.lean b/Mathlib/Order/GaloisConnection/Defs.lean
index 750d6b935e2f4f..df9d72a583749f 100644
--- a/Mathlib/Order/GaloisConnection/Defs.lean
+++ b/Mathlib/Order/GaloisConnection/Defs.lean
@@ -39,19 +39,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) :=
@@ -60,36 +65,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
@@ -97,20 +95,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
@@ -120,60 +123,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/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean
index 5e285ab95117e4..692cd0d17ac0d1 100644
--- a/Mathlib/Tactic/Translate/ToDual.lean
+++ b/Mathlib/Tactic/Translate/ToDual.lean
@@ -165,6 +165,8 @@ def nameDict : Std.HashMap String (List String) := .ofList [
   ("ioi", ["Iio"]),
   ("ici", ["Iic"]),
   ("iic", ["Ici"]),
+  ("u", ["L"]),
+  ("l", ["U"]),
 
   ("epi", ["Mono"]),
   /- `mono` can also refer to monotone, so we don't translate it. -/

From c440be2fd56385eba219d5eb02a3b7221fb36bb8 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Tue, 23 Dec 2025 17:42:15 +0100
Subject: [PATCH 21/26] refactor(translate): merge `expand` into 
 `applyReplacementFun`

---
 Mathlib/Tactic/Translate/Core.lean | 167 ++++++++++++++++-------------
 MathlibTest/toAdditive.lean        |   6 --
 2 files changed, 95 insertions(+), 78 deletions(-)

diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index 800d99d52b2d28..f3dcaabf1db33c 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -281,45 +281,12 @@ structure Config : Type where
 -- See https://github.com/leanprover/lean4/issues/10295
 attribute [nolint unusedArguments] instReprConfig.repr
 
-/-- Eta expands `e` at most `n` times. -/
+/-- Eta expands `e` exactly `n` times. -/
 def etaExpandN (n : Nat) (e : Expr) : MetaM Expr := do
-  forallBoundedTelescope (← inferType e) (some n) fun xs _ ↦ mkLambdaFVars xs (mkAppN e xs)
-
-/-- `e.expand` eta-expands all expressions that have as head a constant `n` in `reorder`.
-They are expanded until they are applied to one more argument than the maximum in `reorder.find n`.
-It also expands all kernel projections that have as head a constant `n` in `reorder`. -/
-def expand (t : TranslateData) (e : Expr) : MetaM Expr := do
-  let env ← getEnv
-  let e₂ ← Meta.transform e (skipConstInApp := true) fun e ↦
-    e.withApp fun f args ↦ do
-    match f with
-    | .proj n i s =>
-      let some info := getStructureInfo? (← getEnv) n | return .continue -- e.g. if `n` is `Exists`
-      let some projName := info.getProjFn? i | unreachable!
-      -- if `projName` has a translation, replace `f` with the application `projName s`
-      -- and then visit `projName s args` again.
-      if findTranslation? env t projName |>.isNone then
-        return .continue
-      return .visit <| (← whnfD (← inferType s)).withApp fun sf sargs ↦
-        mkAppN (mkApp (mkAppN (.const projName sf.constLevels!) sargs) s) args
-    | .const c _ =>
-      let some info := t.argInfoAttr.find? env c | return .continue
-      if info.reorder.isEmpty then
-        -- no need to expand if nothing needs reordering
-        return .continue
-      let needed_n := info.reorder.flatten.foldl Nat.max 0 + 1
-      if needed_n ≤ args.size then
-        return .continue
-      else
-        -- in this case, we need to reorder arguments that are not yet
-        -- applied, so first η-expand the function.
-        let e' ← etaExpandN (needed_n - args.size) e
-        trace[translate_detail] "expanded {e} to {e'}"
-        return .continue e'
-    | _ => return .continue
-  if e != e₂ then
-    trace[translate_detail] "expand:\nBefore: {e}\nAfter: {e₂}"
-  return e₂
+  forallBoundedTelescope (← inferType e) (some n) fun xs _ ↦ do
+    if xs.size ≠ n then
+      throwError "{e} is not a function of arity at least {n}"
+    mkLambdaFVars xs (mkAppN e xs)
 
 /-- Implementation function for `shouldTranslate`.
 Failure means that in that subexpression there is no constant that blocks `e` from being translated.
@@ -395,24 +362,67 @@ is tested, instead of the first argument.
 It will also reorder arguments of certain functions, using `reorderFn`:
 e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorderFn g = some [1]`.
 -/
-def applyReplacementFun (t : TranslateData) (e : Expr) (dontTranslate : Array FVarId := #[]) :
-    MetaM Expr := do
-  let e' := aux (← getEnv) (← getBoolOption `trace.translate_detail) (← expand t e)
-  -- Make sure any new reserved names in the expr are realized; this needs to be done outside of
-  -- `aux` as it is monadic.
+partial def applyReplacementFun (t : TranslateData) (e : Expr)
+    (dontTranslate : Array FVarId := #[]) : MetaM Expr := do
+  let e' ← visit e |>.run {}
+  -- Make sure any new reserved names in the expr are realized
   e'.getUsedConstants.forM fun n => do
     if !(← hasConst (skipRealize := false) n) && isReservedName (← getEnv) n then
       executeReservedNameAction n
   return e'
-where /-- Implementation of `applyReplacementFun`. -/
-  aux (env : Environment) (trace : Bool) : Expr → Expr :=
-  memoFix fun r e ↦ Id.run do
-    if trace then
-      dbg_trace s!"replacing at {e}"
-    if !(e matches .const .. | .app ..) then
-      e.traverseChildren r
-    else e.withApp fun f args ↦ do
-      let .const n₀ ls₀ := f | return mkAppN (← r f) (← args.mapM r)
+where
+  -- In `visitLambda`, `visitForall` and `visitLet`, we use a fresh `lctx` to store
+  -- the translated types of the new free variables.
+  visitLambda (fvars : Array Expr) (lctx : LocalContext) :
+      Expr → MonadCacheT ExprStructEq Expr MetaM Expr
+    | .lam n d b c =>
+      withLocalDecl n c (d.instantiateRev fvars) fun x => do
+        let decl ← getFVarLocalDecl x
+        let decl := decl.setType (← visit decl.type)
+        visitLambda (fvars.push x) (lctx.addDecl decl) b
+    | e => do
+      let e ← visit (e.instantiateRev fvars); withLCtx lctx {} do mkLambdaFVars fvars e
+  visitForall (fvars : Array Expr) (lctx : LocalContext) :
+      Expr → MonadCacheT ExprStructEq Expr MetaM Expr
+    | .forallE n d b c =>
+      withLocalDecl n c (d.instantiateRev fvars) fun x => do
+        let decl ← getFVarLocalDecl x
+        let decl := decl.setType (← visit decl.type)
+        visitForall (fvars.push x) (lctx.addDecl decl) b
+    | e => do
+      let e ← visit (e.instantiateRev fvars); withLCtx lctx {} do mkForallFVars fvars e
+  visitLet (fvars : Array Expr) (lctx : LocalContext) :
+      Expr → MonadCacheT ExprStructEq Expr MetaM Expr
+    | .letE n t v b nondep =>
+      withLetDecl n (t.instantiateRev fvars) (v.instantiateRev fvars) (nondep := nondep)
+        fun x => do
+        let decl ← getFVarLocalDecl x
+        let decl := decl.setType (← visit decl.type) |>.setValue (← visit (decl.value true))
+        visitLet (fvars.push x) (lctx.addDecl decl) b
+    | e => do
+      let e ← visit (e.instantiateRev fvars)
+      withLCtx lctx {} do mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) fvars e
+  /-- The implementation of this function is based on `Meta.transform`.
+  We can't use `Meta.transform`, because that would cause the types of free variables to be
+  translated, which would create type-incorrect terms. Instead, we give the free variables
+  their original type and the translated type is only used when constructing the final term. -/
+  visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr :=
+  checkCache { val := e : ExprStructEq } fun _ => do
+  let visitApp := e.withApp fun f args ↦ do
+    let env ← getEnv
+    match f with
+    | .proj n i b =>
+      let some info := getStructureInfo? env n |
+        return mkAppN (f.updateProj! (← visit b)) (← args.mapM visit) -- e.g. if `n` is `Exists`
+      let some projName := info.getProjFn? i | unreachable!
+      -- if `projName` has a translation, replace `f` with the application `projName s`
+      -- and then visit `projName s args` again.
+      if findTranslation? env t projName |>.isNone then
+        return mkAppN (f.updateProj! (← visit b)) (← args.mapM visit)
+      visit <| (← whnfD (← inferType b)).withApp fun bf bargs ↦
+        mkAppN (.app (mkAppN (.const projName bf.constLevels!) bargs) b) args
+    | .const n₀ ls₀ =>
+      withTraceNode `translate_detail (fun res => return m!"{exceptEmoji res} replacing at {e}") do
       -- Replace numeral `1` with `0` when required
       if t.changeNumeral then
         if let some numeralArgs := changeNumeralAttr.find? env n₀ then
@@ -421,35 +431,48 @@ where /-- Implementation of `applyReplacementFun`. -/
               -- In this case, we still update all arguments of `g` that are not numerals,
               -- since all other arguments can contain subexpressions like
               -- `(fun x ↦ ℕ) (1 : G)`, and we have to update the `(1 : G)` to `(0 : G)`
-              if trace then
-                dbg_trace s!"applyReplacementFun: We change the numerals in this expression. \
-                  However, we will still recurse into all the non-numeral arguments."
+              trace[translate_detail] "applyReplacementFun: We change the numerals in this \
+                  expression. However, we will still recurse into all the non-numeral arguments."
               let args := numeralArgs.foldl (·.modify · changeNumeral) args
-              return mkAppN f (← args.mapM r)
+              return mkAppN f (← args.mapM visit)
       let some n₁ := findTranslation? env t n₀ <|> do
         let n₁ := findPrefixTranslation env n₀ t; guard (n₀ != n₁); some n₁
-        | return mkAppN f (← args.mapM r)
+        | return mkAppN f (← args.mapM visit)
       let { reorder, relevantArg } := t.argInfoAttr.find? env n₀ |>.getD {}
       -- Use `relevantArg` to test if the head should be translated.
       if h : relevantArg < args.size then
-        if let some fxd := shouldTranslate env t args[relevantArg] dontTranslate then
-          if trace then
-            match fxd with
-            | .inl fxd => dbg_trace s!"The application of {n₀} contains the fixed type \
-              {fxd}, so it is not changed."
-            | .inr _ => dbg_trace s!"The application of {n₀} contains a fixed \
-              variable so it is not changed."
-          return mkAppN f (← args.mapM r)
+        if let some fx := shouldTranslate env t args[relevantArg] dontTranslate then
+          let fx := match fx with | .inl fx => m!"type {fx}" | .inr fx => m!"variable {mkFVar fx}"
+          trace[translate_detail]
+            "The application of {n₀} contains the fixed {fx} so it is not changed."
+          return mkAppN f (← args.mapM visit)
+      -- If the number of arguments is too small for `reorder`, we need to eta expand first
+      unless reorder.isEmpty do
+        let reorderNumArgs := reorder.flatten.foldl Nat.max 0 + 1
+        if reorderNumArgs > args.size then
+          let e' ← etaExpandN (reorderNumArgs - args.size) e
+          trace[translate_detail] "eta expanded {e} to {e'}"
+          return ← visit e'
       let swapUniv := reorder.any (·.contains 0)
       let ls₁ := if swapUniv then ls₀.swapFirstTwo else ls₀
       let args := args.permute! reorder
-      if trace then
-        dbg_trace s!"changing {n₀} to {n₁}"
-        if swapUniv then
-          dbg_trace s!"reordering the universe variables from {ls₀} to {ls₁}"
-        unless reorder.isEmpty do
-          dbg_trace s!"reordering the arguments of {n₀} using the cyclic permutations {reorder}"
-      return mkAppN (.const n₁ ls₁) (← args.mapM r)
+      trace[translate_detail]"changing {n₀} to {n₁}"
+      if swapUniv then
+        trace[translate_detail] "reordering the universe variables from {ls₀} to {ls₁}"
+      unless reorder.isEmpty do
+        trace[translate_detail]
+          "reordering the arguments of {n₀} using the cyclic permutations {reorder}"
+      return mkAppN (.const n₁ ls₁) (← args.mapM visit)
+    | _ => return mkAppN (← visit f) (← args.mapM visit)
+  match e with
+  | .forallE ..    => visitForall #[] {} e
+  | .lam ..        => visitLambda #[] {} e
+  | .letE ..       => visitLet #[] {} e
+  | .mdata _ b     => return e.updateMData! (← visit b)
+  | .proj _ _ b    => visitApp
+  | .app ..        => visitApp
+  | .const ..      => visitApp
+  | _              => return e
 
 /-- Rename binder names in pi type. -/
 def renameBinderNames (t : TranslateData) (src : Expr) : Expr :=
diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean
index f7ac6720ffc2af..3a052cd499e4f9 100644
--- a/MathlibTest/toAdditive.lean
+++ b/MathlibTest/toAdditive.lean
@@ -172,13 +172,7 @@ run_meta do
   guard <| (← getReducibilityStatus `Test.bar22.match_1) != .reducible
   guard <| (Compiler.getInlineAttribute? (← getEnv) `Test.bar22.match_1) == some .inline
 
-/- test the eta-expansion applied on `foo6`. -/
 run_cmd do
-  let c ← getConstInfo `Test.foo6
-  let e : Expr ← liftCoreM <| MetaM.run' <| expand ToAdditive.data c.value!
-  let t ← liftCoreM <| MetaM.run' <| expand ToAdditive.data c.type
-  let decl := c |>.updateName `Test.barr6 |>.updateType t |>.updateValue e |>.toDeclaration!
-  liftCoreM <| addAndCompile decl
   -- test that we cannot transport a declaration to itself
   successIfFail <| liftCoreM <| addTranslationAttr ToAdditive.data `bar11_works { ref := ← getRef }
 

From 193aee40f78ad09eaf29668d52d933559227b3fc Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Tue, 23 Dec 2025 17:42:46 +0100
Subject: [PATCH 22/26] Revert "refactor(translate): merge `expand` into 
 `applyReplacementFun`"

This reverts commit c440be2fd56385eba219d5eb02a3b7221fb36bb8.
---
 Mathlib/Tactic/Translate/Core.lean | 167 +++++++++++++----------------
 MathlibTest/toAdditive.lean        |   6 ++
 2 files changed, 78 insertions(+), 95 deletions(-)

diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index f3dcaabf1db33c..800d99d52b2d28 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -281,12 +281,45 @@ structure Config : Type where
 -- See https://github.com/leanprover/lean4/issues/10295
 attribute [nolint unusedArguments] instReprConfig.repr
 
-/-- Eta expands `e` exactly `n` times. -/
+/-- Eta expands `e` at most `n` times. -/
 def etaExpandN (n : Nat) (e : Expr) : MetaM Expr := do
-  forallBoundedTelescope (← inferType e) (some n) fun xs _ ↦ do
-    if xs.size ≠ n then
-      throwError "{e} is not a function of arity at least {n}"
-    mkLambdaFVars xs (mkAppN e xs)
+  forallBoundedTelescope (← inferType e) (some n) fun xs _ ↦ mkLambdaFVars xs (mkAppN e xs)
+
+/-- `e.expand` eta-expands all expressions that have as head a constant `n` in `reorder`.
+They are expanded until they are applied to one more argument than the maximum in `reorder.find n`.
+It also expands all kernel projections that have as head a constant `n` in `reorder`. -/
+def expand (t : TranslateData) (e : Expr) : MetaM Expr := do
+  let env ← getEnv
+  let e₂ ← Meta.transform e (skipConstInApp := true) fun e ↦
+    e.withApp fun f args ↦ do
+    match f with
+    | .proj n i s =>
+      let some info := getStructureInfo? (← getEnv) n | return .continue -- e.g. if `n` is `Exists`
+      let some projName := info.getProjFn? i | unreachable!
+      -- if `projName` has a translation, replace `f` with the application `projName s`
+      -- and then visit `projName s args` again.
+      if findTranslation? env t projName |>.isNone then
+        return .continue
+      return .visit <| (← whnfD (← inferType s)).withApp fun sf sargs ↦
+        mkAppN (mkApp (mkAppN (.const projName sf.constLevels!) sargs) s) args
+    | .const c _ =>
+      let some info := t.argInfoAttr.find? env c | return .continue
+      if info.reorder.isEmpty then
+        -- no need to expand if nothing needs reordering
+        return .continue
+      let needed_n := info.reorder.flatten.foldl Nat.max 0 + 1
+      if needed_n ≤ args.size then
+        return .continue
+      else
+        -- in this case, we need to reorder arguments that are not yet
+        -- applied, so first η-expand the function.
+        let e' ← etaExpandN (needed_n - args.size) e
+        trace[translate_detail] "expanded {e} to {e'}"
+        return .continue e'
+    | _ => return .continue
+  if e != e₂ then
+    trace[translate_detail] "expand:\nBefore: {e}\nAfter: {e₂}"
+  return e₂
 
 /-- Implementation function for `shouldTranslate`.
 Failure means that in that subexpression there is no constant that blocks `e` from being translated.
@@ -362,67 +395,24 @@ is tested, instead of the first argument.
 It will also reorder arguments of certain functions, using `reorderFn`:
 e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorderFn g = some [1]`.
 -/
-partial def applyReplacementFun (t : TranslateData) (e : Expr)
-    (dontTranslate : Array FVarId := #[]) : MetaM Expr := do
-  let e' ← visit e |>.run {}
-  -- Make sure any new reserved names in the expr are realized
+def applyReplacementFun (t : TranslateData) (e : Expr) (dontTranslate : Array FVarId := #[]) :
+    MetaM Expr := do
+  let e' := aux (← getEnv) (← getBoolOption `trace.translate_detail) (← expand t e)
+  -- Make sure any new reserved names in the expr are realized; this needs to be done outside of
+  -- `aux` as it is monadic.
   e'.getUsedConstants.forM fun n => do
     if !(← hasConst (skipRealize := false) n) && isReservedName (← getEnv) n then
       executeReservedNameAction n
   return e'
-where
-  -- In `visitLambda`, `visitForall` and `visitLet`, we use a fresh `lctx` to store
-  -- the translated types of the new free variables.
-  visitLambda (fvars : Array Expr) (lctx : LocalContext) :
-      Expr → MonadCacheT ExprStructEq Expr MetaM Expr
-    | .lam n d b c =>
-      withLocalDecl n c (d.instantiateRev fvars) fun x => do
-        let decl ← getFVarLocalDecl x
-        let decl := decl.setType (← visit decl.type)
-        visitLambda (fvars.push x) (lctx.addDecl decl) b
-    | e => do
-      let e ← visit (e.instantiateRev fvars); withLCtx lctx {} do mkLambdaFVars fvars e
-  visitForall (fvars : Array Expr) (lctx : LocalContext) :
-      Expr → MonadCacheT ExprStructEq Expr MetaM Expr
-    | .forallE n d b c =>
-      withLocalDecl n c (d.instantiateRev fvars) fun x => do
-        let decl ← getFVarLocalDecl x
-        let decl := decl.setType (← visit decl.type)
-        visitForall (fvars.push x) (lctx.addDecl decl) b
-    | e => do
-      let e ← visit (e.instantiateRev fvars); withLCtx lctx {} do mkForallFVars fvars e
-  visitLet (fvars : Array Expr) (lctx : LocalContext) :
-      Expr → MonadCacheT ExprStructEq Expr MetaM Expr
-    | .letE n t v b nondep =>
-      withLetDecl n (t.instantiateRev fvars) (v.instantiateRev fvars) (nondep := nondep)
-        fun x => do
-        let decl ← getFVarLocalDecl x
-        let decl := decl.setType (← visit decl.type) |>.setValue (← visit (decl.value true))
-        visitLet (fvars.push x) (lctx.addDecl decl) b
-    | e => do
-      let e ← visit (e.instantiateRev fvars)
-      withLCtx lctx {} do mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) fvars e
-  /-- The implementation of this function is based on `Meta.transform`.
-  We can't use `Meta.transform`, because that would cause the types of free variables to be
-  translated, which would create type-incorrect terms. Instead, we give the free variables
-  their original type and the translated type is only used when constructing the final term. -/
-  visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr :=
-  checkCache { val := e : ExprStructEq } fun _ => do
-  let visitApp := e.withApp fun f args ↦ do
-    let env ← getEnv
-    match f with
-    | .proj n i b =>
-      let some info := getStructureInfo? env n |
-        return mkAppN (f.updateProj! (← visit b)) (← args.mapM visit) -- e.g. if `n` is `Exists`
-      let some projName := info.getProjFn? i | unreachable!
-      -- if `projName` has a translation, replace `f` with the application `projName s`
-      -- and then visit `projName s args` again.
-      if findTranslation? env t projName |>.isNone then
-        return mkAppN (f.updateProj! (← visit b)) (← args.mapM visit)
-      visit <| (← whnfD (← inferType b)).withApp fun bf bargs ↦
-        mkAppN (.app (mkAppN (.const projName bf.constLevels!) bargs) b) args
-    | .const n₀ ls₀ =>
-      withTraceNode `translate_detail (fun res => return m!"{exceptEmoji res} replacing at {e}") do
+where /-- Implementation of `applyReplacementFun`. -/
+  aux (env : Environment) (trace : Bool) : Expr → Expr :=
+  memoFix fun r e ↦ Id.run do
+    if trace then
+      dbg_trace s!"replacing at {e}"
+    if !(e matches .const .. | .app ..) then
+      e.traverseChildren r
+    else e.withApp fun f args ↦ do
+      let .const n₀ ls₀ := f | return mkAppN (← r f) (← args.mapM r)
       -- Replace numeral `1` with `0` when required
       if t.changeNumeral then
         if let some numeralArgs := changeNumeralAttr.find? env n₀ then
@@ -431,48 +421,35 @@ where
               -- In this case, we still update all arguments of `g` that are not numerals,
               -- since all other arguments can contain subexpressions like
               -- `(fun x ↦ ℕ) (1 : G)`, and we have to update the `(1 : G)` to `(0 : G)`
-              trace[translate_detail] "applyReplacementFun: We change the numerals in this \
-                  expression. However, we will still recurse into all the non-numeral arguments."
+              if trace then
+                dbg_trace s!"applyReplacementFun: We change the numerals in this expression. \
+                  However, we will still recurse into all the non-numeral arguments."
               let args := numeralArgs.foldl (·.modify · changeNumeral) args
-              return mkAppN f (← args.mapM visit)
+              return mkAppN f (← args.mapM r)
       let some n₁ := findTranslation? env t n₀ <|> do
         let n₁ := findPrefixTranslation env n₀ t; guard (n₀ != n₁); some n₁
-        | return mkAppN f (← args.mapM visit)
+        | return mkAppN f (← args.mapM r)
       let { reorder, relevantArg } := t.argInfoAttr.find? env n₀ |>.getD {}
       -- Use `relevantArg` to test if the head should be translated.
       if h : relevantArg < args.size then
-        if let some fx := shouldTranslate env t args[relevantArg] dontTranslate then
-          let fx := match fx with | .inl fx => m!"type {fx}" | .inr fx => m!"variable {mkFVar fx}"
-          trace[translate_detail]
-            "The application of {n₀} contains the fixed {fx} so it is not changed."
-          return mkAppN f (← args.mapM visit)
-      -- If the number of arguments is too small for `reorder`, we need to eta expand first
-      unless reorder.isEmpty do
-        let reorderNumArgs := reorder.flatten.foldl Nat.max 0 + 1
-        if reorderNumArgs > args.size then
-          let e' ← etaExpandN (reorderNumArgs - args.size) e
-          trace[translate_detail] "eta expanded {e} to {e'}"
-          return ← visit e'
+        if let some fxd := shouldTranslate env t args[relevantArg] dontTranslate then
+          if trace then
+            match fxd with
+            | .inl fxd => dbg_trace s!"The application of {n₀} contains the fixed type \
+              {fxd}, so it is not changed."
+            | .inr _ => dbg_trace s!"The application of {n₀} contains a fixed \
+              variable so it is not changed."
+          return mkAppN f (← args.mapM r)
       let swapUniv := reorder.any (·.contains 0)
       let ls₁ := if swapUniv then ls₀.swapFirstTwo else ls₀
       let args := args.permute! reorder
-      trace[translate_detail]"changing {n₀} to {n₁}"
-      if swapUniv then
-        trace[translate_detail] "reordering the universe variables from {ls₀} to {ls₁}"
-      unless reorder.isEmpty do
-        trace[translate_detail]
-          "reordering the arguments of {n₀} using the cyclic permutations {reorder}"
-      return mkAppN (.const n₁ ls₁) (← args.mapM visit)
-    | _ => return mkAppN (← visit f) (← args.mapM visit)
-  match e with
-  | .forallE ..    => visitForall #[] {} e
-  | .lam ..        => visitLambda #[] {} e
-  | .letE ..       => visitLet #[] {} e
-  | .mdata _ b     => return e.updateMData! (← visit b)
-  | .proj _ _ b    => visitApp
-  | .app ..        => visitApp
-  | .const ..      => visitApp
-  | _              => return e
+      if trace then
+        dbg_trace s!"changing {n₀} to {n₁}"
+        if swapUniv then
+          dbg_trace s!"reordering the universe variables from {ls₀} to {ls₁}"
+        unless reorder.isEmpty do
+          dbg_trace s!"reordering the arguments of {n₀} using the cyclic permutations {reorder}"
+      return mkAppN (.const n₁ ls₁) (← args.mapM r)
 
 /-- Rename binder names in pi type. -/
 def renameBinderNames (t : TranslateData) (src : Expr) : Expr :=
diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean
index 3a052cd499e4f9..f7ac6720ffc2af 100644
--- a/MathlibTest/toAdditive.lean
+++ b/MathlibTest/toAdditive.lean
@@ -172,7 +172,13 @@ run_meta do
   guard <| (← getReducibilityStatus `Test.bar22.match_1) != .reducible
   guard <| (Compiler.getInlineAttribute? (← getEnv) `Test.bar22.match_1) == some .inline
 
+/- test the eta-expansion applied on `foo6`. -/
 run_cmd do
+  let c ← getConstInfo `Test.foo6
+  let e : Expr ← liftCoreM <| MetaM.run' <| expand ToAdditive.data c.value!
+  let t ← liftCoreM <| MetaM.run' <| expand ToAdditive.data c.type
+  let decl := c |>.updateName `Test.barr6 |>.updateType t |>.updateValue e |>.toDeclaration!
+  liftCoreM <| addAndCompile decl
   -- test that we cannot transport a declaration to itself
   successIfFail <| liftCoreM <| addTranslationAttr ToAdditive.data `bar11_works { ref := ← getRef }
 

From df64221c060eba1c82f119935bacbca6b63714c9 Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Date: Fri, 26 Dec 2025 11:23:23 +0200
Subject: [PATCH 23/26] fix beta reduction problem?

---
 Mathlib/Tactic/Translate/UnfoldBoundary.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index 6a2979c69038ee..b7571184529a4d 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -170,6 +170,10 @@ public def UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Expr)
 /-- 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
-  Meta.deltaExpand e b.insertionFuns.contains
+  -- This is the same as Meta.deltaExpand, but with an extra beta reduction.
+  Core.transform e fun e => do
+    match ← delta? e b.insertionFuns.contains with
+    | some e' => return .visit e'.headBeta
+    | none    => return .continue
 
 end Mathlib.Tactic.UnfoldBoundary

From 4014a6babb029a3fc479043c2feb054f2cc4a9cd Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Date: Fri, 26 Dec 2025 19:32:48 +0200
Subject: [PATCH 24/26] fix decidable instances

---
 Mathlib/Order/WithBot.lean | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
index bd19391c38ac21..d959048906cff2 100644
--- a/Mathlib/Order/WithBot.lean
+++ b/Mathlib/Order/WithBot.lean
@@ -681,18 +681,30 @@ instance _root_.WithTop.distribLattice [DistribLattice α] : DistribLattice (Wit
 instance decidableEq [DecidableEq α] : DecidableEq (WithBot α) :=
   inferInstanceAs <| DecidableEq (Option α)
 
-@[to_dual]
+-- `to_dual` is not happy to translate the equational theorems of these decidable instances,
+-- so we define the duals separately.
 instance decidableLE [LE α] [DecidableLE α] : DecidableLE (WithBot α)
   | ⊥, _ => isTrue <| by simp
   | (a : α), ⊥ => isFalse <| by simp
   | (a : α), (b : α) => decidable_of_iff' _ coe_le_coe
 
-@[to_dual]
 instance decidableLT [LT α] [DecidableLT α] : DecidableLT (WithBot α)
   | _, ⊥ => isFalse <| by simp
   | ⊥, (a : α) => isTrue <| by simp
   | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe
 
+@[to_dual existing]
+instance _root_.WithTop.decidableLE [LE α] [DecidableLE α] : DecidableLE (WithTop α)
+  | _, ⊤ => isTrue <| by simp
+  | ⊤, (a : α) => isFalse <| by simp
+  | (a : α), (b : α) => decidable_of_iff' _ coe_le_coe
+
+@[to_dual existing]
+instance _root_.WithTop.decidableLT [LT α] [DecidableLT α] : DecidableLT (WithTop α)
+  | ⊤, _ => isFalse <| by simp
+  | (a : α), ⊤ => isTrue <| by simp
+  | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe
+
 instance isTotal_le [LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithBot α) (· ≤ ·) where
   total x y := by cases x <;> cases y <;> simp; simpa using IsTotal.total ..
 

From 221a8a7a8855587263e0f1ce648924a504423a7d Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Wed, 14 Jan 2026 16:07:23 +0000
Subject: [PATCH 25/26] .

---
 Mathlib/Tactic/Translate/Core.lean | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index 998b3a80a99ad0..a80063a23288be 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -555,14 +555,13 @@ 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
-  if let some value := decl.value? (allowOpaque := true) then
-    let mut value := value
-    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 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

From e9532f851ca23ccc0596c311f7794ba9358ab60d Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Date: Fri, 16 Jan 2026 13:40:02 +0000
Subject: [PATCH 26/26] clean up

---
 Mathlib/Order/WithBot.lean                    |  16 +--
 .../Tactic/Translate/TagUnfoldBoundary.lean   | 104 ++++++++++++++++++
 Mathlib/Tactic/Translate/ToDual.lean          |  84 ++------------
 Mathlib/Tactic/Translate/UnfoldBoundary.lean  |  22 ++--
 MathlibTest/ToDual.lean                       |   6 +-
 5 files changed, 132 insertions(+), 100 deletions(-)
 create mode 100644 Mathlib/Tactic/Translate/TagUnfoldBoundary.lean

diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
index bfb37935d59f1a..24fa9859d3161d 100644
--- a/Mathlib/Order/WithBot.lean
+++ b/Mathlib/Order/WithBot.lean
@@ -728,30 +728,18 @@ instance _root_.WithTop.distribLattice [DistribLattice α] : DistribLattice (Wit
 instance decidableEq [DecidableEq α] : DecidableEq (WithBot α) :=
   inferInstanceAs <| DecidableEq (Option α)
 
--- `to_dual` is not happy to translate the equational theorems of these decidable instances,
--- so we define the duals separately.
+@[to_dual]
 instance decidableLE [LE α] [DecidableLE α] : DecidableLE (WithBot α)
   | ⊥, _ => isTrue <| by simp
   | (a : α), ⊥ => isFalse <| by simp
   | (a : α), (b : α) => decidable_of_iff' _ coe_le_coe
 
+@[to_dual]
 instance decidableLT [LT α] [DecidableLT α] : DecidableLT (WithBot α)
   | _, ⊥ => isFalse <| by simp
   | ⊥, (a : α) => isTrue <| by simp
   | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe
 
-@[to_dual existing]
-instance _root_.WithTop.decidableLE [LE α] [DecidableLE α] : DecidableLE (WithTop α)
-  | _, ⊤ => isTrue <| by simp
-  | ⊤, (a : α) => isFalse <| by simp
-  | (a : α), (b : α) => decidable_of_iff' _ coe_le_coe
-
-@[to_dual existing]
-instance _root_.WithTop.decidableLT [LT α] [DecidableLT α] : DecidableLT (WithTop α)
-  | ⊤, _ => isFalse <| by simp
-  | (a : α), ⊤ => isTrue <| by simp
-  | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe
-
 instance isTotal_le [LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithBot α) (· ≤ ·) where
   total x y := by cases x <;> cases y <;> simp; simpa using IsTotal.total ..
 
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 52c9d64eebc2e2..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.
@@ -227,6 +227,14 @@ def data : TranslateData where
   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"
@@ -235,78 +243,4 @@ initialize registerBuiltinAttribute {
     applicationTime := .afterCompilation
   }
 
-private inductive CastKind where
-| eq | unfoldFun | refoldFun
-
-private 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
-
-private def CastKind.mkProof (lhs : Expr) : CastKind → MetaM Expr
-  | .eq => mkEqRefl lhs
-  | _ => return .lam `_ lhs (.bvar 0) .default
-
-private def elabInsertCast (declName : Name) (castKind : CastKind) (stx : Term) :
-    CommandElabM (Name × Name) :=
-  Command.liftTermElabM do withDeclNameForAuxNaming declName do withExporting do
-  let .defnInfo info ← getConstInfo declName | throwError "`{declName}` is not a definition"
-  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 `_to_dual_cast
-    addDecl name (← castKind.mkRel lhs body) (← castKind.mkProof lhs)
-
-    let dualLhs ← applyReplacementFun data lhs
-    let dualBody ← applyReplacementFun data body
-    let dualType ← castKind.mkRel dualLhs dualBody
-    -- Make the goal easier to prove by unfolding the dual lhs
-    let dualType' ← castKind.mkRel ((← unfoldDefinition? dualLhs).getD dualLhs) dualBody
-    let dualValue ← elabTermEnsuringType stx dualType' <* synthesizeSyntheticMVarsNoPostponing
-    let dualName ← mkAuxDeclName `_to_dual_cast
-    addDecl dualName dualType (← instantiateMVars dualValue)
-
-    let relevantArg? := (argInfoAttr.find? (← getEnv) declName).map (·.relevantArg)
-    _ ← addTranslationAttr data name
-      { tgt := dualName, existing := true, ref := .missing, relevantArg? }
-    return (name, dualName)
-
-/-- The `to_dual_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. -/
-elab "to_dual_insert_cast" declName:ident " := " valStx:term : command => do
-  let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
-  let (name, _) ← elabInsertCast declName .eq valStx
-  unfolds.add declName { origin := .decl name, proof := mkConst name, rfl := true }
-
-/-- The `to_dual_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. -/
-elab "to_dual_insert_cast_fun" declName:ident " := " valStx₁:term ", " valStx₂:term : command => do
-  let declName ← Command.liftCoreM <| realizeGlobalConstNoOverloadWithInfo declName
-  let (name₁, dualName₁) ← elabInsertCast declName .unfoldFun valStx₁
-  let (name₂, dualName₂) ← elabInsertCast declName .refoldFun valStx₂
-  casts.add declName (name₁, name₂)
-  insertionFuns.add name₁ (); insertionFuns.add dualName₁ ()
-  insertionFuns.add name₂ (); insertionFuns.add dualName₂ ()
-
 end Mathlib.Tactic.ToDual
diff --git a/Mathlib/Tactic/Translate/UnfoldBoundary.lean b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
index b7571184529a4d..4b0166fbfdaebd 100644
--- a/Mathlib/Tactic/Translate/UnfoldBoundary.lean
+++ b/Mathlib/Tactic/Translate/UnfoldBoundary.lean
@@ -6,7 +6,7 @@ Authors: Jovan Gerbscheid
 module
 
 public meta import Lean.Meta.Tactic.Delta
-public meta import Batteries.Lean.NameMapAttribute
+public import Batteries.Lean.NameMapAttribute
 public import Mathlib.Init
 
 /-!
@@ -24,7 +24,7 @@ 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 folding. This is for types, where we
+- Explicit casting functions, both for unfolding and refolding. This is for types, where we
   cannot express their equivalence with an equality. For example `DecidableLE`.
 -/
 
@@ -155,8 +155,8 @@ public def UnfoldBoundaryExt.cast (b : UnfoldBoundaryExt) (e expectedType : Expr
 /-- 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. -/
+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
@@ -170,10 +170,16 @@ public def UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Expr)
 /-- 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.
+  -- This is the same as `Meta.deltaExpand`, but with an extra beta reduction.
   Core.transform e fun e => do
-    match ← delta? e b.insertionFuns.contains with
-    | some e' => return .visit e'.headBeta
-    | none    => return .continue
+    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 847a85915b3725..8a4ed219e84f79 100644
--- a/MathlibTest/ToDual.lean
+++ b/MathlibTest/ToDual.lean
@@ -151,7 +151,7 @@ def lt_sum_eq_of_le [DecidableLE α] {a b : α} (hab : 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 α := h
+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
@@ -174,7 +174,7 @@ fun {α} [PartialOrder α] h =>
 def DecidableLE3 (h : DecidableLE α) : ∀ a b : α, Decidable (a ≤ b) := h
 
 @[to_dual DecidableLE4_dual]
-def DecidableLE4 (h : DecidableLE α) : ∀ a b : α, Decidable (a ≤ b) := id h
+def DecidableLE4 (h : DecidableLE α) (a b : α) : Decidable (a ≤ b) := h a b
 
 -- The arguments to `h` have been introduced, and swapped:
 /--
@@ -182,7 +182,7 @@ info: fun {α} [PartialOrder α] h a b => h b a
 ---
 info: fun {α} [PartialOrder α] h => id fun 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