From 54175f3b995cc6792d7de71c7a66f5fa209daa60 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 23 Oct 2025 22:54:32 +0200
Subject: [PATCH] fix: decreasing_by: remove mdata (#10931)

This PR strips the `Expr.mdata` that `WF.Fix` uses to associate goal
with recursive calls from the goal presented to the tactics.
Fixes #10895.
---
 src/Lean/Elab/PreDefinition/WF/Fix.lean |  2 ++
 tests/lean/run/issue10895.lean          | 16 ++++++++++++++++
 tests/lean/run/wfrecUnary.lean          |  1 -
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/issue10895.lean

diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 203cb3551f..e1813edbcc 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -221,8 +221,10 @@ def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decr
           let type ← goal.getType
           let some ref := getRecAppSyntax? (← goal.getType)
             | throwError "MVar not annotated as a recursive call:{indentExpr type}"
+          goal.setType type.mdataExpr!
           withRef ref <| applyDefaultDecrTactic goal
       | some decrTactic => withRef decrTactic.ref do
+        goals.forM fun goal => do goal.setType (← goal.getType).mdataExpr!
         unless goals.isEmpty do -- unlikely to be empty
           -- make info from `runTactic` available
           goals.forM fun goal => pushInfoTree (.hole goal)
diff --git a/tests/lean/run/issue10895.lean b/tests/lean/run/issue10895.lean
new file mode 100644
index 0000000000..bef0a954d7
--- /dev/null
+++ b/tests/lean/run/issue10895.lean
@@ -0,0 +1,16 @@
+axiom T : Type
+axiom T.lt : T → T → Prop
+axiom T.wf_lt : WellFounded T.lt
+axiom T.f : T → T
+instance : WellFoundedRelation T := ⟨_, T.wf_lt⟩
+axiom T.lt_f x : (T.f x).lt x
+
+set_option pp.raw true
+
+#guard_msgs in
+noncomputable def foo (t : T) : Unit :=
+  foo (T.f t)
+termination_by t
+decreasing_by
+  have := T.lt_f t
+  grind
diff --git a/tests/lean/run/wfrecUnary.lean b/tests/lean/run/wfrecUnary.lean
index 5f7e403db1..f857771074 100644
--- a/tests/lean/run/wfrecUnary.lean
+++ b/tests/lean/run/wfrecUnary.lean
@@ -4,5 +4,4 @@ def f (n : Nat) : Nat :=
   else
     2 * f (n-1)
 decreasing_by
-  simp [measure, id, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.pred_lt h