From 3833984756c74d1dac426fe5584cb06ea3fffa7f Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Thu, 15 Jan 2026 17:05:35 +0100
Subject: [PATCH] feat: allow go-to-projection to look through reducible
 definitions (#12004)

This PR allows 'Go to Definition' to look through reducible definition
when looking for typeclass instance projections.

Specifically, this means that using 'Go to Definition' on uses of
`GT.gt` will now yield the corresponding `LT` instance as well.
---
 src/Lean/Server/GoTo.lean                     | 19 ++++++++---
 tests/lean/interactive/goTo.lean              | 12 +++++++
 tests/lean/interactive/goTo.lean.expected.out | 32 +++++++++++++++++++
 3 files changed, 58 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean
index 1846f16fc2..e2b08ca2c0 100644
--- a/src/Lean/Server/GoTo.lean
+++ b/src/Lean/Server/GoTo.lean
@@ -39,15 +39,24 @@ def GoToKind.determineTargetExprs (kind : GoToKind) (ti : TermInfo) : MetaM (Arr
   | _ =>
     return #[← instantiateMVars ti.expr]
 
-def getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr) := do
-  let env ← getEnv
-  let .const n _ := e.getAppFn'
-    | return none
-  let some projInfo := env.getProjectionFnInfo? n
+partial def getInstanceProjectionArg? (e : Expr) : MetaM (Option Expr) := do
+  let some (e, projInfo) ← Meta.withReducible <| reduceToProjection? e
     | return none
   let instIdx := projInfo.numParams
   let appArgs := e.getAppArgs
   return appArgs[instIdx]?
+where
+  reduceToProjection? (e : Expr) : MetaM (Option (Expr × ProjectionFunctionInfo)) := do
+    let env ← getEnv
+    let .const n _ := e.getAppFn'
+      | return none
+    if let some projInfo := env.getProjectionFnInfo? n then
+      return some (e, projInfo)
+    -- Unfold reducible definitions when looking for a projection.
+    -- For example, this ensures that we get `LT.lt` instance projection entries on `GT.gt`.
+    let some e ← Meta.unfoldDefinition? e
+      | return none
+    reduceToProjection? e
 
 def isInstanceProjection (e : Expr) : MetaM Bool := do
   return (← getInstanceProjectionArg? e).isSome
diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean
index 6b9a10c025..75b7566149 100644
--- a/tests/lean/interactive/goTo.lean
+++ b/tests/lean/interactive/goTo.lean
@@ -112,3 +112,15 @@ set_option pp.all true in
 -- duplicate definitions link to the original
 def mkFoo₁ := 1
      --^ textDocument/definition
+
+-- go-to-projection should be able to look through reducible definitions
+@[reducible] def foo'' (n : Nat) := Foo2.foo n
+
+#check foo'' 0
+      --^ textDocument/definition
+
+-- go-to-projection should not be able to look through semi-reducible definitions
+def foo''' (n : Nat) := Foo2.foo n
+
+#check foo''' 0
+      --^ textDocument/definition
diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out
index 81930cce30..d785b6c4fc 100644
--- a/tests/lean/interactive/goTo.lean.expected.out
+++ b/tests/lean/interactive/goTo.lean.expected.out
@@ -301,3 +301,35 @@
   "originSelectionRange":
   {"start": {"line": 112, "character": 4},
    "end": {"line": 112, "character": 10}}}]
+{"textDocument": {"uri": "file:///goTo.lean"},
+ "position": {"line": 118, "character": 8}}
+[{"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": 8}},
+  "originSelectionRange":
+  {"start": {"line": 118, "character": 7},
+   "end": {"line": 118, "character": 14}}},
+ {"targetUri": "file:///goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 116, "character": 17},
+   "end": {"line": 116, "character": 22}},
+  "targetRange":
+  {"start": {"line": 116, "character": 17},
+   "end": {"line": 116, "character": 22}},
+  "originSelectionRange":
+  {"start": {"line": 118, "character": 7},
+   "end": {"line": 118, "character": 14}}}]
+{"textDocument": {"uri": "file:///goTo.lean"},
+ "position": {"line": 124, "character": 8}}
+[{"targetUri": "file:///goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 122, "character": 4},
+   "end": {"line": 122, "character": 10}},
+  "targetRange":
+  {"start": {"line": 122, "character": 4},
+   "end": {"line": 122, "character": 10}},
+  "originSelectionRange":
+  {"start": {"line": 124, "character": 7},
+   "end": {"line": 124, "character": 13}}}]