diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 946e34da5c..6b01e900c7 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -375,7 +375,8 @@ section RequestHandling
     let text := doc.meta.text
     let pos := text.lspPosToUtf8Pos p.position
     -- dbg_trace ">> handleCompletion invoked {pos}"
-    withWaitFindSnap doc (fun s => s.endPos > pos)
+    -- NOTE: use `>=` since the cursor can be *after* the input
+    withWaitFindSnap doc (fun s => s.endPos >= pos)
       (notFoundX := pure { items := #[], isIncomplete := true }) fun snap => do
         for infoTree in snap.cmdState.infoState.trees do
           -- for (ctx, info) in infoTree.getCompletionInfos do
@@ -451,7 +452,8 @@ section RequestHandling
     let doc ← st.docRef.get
     let text := doc.meta.text
     let hoverPos := text.lspPosToUtf8Pos p.position
-    withWaitFindSnap doc (fun s => s.endPos > hoverPos)
+    -- NOTE: use `>=` since the cursor can be *after* the input
+    withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
       (notFoundX := return none) fun snap => do
         for t in snap.cmdState.infoState.trees do
           if let rs@(_ :: _) := t.goalsAt? hoverPos then
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 9287ab7119..0340ab40f3 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -156,11 +156,11 @@ structure GoalsAtResult where
 /-
   Try to retrieve `TacticInfo` for `hoverPos`.
   We retrieve the `TacticInfo` `info`, if there is a node of the form `node (ofTacticInfo info) children` s.t.
-  - If `hoverPos <= headPos && hoverPos < endPos + getTrailingSize` and
+  - `hoverPos` is sufficiently inside `info`'s range (see code), and
   - None of the `children` can provide satisfy the condition above. That is, for composite tactics such as
     `induction`, we always give preference for information stored in nested (children) tactics.
 
-  Moreover, we instruct the LSP server to use the state after the tactic execution If hoverPos >= endPos
+  Moreover, we instruct the LSP server to use the state after the tactic execution if hoverPos >= endPos
 -/
 partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := do
   t.deepestNodes fun
@@ -168,7 +168,9 @@ partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List Goal
       let (some pos, some tailPos) ← pure (i.pos?, i.tailPos?)
         | failure
       let trailSize := i.stx.getTrailingSize
-      guard <| pos ≤ hoverPos ∧ hoverPos < tailPos + trailSize
+      -- NOTE: include position just after tactic, i.e. when the cursor is still adjacent
+      -- (even when `trailSize == 0`, which is the case at EOF)
+      guard <| pos ≤ hoverPos ∧ hoverPos < tailPos + Nat.max 1 trailSize
       return { ctxInfo := ctx, tacticInfo := ti, useAfter := hoverPos > pos }
     | _, _ => none
 
diff --git a/tests/lean/interactive/completionEOF.lean b/tests/lean/interactive/completionEOF.lean
new file mode 100644
index 0000000000..31b03b3f66
--- /dev/null
+++ b/tests/lean/interactive/completionEOF.lean
@@ -0,0 +1,9 @@
+-- Local Variables:
+-- require-final-newline: nil
+-- End:
+prelude
+
+axiom And : Type
+
+       --v textDocument/completion
+#check An
\ No newline at end of file
diff --git a/tests/lean/interactive/completionEOF.lean.expected.out b/tests/lean/interactive/completionEOF.lean.expected.out
new file mode 100644
index 0000000000..e2708032cf
--- /dev/null
+++ b/tests/lean/interactive/completionEOF.lean.expected.out
@@ -0,0 +1,3 @@
+{"textDocument": {"uri": "file://completionEOF.lean"},
+ "position": {"line": 8, "character": 9}}
+{"items": [{"label": "And", "detail": "Type"}], "isIncomplete": true}
diff --git a/tests/lean/interactive/goalEOF.lean b/tests/lean/interactive/goalEOF.lean
new file mode 100644
index 0000000000..6e6b56655a
--- /dev/null
+++ b/tests/lean/interactive/goalEOF.lean
@@ -0,0 +1,6 @@
+-- Local Variables:
+-- require-final-newline: nil
+-- End:
+
+                       --v $/lean/plainGoal
+example : False := by rfl
\ No newline at end of file
diff --git a/tests/lean/interactive/goalEOF.lean.expected.out b/tests/lean/interactive/goalEOF.lean.expected.out
new file mode 100644
index 0000000000..8bb8197ac4
--- /dev/null
+++ b/tests/lean/interactive/goalEOF.lean.expected.out
@@ -0,0 +1,3 @@
+{"textDocument": {"uri": "file://goalEOF.lean"},
+ "position": {"line": 5, "character": 25}}
+{"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]}
diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean
index 9c26776039..56d7a9bd7c 100644
--- a/tests/lean/interactive/run.lean
+++ b/tests/lean/interactive/run.lean
@@ -20,13 +20,21 @@ partial def main (args : List String) : IO Unit := do
     let mut versionNo : Nat := 2
     let mut requestNo : Nat := 2
     for line in text.splitOn "\n" do
-      match line.splitOn "--^" with
+      match line.splitOn "--" with
       | [ws, directive] =>
+        let line ← match directive[0] with
+          | 'v' => pure <| lineNo + 1  -- TODO: support subsequent 'v'... or not
+          | '^' => pure <| lastActualLineNo
+          | _ =>
+            lastActualLineNo := lineNo
+            lineNo := lineNo + 1
+            continue
+        let directive := directive.drop 1
         let colon := directive.posOf ':'
         let method := directive.extract 0 colon |>.trim
         -- TODO: correctly compute in presence of Unicode
         let column := ws.bsize + "--".length
-        let pos : Lsp.Position := { line := lastActualLineNo, character := column }
+        let pos : Lsp.Position := { line := line, character := column }
         let params := if colon < directive.bsize then directive.extract (colon + 1) directive.bsize |>.trim else "{}"
         match method with
         | "insert" =>