feat: server: show goal state after tactic if cursor not strictly before tactic

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

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⊢ α"]}