diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 1e211516be47..9d312dea11e1 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -66,11 +66,11 @@ def handleHover (p : HoverParams)
         | none => pure none
 
       -- now try info tree
-      if let some (ci, i) := snap.infoTree.hoverableInfoAt? hoverPos then
-        if let some range := i.range? then
+      if let some ictx := snap.infoTree.hoverableInfoAt? hoverPos then
+        if let some range := ictx.info.range? then
           -- prefer info tree if at least as specific as parser docstring
           if stxDoc?.all fun (_, stxRange) => stxRange.includes range then
-            if let some hoverFmt ← i.fmtHover? ci then
+            if let some hoverFmt ← ictx.info.fmtHover? ictx.ctx then
               return mkHover (toString hoverFmt.fmt) range
 
       if let some (doc, range) := stxDoc? then
@@ -79,7 +79,7 @@ def handleHover (p : HoverParams)
       return none
 
 open Elab GoToKind in
-def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info)
+def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
     (infoTree? : Option InfoTree := none) : RequestM (Array LocationLink) := do
   let rc ← read
   let doc ← readDoc
@@ -116,6 +116,9 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
       return #[ll]
     return #[]
 
+  let i := ictx.info
+  let ci := ictx.ctx
+  let children := ictx.children
   match i with
   | .ofTermInfo ti =>
     let mut expr := ti.expr
@@ -126,6 +129,43 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
     | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
     | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
     | _ => pure ()
