fix: add message context in delabToRefinableSuggestion

mhuisi · mhuisi · commit f6eadfb1d814 · 2025-10-11T13:05:26.000+02:00
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
@@ -73,7 +73,7 @@ def delabToRefinableSyntax (e : Expr) : MetaM Term :=
 
 /-- Delaborate `e` into a suggestion suitable for use by `refine`. -/
 def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion :=
-  return { suggestion := ← delabToRefinableSyntax e, messageData? := e }
+  return { suggestion := ← delabToRefinableSyntax e, messageData? := ← addMessageContext <| toMessageData e }
 
 /-- Add a "try this" suggestion. This has two effects:
 
