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

@@ -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)

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

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