+
+    -- Check whether this `TermInfo` node is directly responsible for its `.expr`.
+    -- This is the case iff all of its children represent strictly smaller subexpressions;
+    -- it is sufficient to check this of all direct children of this node (and that its elaborator didn't expand it as a macro)
+    let isExprGenerator := children.all fun
+      | .node (Info.ofTermInfo info) _ => info.expr != expr
+      | .node (Info.ofMacroExpansionInfo _) _ => false
+      | _ => true
+
+    -- don't go-to-instance if this `TermInfo` didn't directly generate its `.expr`
+    if kind != declaration && isExprGenerator then
+      -- go-to-definition on a projection application of a typeclass
+      -- should return all instances generated by TC
+      expr ← ci.runMetaM i.lctx do instantiateMVars expr
+      if let .const n _ := expr.getAppFn then
+        -- also include constant along with instance results
+        let mut results ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
+        if let some info := ci.env.getProjectionFnInfo? n then
+          let mut elaborators := default
+          if let some ei := i.toElabInfo? then do
+            -- also include elaborator along with instance results, as this wouldn't be accessible otherwise
+            if ei.elaborator != `Delab -- prevent an error if this `TermInfo` came from the infoview
+              && ei.elaborator != `Lean.Elab.Term.elabApp && ei.elaborator != `Lean.Elab.Term.elabIdent -- don't include trivial elaborators
+              then do
+              elaborators ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
+          let instIdx := info.numParams
+          let appArgs := expr.getAppArgs
+          let rec extractInstances : Expr → RequestM (Array Name)
+            | .const declName _ => do
+              if ← ci.runMetaM i.lctx do Lean.Meta.isInstance declName then pure #[declName] else pure #[]
+            | .app fn arg => do pure $ (← extractInstances fn).append (← extractInstances arg)
+            | _ => pure #[]
+          if let some instArg := appArgs.get? instIdx then
+            for inst in (← extractInstances instArg) do
+              results := results.append (← ci.runMetaM i.lctx <| locationLinksFromDecl i inst)
+            results := results.append elaborators -- put elaborators at the end of the results
+        return results
   | .ofFieldInfo fi =>
     if kind == type then
       let expr ← ci.runMetaM i.lctx do
@@ -157,8 +197,8 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
 
   withWaitFindSnap doc (fun s => s.endPos > hoverPos)
     (notFoundX := pure #[]) fun snap => do
-      if let some (ci, i) := snap.infoTree.hoverableInfoAt? (includeStop := true /- #767 -/) hoverPos then
-        locationLinksOfInfo kind ci i snap.infoTree
+      if let some infoWithCtx := snap.infoTree.hoverableInfoAt? (omitIdentApps := true) (includeStop := true /- #767 -/) hoverPos then
+        locationLinksOfInfo kind infoWithCtx snap.infoTree
       else return #[]
 
 open RequestM in
@@ -214,7 +254,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
   let hoverPos := text.lspPosToUtf8Pos p.position
   withWaitFindSnap doc (fun s => s.endPos > hoverPos)
     (notFoundX := pure none) fun snap => do
-      if let some (ci, i@(Elab.Info.ofTermInfo ti)) := snap.infoTree.termGoalAt? hoverPos then
+      if let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := snap.infoTree.termGoalAt? hoverPos then
         let ty ← ci.runMetaM i.lctx do
           instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
         -- for binders, hide the last hypothesis (the binder itself)
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 1e5b8e2d2455..a3918d62f3c1 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -15,7 +15,7 @@ import Lean.Server.FileWorker.RequestHandling
 /-! Registers all widget-related RPC procedures. -/
 
 namespace Lean.Widget
-open Server
+open Server Lean.Elab
 
 structure MsgToInteractive where
   msg : WithRpcRef MessageData
@@ -127,7 +127,7 @@ builtin_initialize
     (Array Lsp.LocationLink)
     fun ⟨kind, ⟨i⟩⟩ => RequestM.asTask do
       let rc ← read
-      let ls ← FileWorker.locationLinksOfInfo kind i.ctx i.info
+      let ls ← FileWorker.locationLinksOfInfo kind i
       if !ls.isEmpty then return ls
       -- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
       let .ofTermInfo ti := i.info | return #[]
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index b0658aafc066..a9f52e24729b 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -8,6 +8,33 @@ import Lean.PrettyPrinter
 
 namespace Lean.Elab
 
+/-- Elaborator information with elaborator context.
+
+It can be thought of as a "thunked" elaboration computation that allows us
+to retroactively extract type information, symbol locations, etc.
+through arbitrary invocations of `runMetaM` (where the necessary context and state
+can be reconstructed from `ctx` and `info.lctx`).
+
+W.r.t. widgets, this is used to tag different parts of expressions in `ppExprTagged`.
+This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
+It carries over information about delaborated
+`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
+functionality is purpose-specific to showing the contents of infoview popups.
+
+For use in standard LSP go-to-definition (see `Lean.Server.FileWorker.locationLinksOfInfo`),
+all the elaborator information we need for similar tasks is already fully recoverable via
+the `InfoTree` structure (see `Lean.Elab.InfoTree.visitM`).
+There we use this as a convienience wrapper for queried nodes (e.g. the return value of
+`Lean.Elab.InfoTree.hoverableInfoAt?`). It also includes the children info nodes
+as additional context (this is unused in the RPC case, as delaboration has no notion of child nodes).
+
+NOTE: This type is for internal use in the infoview/LSP. It should not be used in user widgets.
+-/
+structure InfoWithCtx where
+  ctx  : Elab.ContextInfo
+  info : Elab.Info
+  children : PersistentArray InfoTree
+
 /-- Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up. -/
 partial def InfoTree.visitM [Monad m]
     (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
@@ -135,11 +162,16 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
   infos.toArray.getMax? (fun a b => a.1 > b.1) |>.map fun (_, ci, i) => (ci, i)
 
 /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
-partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) : Option (ContextInfo × Info) := Id.run do
-  let results := t.visitM (m := Id) (postNode := fun ctx info _ results => do
+partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) (omitIdentApps := false) : Option InfoWithCtx := Id.run do
+  let results := t.visitM (m := Id) (postNode := fun ctx info children results => do
     let mut results := results.bind (·.getD [])
     if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then
-      results := results.filter (·.2.2.stx != info.stx[0])
+        results := results.filter (·.2.info.stx != info.stx[0])
+    if omitIdentApps && info.stx.isIdent then
+      -- if an identifier stands for an application (e.g. in the case of a typeclass projection), prefer the application
+      if let .ofTermInfo ti := info then
+        if ti.expr.isApp then
+          results := results.filter (·.2.info.stx != info.stx)
     unless results.isEmpty do
       return results  -- prefer innermost results
     /-
@@ -161,7 +193,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
       Int.negOfNat (r.stop - r.start).byteIdx,
       -- prefer results for constants over variables (which overlap at declaration names)
       if info matches .ofTermInfo { expr := .fvar .., .. } then 0 else 1)
-    [(priority, ctx, info)]) |>.getD []
+    [(priority, {ctx, info, children})]) |>.getD []
   -- sort results by lexicographical priority
   let maxPrio? :=
     let _ := @lexOrd
