diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 948617c210..c4f79476de 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -115,6 +115,8 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
 @[builtinTermElab «letrec»] def elabLetRec : TermElab := fun stx expectedType? => do
   let view ← mkLetRecDeclView stx
   withAuxLocalDecls view.decls fun fvars => do
+    for decl in view.decls, fvar in fvars do
+      addTermInfo (isBinder := true) decl.ref[0] fvar
     let values ← elabLetRecDeclValues view
     let body ← elabTermEnsuringType view.body expectedType?
     registerLetRecsToLift view.decls fvars values
diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean
index c90a7b9c9d..edfaa7bdff 100644
--- a/tests/lean/interactive/goTo.lean
+++ b/tests/lean/interactive/goTo.lean
@@ -49,5 +49,6 @@ example : Nat :=
   let a := 1
 --v textDocument/definition
   a + b
+    --^ textDocument/definition
 where
   b := 2
diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out
index 0e559e5c69..6d9baf3c15 100644
--- a/tests/lean/interactive/goTo.lean.expected.out
+++ b/tests/lean/interactive/goTo.lean.expected.out
@@ -96,3 +96,12 @@
   {"start": {"line": 48, "character": 6}, "end": {"line": 48, "character": 7}},
   "originSelectionRange":
   {"start": {"line": 50, "character": 2}, "end": {"line": 50, "character": 3}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 50, "character": 6}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 53, "character": 2}, "end": {"line": 53, "character": 3}},
+  "targetRange":
+  {"start": {"line": 53, "character": 2}, "end": {"line": 53, "character": 3}},
+  "originSelectionRange":
+  {"start": {"line": 50, "character": 6}, "end": {"line": 50, "character": 7}}}]