diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 6a023064cb..9c08dd45ee 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -150,19 +150,23 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
 
 /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
 partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) : Option (ContextInfo × Info) := Id.run do
-  let results := t.visitM (m := Id) (postNode := fun ctx i _ results => do
+  let results := t.visitM (m := Id) (postNode := fun ctx info _ results => do
     let mut results := results.bind (·.getD [])
-    if omitAppFns && i.stx.isOfKind ``Parser.Term.app && i.stx[0].isIdent then
-      results := results.filter (·.2.2.stx != i.stx[0])
-    if results.isEmpty && (i matches Info.ofFieldInfo _ || i.toElabInfo?.isSome) && i.contains hoverPos includeStop then
-      let r := i.range?.get!
+    if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then
+      results := results.filter (·.2.2.stx != info.stx[0])
+    /-
+      Remark: we skip `info` nodes associated with the `nullKind` because some tactics (e.g., `rewrite`) attach auxiliary null nodes to control
+      which goal is displayed in the info views. See issue #1403
+    -/
+    if results.isEmpty && info.stx.getKind != nullKind && (info matches Info.ofFieldInfo _ || info.toElabInfo?.isSome) && info.contains hoverPos includeStop then
+      let r := info.range?.get!
       let priority :=
         if r.stop == hoverPos then
           0  -- prefer results directly *after* the hover position (only matters for `includeStop = true`; see #767)
-        else if i matches .ofTermInfo { expr := .fvar .., .. } then
+        else if info matches .ofTermInfo { expr := .fvar .., .. } then
           0  -- prefer results for constants over variables (which overlap at declaration names)
         else 1
-      [(priority, ctx, i)]
+      [(priority, ctx, info)]
     else
       results) |>.getD []
   let maxPrio? := results.map (·.1) |>.maximum?
diff --git a/tests/lean/interactive/1403.lean b/tests/lean/interactive/1403.lean
new file mode 100644
index 0000000000..cf8c0a4aaf
--- /dev/null
+++ b/tests/lean/interactive/1403.lean
@@ -0,0 +1,4 @@
+example : True := by
+  rewrite []
+--^ textDocument/hover
+  trivial
diff --git a/tests/lean/interactive/1403.lean.expected.out b/tests/lean/interactive/1403.lean.expected.out
new file mode 100644
index 0000000000..d2c5e00720
--- /dev/null
+++ b/tests/lean/interactive/1403.lean.expected.out
@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file://1403.lean"},
+ "position": {"line": 1, "character": 2}}
+{"range":
+ {"start": {"line": 1, "character": 2}, "end": {"line": 1, "character": 12}},
+ "contents":
+ {"value":
+  "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used. This provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal.\n",
+  "kind": "markdown"}}