@@ -169,8 +201,8 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
     let _ := @maxOfLe
     results.map (·.1) |>.maximum?
   let res? := results.find? (·.1 == maxPrio?) |>.map (·.2)
-  if let some (_, i) := res? then
-    if let .ofTermInfo ti := i then
+  if let some i := res? then
+    if let .ofTermInfo ti := i.info then
       if ti.expr.isSyntheticSorry then
         return none
   return res?
@@ -328,7 +360,7 @@ where
     stx.getNumArgs == 2 && stx[0].isToken "by" && stx[1].getNumArgs == 1 && stx[1][0].isMissing
 
 
-partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) :=
+partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option InfoWithCtx :=
   -- In the case `f a b`, where `f` is an identifier, the term goal at `f` should be the goal for the full application `f a b`.
   hoverableInfoAt? t hoverPos (includeStop := true) (omitAppFns := true)
 
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index a991a19bd7f2..fd0dd3005c7f 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -1,26 +1,13 @@
 import Lean.Elab.InfoTree
 import Lean.Message
 import Lean.Server.Rpc.Basic
+import Lean.Server.InfoUtils
 
 namespace Lean.Widget
 
 open Elab Server
 
-/-- Elaborator information with elaborator context.
-
-This is used to tag different parts of expressions in `ppExprTagged`.
-This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
-
-The purpose of `InfoWithCtx` is to carry over information about delaborated
-`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
-functionality is purpose-specific to showing the contents of infoview popups.
-
-NOTE: This type is for internal use in the infoview. It should not be used in user widgets. -/
-structure InfoWithCtx where
-  ctx  : Elab.ContextInfo
-  info : Elab.Info
-  deriving TypeName
-
+deriving instance TypeName for InfoWithCtx
 deriving instance TypeName for MessageData
 deriving instance TypeName for LocalContext
 deriving instance TypeName for Elab.ContextInfo
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index de70d7e49595..edff58cfd558 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki
 -/
 import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
+import Lean.Server.InfoUtils
 import Lean.Widget.TaggedText
 import Lean.Widget.Basic
 
@@ -28,7 +29,7 @@ inductive DiffTag where
 /-- Information about a subexpression within delaborated code. -/
 structure SubexprInfo where
   /-- The `Elab.Info` node with the semantics of this part of the output. -/
-  info : WithRpcRef InfoWithCtx
+  info : WithRpcRef Lean.Elab.InfoWithCtx
   /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/
   subexprPos : Lean.SubExpr.Pos
   -- TODO(WN): add fields for semantic highlighting
@@ -67,7 +68,7 @@ where
       | none   => go subTt
       | some i =>
         let t : SubexprInfo := {
-          info := WithRpcRef.mk { ctx, info := i }
+          info := WithRpcRef.mk { ctx, info := i, children := .empty }
           subexprPos := n
         }
         TaggedText.tag t (go subTt)
diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean
index 16581f4382f6..910db5f838e8 100644
--- a/tests/lean/interactive/goTo.lean
+++ b/tests/lean/interactive/goTo.lean
@@ -36,9 +36,9 @@ def mkFoo₂ := mkFoo₁
 
 syntax (name := elabTest) "test" : term
 
-@[term_elab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun _ _ => do
+@[term_elab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun orig _ => do
   let stx ← `(2)
