diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index dfb639f395..3e41e9e50c 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -58,12 +58,9 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
   -- We don't want to create an info tree node from a simple attribute to the generic parser.
   let declTarget := if attrSyntaxNodeKind == ``Lean.Parser.Attr.simple then impl.ref else attrSyntaxNodeKind
   if (← getEnv).contains declTarget && (← getInfoState).enabled then
-    pushInfoLeaf <| Info.ofTermInfo {
-      elaborator    := .anonymous
-      lctx          := {}
-      expr          := mkConst declTarget
-      stx           := attrInstance[1][0] -- We want to associate the information to the first atom only
-      expectedType? := none
+    pushInfoLeaf <| .ofCommandInfo {
+      elaborator := declTarget  -- not truly an elaborator, but a sensible target for go-to-definition
+      stx        := attrInstance[1][0] -- We want to associate the information to the first atom only
     }
   /- The `AttrM` does not have sufficient information for expanding macros in `args`.
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 876fcb994b..1dfb7ba799 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -160,3 +160,7 @@ def g (n : Nat) : Nat := g 0
 termination_by g n => n
 decreasing_by have n' := n; admit
                        --^ textDocument/hover
+
+@[inline]
+--^ textDocument/hover
+def one := 1
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 0a9bd24741..6709e7cbfe 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -228,3 +228,6 @@ null
  {"start": {"line": 160, "character": 25},
   "end": {"line": 160, "character": 26}},
  "contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 163, "character": 2}}
+null