From c4f2d64d013d265acd9ebc139ede9c20882c64b2 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 24 Jul 2026 16:17:22 +0200
Subject: [PATCH 1/9] change something

---
 foo | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 foo

diff --git a/foo b/foo
new file mode 100644
index 000000000000..e69de29bb2d1

From 2306c35d7935b33b18e178dc9f47739170807d0f Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 24 Jul 2026 15:19:57 +0000
Subject: [PATCH 2/9] fix error message for rfl

---
 src/Lean/Meta/Basic.lean                  |  6 +++++-
 src/Lean/Meta/Check.lean                  |  3 ++-
 src/Lean/Meta/Tactic/Rfl.lean             |  3 ++-
 tests/elab/addPPExplicitToExposeDiff.lean | 18 ++++++++++++++++++
 4 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index e207f8f137bd..515ea9f625c7 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2830,7 +2830,11 @@ Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic
 The optional array of expressions is used to set the `hasSyntheticSorry` fields, and should
 comprise the expressions that are included in the message data.
 -/
-def MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
+def MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[])
+    (config? : Option Meta.Config := none) : MessageData :=
+  let f := match config? with
+    | some config => withConfig (fun _ => config) f
+    | none => f
   .lazy
     (f := fun ppctxt => do
       match (← ppctxt.runMetaM f |>.toBaseIO) with
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 3796de18422b..76b746c97aa8 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -224,7 +224,8 @@ function. Any expressions appearing in the trailing message should be included i
 def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
     (trailing? : Option MessageData := none) (trailingExprs : Array Expr := #[])
     : MetaM MessageData := do
-  return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs) do
+  return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs)
+      (config? := some (← getConfig)) do
     let mut msg ← (try
       let givenTypeType ← inferType givenType
       let expectedTypeType ← inferType expectedType
diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 3204c5a627e7..78069f04d0b5 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -85,7 +85,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
 
   let success ← approxDefEq <| isDefEqGuarded lhs rhs
   unless success do
-    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+    let explanation := MessageData.ofLazyM (es := #[lhs, rhs])
+        (config? := some (← approxDefEq getConfig)) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
       return m!"The left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
     throwTacticEx `rfl goal explanation
diff --git a/tests/elab/addPPExplicitToExposeDiff.lean b/tests/elab/addPPExplicitToExposeDiff.lean
index 6288f3d1b031..ebb063dd3252 100644
--- a/tests/elab/addPPExplicitToExposeDiff.lean
+++ b/tests/elab/addPPExplicitToExposeDiff.lean
@@ -64,6 +64,24 @@ but is expected to have type
 example : @f 1 2 := by
   exact (sorry : @f 0 _)
 
+def myId {x : Nat} : Nat := x
+def one : Nat := 1
+
+/-!
+TODO: comment
+-/
+/--
+error: Type mismatch
+  sorry
+has type
+  @f (@myId 1) 2
+but is expected to have type
+  @f (@myId one) 2
+-/
+#guard_msgs in
+example : @f (myId (x := one)) 2 := by
+  with_implicit exact (sorry : @f (myId (x := 1)) 2)
+
 /-!
 Add type ascriptions for numerals if they have different types.
 -/

From f573febbb220285987c395c659f73ee3c6f063dc Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 24 Jul 2026 15:37:39 +0000
Subject: [PATCH 3/9] change, rewrite, #check_tactic

---
 src/Lean/Elab/CheckTactic.lean               |  2 +-
 src/Lean/Elab/Tactic/Change.lean             |  2 +-
 src/Lean/Meta/Tactic/Rewrite.lean            |  3 +-
 tests/elab/addPPExplicitToExposeDiff.lean    | 53 ++++++++++++++++++++
 tests/elab/implicitReducibleFunctorComp.lean |  4 +-
 tests/elab/typeCheckNote.lean                |  4 +-
 6 files changed, 61 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/CheckTactic.lean b/src/Lean/Elab/CheckTactic.lean
index 0ed4849ab7ea..fea65066ca51 100644
--- a/src/Lean/Elab/CheckTactic.lean
+++ b/src/Lean/Elab/CheckTactic.lean
@@ -42,7 +42,7 @@ def elabCheckTactic : CommandElab := fun stx => do
       | [next] => do
         let (val, _, _) ← matchCheckGoalType stx (←next.getType)
         if !(← Meta.withReducible <| isDefEq val expTerm) then
-          let (val, expTerm) ← addPPExplicitToExposeDiff val expTerm
+          let (val, expTerm) ← Meta.withReducible <| addPPExplicitToExposeDiff val expTerm
           throwErrorAt stx
             m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
       | _ => do
diff --git a/src/Lean/Elab/Tactic/Change.lean b/src/Lean/Elab/Tactic/Change.lean
index 07722437f8c3..8fb385c2237c 100644
--- a/src/Lean/Elab/Tactic/Change.lean
+++ b/src/Lean/Elab/Tactic/Change.lean
@@ -42,7 +42,7 @@ def elabChange (e : Expr) (p : Term) (mkDefeqError : Expr → Expr → MetaM Mes
     pure p
   withAssignableSyntheticOpaque do
     unless ← isDefEq p e do
-      throwError MessageData.ofLazyM (es := #[p, e]) do
+      throwError MessageData.ofLazyM (es := #[p, e]) (config? := some (← getConfig)) do
         let (p, tgt) ← addPPExplicitToExposeDiff p e
         mkDefeqError p tgt
     instantiateMVars p
diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index f616c869ab7d..81baa42dc449 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -46,7 +46,8 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let e ← instantiateMVars e
           let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs config.occs
           unless eAbst.hasLooseBVars do
-            let (tgt, pat) ← addPPExplicitToExposeDiff e lhs
+            let (tgt, pat) ← withConfig (fun oldConfig => { config, oldConfig with }) <|
+              addPPExplicitToExposeDiff e lhs
             throwTacticEx `rewrite mvarId m!"Did not find an occurrence of the pattern{indentExpr pat}\nin the target expression{indentExpr tgt}"
           -- construct rewrite proof
           let eNew := eAbst.instantiate1 rhs
diff --git a/tests/elab/addPPExplicitToExposeDiff.lean b/tests/elab/addPPExplicitToExposeDiff.lean
index ebb063dd3252..27739c26c84b 100644
--- a/tests/elab/addPPExplicitToExposeDiff.lean
+++ b/tests/elab/addPPExplicitToExposeDiff.lean
@@ -180,3 +180,56 @@ but is expected to have type
 #guard_msgs in example (p : Nat → Prop) (d1 d2 : DecidablePred p) :
     {x : Nat // @decide _ (d1 x) = true} :=
   (sorry : {x : Nat // @decide _ (d2 x) = true})
+
+/-!
+`change` diagnoses at the transparency of the failed check.
+-/
+/--
+error: 'change' tactic failed, pattern
+  @f (@myId 1) 2
+is not definitionally equal to target
+  @f (@myId one) 2
+-/
+#guard_msgs in
+example : @f (myId (x := one)) 2 := by
+  with_reducible change @f (myId (x := 1)) 2
+
+/-!
+`#check_tactic` diagnoses at the reducible transparency of its check.
+-/
+/--
+error: Term reduces to
+  @myId one
+but is expected to reduce to ⏎
+  @myId 1
+-/
+#guard_msgs in
+#check_tactic (myId (x := one)) ~> myId (x := 1) by skip
+
+/-!
+`#check_tactic` diagnoses at the reducible transparency of its check.
+-/
+/--
+error: Term reduces to
+  @f (@myId one) 2
+but is expected to reduce to ⏎
+  @f (@myId 1) 2
+-/
+#guard_msgs in
+#check_tactic @f (myId (x := one)) 2 ~> @f (myId (x := 1)) 2 by skip
+
+/-!
+`rewrite` diagnoses at the transparency `kabstract` matched at.
+-/
+/--
+error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
+  @f (@myId 1) 2
+in the target expression
+  @f (@myId one) 2
+
+h : f 2 = True
+⊢ f 2
+-/
+#guard_msgs in
+example (h : @f (@myId 1) 2 = True) : @f (myId (x := one)) 2 := by
+  rewrite [h]
diff --git a/tests/elab/implicitReducibleFunctorComp.lean b/tests/elab/implicitReducibleFunctorComp.lean
index 32fd04880cf3..f48ecbb26b9a 100644
--- a/tests/elab/implicitReducibleFunctorComp.lean
+++ b/tests/elab/implicitReducibleFunctorComp.lean
@@ -145,9 +145,9 @@ Full error:
   Application type mismatch: The argument
     G.map (F.map f)
   has type
-    @Quiver.Hom E inst✝.toQuiver (G.obj (F.obj X)) (G.obj (F.obj Y))
+    G.obj (F.obj X) ⟶ G.obj (F.obj Y)
   but is expected to have type
-    @Quiver.Hom E inst✝.toQuiver ((F ⋙ G).obj X) ((F ⋙ G).obj Y)
+    (F ⋙ G).obj X ⟶ (F ⋙ G).obj Y
   in the application
     Category.comp (G.map (F.map f))
 -/
diff --git a/tests/elab/typeCheckNote.lean b/tests/elab/typeCheckNote.lean
index 6bacfd18cc52..2f9a9b21076d 100644
--- a/tests/elab/typeCheckNote.lean
+++ b/tests/elab/typeCheckNote.lean
@@ -97,9 +97,9 @@ Full error:
   Application type mismatch: The argument
     h2
   has type
-    @LT.lt Nat instLTNat idx (composed s a b).s.decls.size
+    idx < (composed s a b).s.decls.size
   but is expected to have type
-    @LT.lt Nat instLTNat idx
+    idx <
       (have res := myF s { x := a };
             myF res.s { x := b }).s.decls.size
   in the application

From b4f70737d64889a657d4290ea00bd3ce9a3dc650 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 24 Jul 2026 15:50:24 +0000
Subject: [PATCH 4/9] apply

---
 src/Lean/Meta/Tactic/Apply.lean           |  7 ++++---
 tests/elab/addPPExplicitToExposeDiff.lean | 16 ++++++++++++++++
 tests/elab/rflTacticErrors.lean           |  4 ++--
 3 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 0b1ce93f4b13..f905ccdebde0 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -28,8 +28,9 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do
 
 private def throwApplyError {α} (mvarId : MVarId)
     (eType : Expr) (conclusionType? : Option Expr) (targetType : Expr)
-    (term? : Option MessageData) : MetaM α := do
-  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) do
+    (term? : Option MessageData) (approx : Bool) : MetaM α := do
+  let config ← if approx then approxDefEq getConfig else getConfig
+  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) (config? := some config) do
     let conclusionType := conclusionType?.getD eType
     let note := if conclusionType?.isSome then .note m!"The full type of {term?.getD "the term"} is{indentExpr eType}" else m!""
     let (conclusionType, targetType) ← addPPExplicitToExposeDiff conclusionType targetType
@@ -215,7 +216,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
         else
           let (_, _, r) ← forallMetaTelescopeReducing eType (some rangeNumArgs.lower)
           pure (some r)
-        throwApplyError mvarId eType conclusionType? targetType term?
+        throwApplyError mvarId eType conclusionType? targetType term? cfg.approx
       termination_by rangeNumArgs.upper - i
     let (newMVars, binderInfos) ← go rangeNumArgs.lower
     postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures
diff --git a/tests/elab/addPPExplicitToExposeDiff.lean b/tests/elab/addPPExplicitToExposeDiff.lean
index 27739c26c84b..67e9eb37e5e8 100644
--- a/tests/elab/addPPExplicitToExposeDiff.lean
+++ b/tests/elab/addPPExplicitToExposeDiff.lean
@@ -233,3 +233,19 @@ h : f 2 = True
 #guard_msgs in
 example (h : @f (@myId 1) 2 = True) : @f (myId (x := one)) 2 := by
   rewrite [h]
+
+/-!
+`apply` diagnoses at the configuration of the failed check.
+-/
+/--
+error: Tactic `apply` failed: could not unify the type of `h`
+  @f (@myId 1) 2
+with the goal
+  @f (@myId one) 2
+
+h : f 2
+⊢ f 2
+-/
+#guard_msgs in
+example (h : @f (@myId 1) 2) : @f (myId (x := one)) 2 := by
+  with_reducible apply h
diff --git a/tests/elab/rflTacticErrors.lean b/tests/elab/rflTacticErrors.lean
index 90326057031c..acea522df6e5 100644
--- a/tests/elab/rflTacticErrors.lean
+++ b/tests/elab/rflTacticErrors.lean
@@ -238,9 +238,9 @@ example : true'' = true   := by with_reducible apply_rfl -- Error
 
 /--
 error: Tactic `apply` failed: could not unify the conclusion of 'HEq.refl'
-  @HEq ?α ?a ?α ?a
+  ?a ≍ ?a
 with the goal
-  @HEq Bool true'' Bool true
+  true'' ≍ true
 
 Note: The full type of 'HEq.refl' is
   ∀ {α : Sort _} (a : α), a ≍ a

From e90a1bf063e594c829303f7f2b4a2dc47fbb0a97 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 24 Jul 2026 16:09:19 +0000
Subject: [PATCH 5/9] defeqAttrib

---
 src/Lean/DefEqAttrib.lean                  |  6 ++++--
 tests/elab/addPPExplicitToExposeDiff.lean  | 19 +++++++++++++++++++
 tests/elab/linterTacticCheckInstances.lean |  8 ++++----
 3 files changed, 27 insertions(+), 6 deletions(-)

diff --git a/src/Lean/DefEqAttrib.lean b/src/Lean/DefEqAttrib.lean
index 571240a56563..fed0fc1b3afc 100644
--- a/src/Lean/DefEqAttrib.lean
+++ b/src/Lean/DefEqAttrib.lean
@@ -54,8 +54,10 @@ def validateDefEqAttr (declName : Name) : AttrM Unit := do
   MetaM.run' do withEqLhsRhs info.type fun lhs rhs => do
     let ok ← isDefEqCareful lhs rhs
     unless ok do
-      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
-        let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) (config? := some (← getConfig)) do
+        -- match the `smartUnfolding` setting of `isDefEqCareful`
+        let (lhs, rhs) ← withOptions (smartUnfolding.set · false) <|
+          addPPExplicitToExposeDiff lhs rhs
         let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \
           not definitionally equal to the right-hand side{indentExpr rhs}"
         if (← getEnv).isExporting then
diff --git a/tests/elab/addPPExplicitToExposeDiff.lean b/tests/elab/addPPExplicitToExposeDiff.lean
index 67e9eb37e5e8..a0666bf98ddd 100644
--- a/tests/elab/addPPExplicitToExposeDiff.lean
+++ b/tests/elab/addPPExplicitToExposeDiff.lean
@@ -249,3 +249,22 @@ h : f 2
 #guard_msgs in
 example (h : @f (@myId 1) 2) : @f (myId (x := one)) 2 := by
   with_reducible apply h
+
+/-!
+`@[defeq]` diagnoses at the configuration of its defeq check (transparency `.all`), so the
+diff is not attributed to `one'` vs. `1`, which are defeq at that transparency.
+-/
+axiom testSorry : α
+@[irreducible] def one' : Nat := 1
+opaque a : Nat
+opaque b : Nat
+opaque g : {_ : Nat} → Nat → Nat
+
+/--
+error: Not a definitional equality: the left-hand side
+  @g a one'
+is not definitionally equal to the right-hand side
+  @g b 1
+-/
+#guard_msgs in
+@[defeq] theorem gEq : @g a one' = @g b 1 := testSorry
diff --git a/tests/elab/linterTacticCheckInstances.lean b/tests/elab/linterTacticCheckInstances.lean
index 7ce96726dc46..482b10ae2ea2 100644
--- a/tests/elab/linterTacticCheckInstances.lean
+++ b/tests/elab/linterTacticCheckInstances.lean
@@ -35,9 +35,9 @@ Full error:
   Application type mismatch: The argument
     h2
   has type
-    @LT.lt Nat instLTNat idx (composed s a b).s.decls.size
+    idx < (composed s a b).s.decls.size
   but is expected to have type
-    @LT.lt Nat instLTNat idx
+    idx <
       (have res := myF s { x := a };
             myF res.s { x := b }).s.decls.size
   in the application
@@ -62,9 +62,9 @@ Full error:
   Application type mismatch: The argument
     h1
   has type
-    @LT.lt Nat instLTNat idx s.decls.size
+    idx < s.decls.size
   but is expected to have type
-    @LT.lt Nat instLTNat idx (composed s a b).s.decls.size
+    idx < (composed s a b).s.decls.size
   in the application
     (composed s a b).s.decls[idx]
 

From 23784f35cbd5ad22d8ae3aa7eaf6abf6ae65bf83 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 27 Jul 2026 10:27:01 +0000
Subject: [PATCH 6/9] cleanups

---
 foo                                       | 0
 src/Lean/Meta/Basic.lean                  | 1 +
 tests/elab/addPPExplicitToExposeDiff.lean | 4 +++-
 3 files changed, 4 insertions(+), 1 deletion(-)
 delete mode 100644 foo

diff --git a/foo b/foo
deleted file mode 100644
index e69de29bb2d1..000000000000
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 515ea9f625c7..1b7315471894 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2829,6 +2829,7 @@ end PPContext
 Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
 The optional array of expressions is used to set the `hasSyntheticSorry` fields, and should
 comprise the expressions that are included in the message data.
+The optional `Meta.Config` object will be used when executing `f`.
 -/
 def MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[])
     (config? : Option Meta.Config := none) : MessageData :=
diff --git a/tests/elab/addPPExplicitToExposeDiff.lean b/tests/elab/addPPExplicitToExposeDiff.lean
index a0666bf98ddd..58b5bc5babc6 100644
--- a/tests/elab/addPPExplicitToExposeDiff.lean
+++ b/tests/elab/addPPExplicitToExposeDiff.lean
@@ -68,7 +68,9 @@ def myId {x : Nat} : Nat := x
 def one : Nat := 1
 
 /-!
-TODO: comment
+Exposes an implicit argument nested inside an outer implicit argument because
+the out explicit arguments can be unified, but the outer implicit argument
+cannot, and its nested explicit arguments can be unified.
 -/
 /--
 error: Type mismatch

From b56baa6548f51a426a89aaa27151a3c03fb066ba Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 27 Jul 2026 10:31:09 +0000
Subject: [PATCH 7/9] less invasive

---
 src/Lean/DefEqAttrib.lean        | 3 ++-
 src/Lean/Elab/Tactic/Change.lean | 3 ++-
 src/Lean/Meta/Basic.lean         | 7 +------
 src/Lean/Meta/Check.lean         | 5 +++--
 src/Lean/Meta/Tactic/Apply.lean  | 3 ++-
 src/Lean/Meta/Tactic/Rfl.lean    | 4 ++--
 6 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/Lean/DefEqAttrib.lean b/src/Lean/DefEqAttrib.lean
index fed0fc1b3afc..f2778945ce52 100644
--- a/src/Lean/DefEqAttrib.lean
+++ b/src/Lean/DefEqAttrib.lean
@@ -54,7 +54,8 @@ def validateDefEqAttr (declName : Name) : AttrM Unit := do
   MetaM.run' do withEqLhsRhs info.type fun lhs rhs => do
     let ok ← isDefEqCareful lhs rhs
     unless ok do
-      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) (config? := some (← getConfig)) do
+      let config ← getConfig
+      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) <| withConfig (fun _ => config) do
         -- match the `smartUnfolding` setting of `isDefEqCareful`
         let (lhs, rhs) ← withOptions (smartUnfolding.set · false) <|
           addPPExplicitToExposeDiff lhs rhs