-  Lean.Elab.Term.elabTerm stx none
+  Lean.Elab.withMacroExpansionInfo orig stx $ Lean.Elab.Term.elabTerm stx none
 
      --v textDocument/declaration
 #check test
@@ -61,6 +61,54 @@ macro_rules | `(test) => `(3)
 #check test
      --^ textDocument/definition
 
+class Foo2 where
+  foo : Nat → Nat
+  foo' : Nat
+
+class Foo3 [Foo2] where
+  foo : [Foo2] → Nat
+
+class inductive Foo4 : Nat → Type where
+| mk : Nat → Foo4 0
+
+def Foo4.foo : [Foo4 n] → Nat
+| .mk n => n
+
+class Foo5 where
+  foo : Foo2
+
+
+instance : Foo2 := .mk id 0
+instance : Foo3 := .mk 0
+instance : Foo4 0 := .mk 0
+instance [foo2 : Foo2] : Foo5 := .mk foo2
+
+-- should go-to instance
+              --v textDocument/definition
+#check Foo2.foo  2
+          --^ textDocument/definition
+#check (Foo2.foo)
+           --^ textDocument/definition
+#check (Foo2.foo')
+           --^ textDocument/definition
+
+-- should go-to projection
+#check @Foo2.foo
+           --^ textDocument/definition
+
+-- test that the correct instance index is extracted
+#check (Foo3.foo)
+           --^ textDocument/definition
+
+-- non-projections should not go-to instance
+#check (Foo4.foo)
+           --^ textDocument/definition
+
+set_option pp.all true in
+-- test that multiple instances can be extracted
+#check (Foo5.foo)
+           --^ textDocument/definition
+
 -- duplicate definitions link to the original
 def mkFoo₁ := 1
      --^ textDocument/definition
diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out
index 0799a12b12c1..ba756c710be2 100644
--- a/tests/lean/interactive/goTo.lean.expected.out
+++ b/tests/lean/interactive/goTo.lean.expected.out
@@ -93,7 +93,7 @@
    "end": {"line": 38, "character": 38}},
   "targetRange":
   {"start": {"line": 38, "character": 22},
-   "end": {"line": 40, "character": 34}},
+   "end": {"line": 40, "character": 78}},
   "originSelectionRange":
   {"start": {"line": 43, "character": 7},
    "end": {"line": 43, "character": 11}}}]
