diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 24b1c41aa5..5836ab2bb7 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -169,7 +169,7 @@ partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List Goal
         | failure
       let trailSize := i.stx.getTrailingSize
       guard <| pos ≤ hoverPos ∧ hoverPos < tailPos + trailSize
-      return { ctxInfo := ctx, tacticInfo := ti, useAfter := hoverPos >= tailPos }
+      return { ctxInfo := ctx, tacticInfo := ti, useAfter := hoverPos > pos }
     | _, _ => none
 
 end Lean.Elab
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index cc57ab815e..845d830c51 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -4,5 +4,5 @@
  "goals": ["α : Sort ?u\n⊢ α → α"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 1, "character": 3}}
-{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
- "goals": ["α : Sort ?u\n⊢ α → α"]}
+{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
+ "goals": ["α : Sort ?u\na : α\n⊢ α"]}