diff --git a/src/Lean/Elab/Tactic/Change.lean b/src/Lean/Elab/Tactic/Change.lean
index 8fb385c2237c..bcf1cc68471e 100644
--- a/src/Lean/Elab/Tactic/Change.lean
+++ b/src/Lean/Elab/Tactic/Change.lean
@@ -42,7 +42,8 @@ def elabChange (e : Expr) (p : Term) (mkDefeqError : Expr → Expr → MetaM Mes
     pure p
   withAssignableSyntheticOpaque do
     unless ← isDefEq p e do
-      throwError MessageData.ofLazyM (es := #[p, e]) (config? := some (← getConfig)) do
+      let config ← getConfig
+      throwError MessageData.ofLazyM (es := #[p, e]) <| withConfig (fun _ => config) do
         let (p, tgt) ← addPPExplicitToExposeDiff p e
         mkDefeqError p tgt
     instantiateMVars p
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 1b7315471894..e207f8f137bd 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2829,13 +2829,8 @@ end PPContext
 Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
 The optional array of expressions is used to set the `hasSyntheticSorry` fields, and should
 comprise the expressions that are included in the message data.
-The optional `Meta.Config` object will be used when executing `f`.
 -/
-def MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[])
-    (config? : Option Meta.Config := none) : MessageData :=
-  let f := match config? with
-    | some config => withConfig (fun _ => config) f
-    | none => f
+def MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
   .lazy
     (f := fun ppctxt => do
       match (← ppctxt.runMetaM f |>.toBaseIO) with
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 76b746c97aa8..efc5431e3641 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -224,8 +224,9 @@ function. Any expressions appearing in the trailing message should be included i
 def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
     (trailing? : Option MessageData := none) (trailingExprs : Array Expr := #[])
     : MetaM MessageData := do
-  return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs)
-      (config? := some (← getConfig)) do
+  let config ← getConfig
+  return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs) <|
+      withConfig (fun _ => config) do
     let mut msg ← (try
       let givenTypeType ← inferType givenType
       let expectedTypeType ← inferType expectedType
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index f905ccdebde0..ab9f9ef6ef8f 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -30,7 +30,8 @@ private def throwApplyError {α} (mvarId : MVarId)
     (eType : Expr) (conclusionType? : Option Expr) (targetType : Expr)
     (term? : Option MessageData) (approx : Bool) : MetaM α := do
   let config ← if approx then approxDefEq getConfig else getConfig
-  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) (config? := some config) do
+  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) <|
+      withConfig (fun _ => config) do
     let conclusionType := conclusionType?.getD eType
     let note := if conclusionType?.isSome then .note m!"The full type of {term?.getD "the term"} is{indentExpr eType}" else m!""
     let (conclusionType, targetType) ← addPPExplicitToExposeDiff conclusionType targetType
diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 78069f04d0b5..efef720a1e3a 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -85,8 +85,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
 
   let success ← approxDefEq <| isDefEqGuarded lhs rhs
   unless success do
-    let explanation := MessageData.ofLazyM (es := #[lhs, rhs])
-        (config? := some (← approxDefEq getConfig)) do
+    let config ← approxDefEq getConfig
+    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) <| withConfig (fun _ => config) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
       return m!"The left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
     throwTacticEx `rfl goal explanation

From f74da2e610f132d16a4b0dc70bfc649f2e6ed41c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 27 Jul 2026 10:41:04 +0000
Subject: [PATCH 8/9] clear_value

---
 src/Lean/Elab/Tactic/BuiltinTactic.lean   |  2 +-
 tests/elab/addPPExplicitToExposeDiff.lean | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 5e1a437ad108..21ea2ce5ab5b 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -447,7 +447,7 @@ where
         let e := (← fvarId.getValue?).get!
         let e' ← Tactic.elabTermEnsuringType v (← fvarId.getType)
         unless ← withAssignableSyntheticOpaque <| isDefEq e e' do
-          let (e, e') ← addPPExplicitToExposeDiff e e'
+          let (e, e') ← withAssignableSyntheticOpaque <| addPPExplicitToExposeDiff e e'
           throwErrorAt v "Provided term{indentExpr e'}\n\
             is not definitionally equal to{indentD m!"{Expr.fvar fvarId} := {e}"}"
         let mvars ← filterOldMVars (← getMVars e') mvarCounterSaved
diff --git a/tests/elab/addPPExplicitToExposeDiff.lean b/tests/elab/addPPExplicitToExposeDiff.lean
index 58b5bc5babc6..8a351beaf4a4 100644
--- a/tests/elab/addPPExplicitToExposeDiff.lean
+++ b/tests/elab/addPPExplicitToExposeDiff.lean
@@ -270,3 +270,18 @@ is not definitionally equal to the right-hand side
 -/
 #guard_msgs in
 @[defeq] theorem gEq : @g a one' = @g b 1 := testSorry
+
+/-!
+`clear_value` diagnoses with assignable synthetic opaque metavariables, matching its check, so
+the diff is attributed to `a` vs. `b` rather than to the assignable `?_`.
+-/
+/--
+error: Provided term
+  f ?_ ∧ @f b 2
+is not definitionally equal to
+  x := f 1 ∧ @f a 2
+-/
+#guard_msgs in
+example : True := by
+  let x : Prop := @f 1 1 ∧ @f a 2
+  clear_value (h : x = (@f 1 ?_ ∧ @f b 2))

From 502b6baf3bc0b74ce92f3e63f8fd9207a9c9cfd9 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 27 Jul 2026 13:07:27 +0000
Subject: [PATCH 9/9] don't trace in addPPExplicitToExposeDiff, except in case
 of errors

---
 src/Lean/Meta/Check.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index efc5431e3641..de29fe9cb514 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -78,7 +78,10 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
     -- but we don't want these assignments to leak out of the function.
     -- Note: we shouldn't instantiate mvars in `visit` to prevent leakage.
     withoutModifyingState do
-      visit (← instantiateMVars a) (← instantiateMVars b)
+      let traceState ← getTraceState
+      let r ← visit (← instantiateMVars a) (← instantiateMVars b)
+      setTraceState traceState
+      return r
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try