diff --git a/tests/lean/interactive/lean3HoverIssue.lean b/tests/lean/interactive/lean3HoverIssue.lean
new file mode 100644
index 0000000000..885a59e73c
--- /dev/null
+++ b/tests/lean/interactive/lean3HoverIssue.lean
@@ -0,0 +1,12 @@
+example (x y : Nat) (h : x = y) : y = x := by exact h.symm
+                                                     --^ textDocument/hover
+                                                  --^ textDocument/hover
+
+example (x y : Nat) (h : x = y) : y = x := h.symm
+                                            --^ textDocument/hover
+
+example (x y : Nat) (h : x = y) : y = x := by exact (Eq.symm (Eq.symm h.symm))
+                                                    --^ textDocument/hover
+                                                               --^ textDocument/hover
+                                                                    --^ textDocument/hover
+                                                                      --^ textDocument/hover
diff --git a/tests/lean/interactive/lean3HoverIssue.lean.expected.out b/tests/lean/interactive/lean3HoverIssue.lean.expected.out
new file mode 100644
index 0000000000..20c60ed87d
--- /dev/null
+++ b/tests/lean/interactive/lean3HoverIssue.lean.expected.out
@@ -0,0 +1,45 @@
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 0, "character": 55}}
+{"range":
+ {"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}},
+ "contents":
+ {"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 0, "character": 52}}
+{"range":
+ {"start": {"line": 0, "character": 52}, "end": {"line": 0, "character": 53}},
+ "contents": {"value": "```lean\nh : x = y\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 4, "character": 46}}
+{"range":
+ {"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}},
+ "contents":
+ {"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 7, "character": 54}}
+{"range":
+ {"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}},
+ "contents":
+ {"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 7, "character": 65}}
+{"range":
+ {"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}},
+ "contents":
+ {"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 7, "character": 70}}
+{"range":
+ {"start": {"line": 7, "character": 70}, "end": {"line": 7, "character": 71}},
+ "contents": {"value": "```lean\nh : x = y\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
+ "position": {"line": 7, "character": 72}}
+{"range":
+ {"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}},
+ "contents":
+ {"value": "```lean\n@Eq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```",
+  "kind": "markdown"}}