@@ -136,12 +136,140 @@
   {"start": {"line": 60, "character": 7},
    "end": {"line": 60, "character": 11}}}]
 {"textDocument": {"uri": "file://goTo.lean"},
- "position": {"line": 64, "character": 7}}
+ "position": {"line": 87, "character": 16}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 87, "character": 7},
+   "end": {"line": 87, "character": 18}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 87, "character": 7},
+   "end": {"line": 87, "character": 18}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 87, "character": 12}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 87, "character": 7},
+   "end": {"line": 87, "character": 15}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 89, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 89, "character": 8},
+   "end": {"line": 89, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 89, "character": 8},
+   "end": {"line": 89, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 91, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 6}},
+  "targetRange":
+  {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 6}},
+  "originSelectionRange":
+  {"start": {"line": 91, "character": 8},
+   "end": {"line": 91, "character": 17}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 91, "character": 8},
+   "end": {"line": 91, "character": 17}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 95, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 95, "character": 8},
+   "end": {"line": 95, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 99, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 68, "character": 2}, "end": {"line": 68, "character": 5}},
+  "targetRange":
+  {"start": {"line": 68, "character": 2}, "end": {"line": 68, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 99, "character": 8},
+   "end": {"line": 99, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 81, "character": 0}, "end": {"line": 81, "character": 8}},
+  "targetRange":
+  {"start": {"line": 81, "character": 0}, "end": {"line": 81, "character": 24}},
+  "originSelectionRange":
+  {"start": {"line": 99, "character": 8},
+   "end": {"line": 99, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 103, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 73, "character": 4}, "end": {"line": 73, "character": 12}},
+  "targetRange":
+  {"start": {"line": 73, "character": 0}, "end": {"line": 74, "character": 12}},
+  "originSelectionRange":
+  {"start": {"line": 103, "character": 8},
+   "end": {"line": 103, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 108, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 77, "character": 2}, "end": {"line": 77, "character": 5}},
+  "targetRange":
+  {"start": {"line": 77, "character": 2}, "end": {"line": 77, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 108, "character": 8},
+   "end": {"line": 108, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 83, "character": 0}, "end": {"line": 83, "character": 8}},
+  "targetRange":
+  {"start": {"line": 83, "character": 0}, "end": {"line": 83, "character": 41}},
+  "originSelectionRange":
+  {"start": {"line": 108, "character": 8},
+   "end": {"line": 108, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 108, "character": 8},
+   "end": {"line": 108, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 112, "character": 7}}
 [{"targetUri": "file://goTo.lean",
   "targetSelectionRange":
   {"start": {"line": 9, "character": 4}, "end": {"line": 9, "character": 10}},
   "targetRange":
   {"start": {"line": 9, "character": 0}, "end": {"line": 17, "character": 1}},
   "originSelectionRange":
-  {"start": {"line": 64, "character": 4},
-   "end": {"line": 64, "character": 10}}}]
+  {"start": {"line": 112, "character": 4},
+   "end": {"line": 112, "character": 10}}}]
diff --git a/tests/lean/interactive/goto2.lean b/tests/lean/interactive/goTo2.lean
similarity index 100%
rename from tests/lean/interactive/goto2.lean
rename to tests/lean/interactive/goTo2.lean
diff --git a/tests/lean/interactive/goto2.lean.expected.out b/tests/lean/interactive/goTo2.lean.expected.out
similarity index 81%
rename from tests/lean/interactive/goto2.lean.expected.out
rename to tests/lean/interactive/goTo2.lean.expected.out
index 203cbc0bc8fa..3dc760c2d105 100644
--- a/tests/lean/interactive/goto2.lean.expected.out
+++ b/tests/lean/interactive/goTo2.lean.expected.out
@@ -1,6 +1,6 @@
-{"textDocument": {"uri": "file://goto2.lean"},
+{"textDocument": {"uri": "file://goTo2.lean"},
  "position": {"line": 10, "character": 15}}
-[{"targetUri": "file://goto2.lean",
+[{"targetUri": "file://goTo2.lean",
   "targetSelectionRange":
   {"start": {"line": 1, "character": 0}, "end": {"line": 1, "character": 55}},
   "targetRange":
@@ -8,9 +8,9 @@
   "originSelectionRange":
   {"start": {"line": 10, "character": 11},
    "end": {"line": 10, "character": 20}}}]
-{"textDocument": {"uri": "file://goto2.lean"},
+{"textDocument": {"uri": "file://goTo2.lean"},
  "position": {"line": 10, "character": 27}}
-[{"targetUri": "file://goto2.lean",
+[{"targetUri": "file://goTo2.lean",
   "targetSelectionRange":
   {"start": {"line": 2, "character": 0}, "end": {"line": 2, "character": 55}},
   "targetRange":
@@ -18,9 +18,9 @@
   "originSelectionRange":
   {"start": {"line": 10, "character": 23},
    "end": {"line": 10, "character": 30}}}]
-{"textDocument": {"uri": "file://goto2.lean"},
+{"textDocument": {"uri": "file://goTo2.lean"},
  "position": {"line": 10, "character": 11}}
-[{"targetUri": "file://goto2.lean",
+[{"targetUri": "file://goTo2.lean",
   "targetSelectionRange":
   {"start": {"line": 14, "character": 4}, "end": {"line": 14, "character": 5}},
   "targetRange":