diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 6483c67ea5..ac53946a0c 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -28,7 +28,10 @@ private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Synt
   let mvarId ← cleanup mvarId
   match decrTactic? with
   | none => applyDefaultDecrTactic mvarId
-  | some decrTactic => Term.runTactic mvarId decrTactic
+  | some decrTactic =>
+    -- make info from `runTactic` available
+    pushInfoTree (.hole mvarId)
+    Term.runTactic mvarId decrTactic
   instantiateMVars mvar
 
 private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) (F : Expr) (e : Expr) : TermElabM Expr := do
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 1a44249f99..07ccc44708 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -155,3 +155,8 @@ example : Nat → Nat → Nat := by
       --v textDocument/definition
   exact x
       --^ textDocument/hover
+
+def g (n : Nat) : Nat := g 0
+termination_by g n => n
+decreasing_by have n' := n; admit
+                       --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 6e41d7b22d..149212d872 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -221,3 +221,9 @@ null
 {"range":
  {"start": {"line": 155, "character": 8}, "end": {"line": 155, "character": 9}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 160, "character": 25}}
+{"range":
+ {"start": {"line": 160, "character": 25},
+  "end": {"line": 160, "character": 26}},
+ "contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}}