diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 9879bc97bc..c14b7936f0 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -418,7 +418,7 @@ where
 
   /- Check whether `stx` is a pattern variable or constructor-like (i.e., constructor or constant tagged with `[matchPattern]` attribute) -/
   processId (stx : Syntax) : M Syntax := do
-    match (← resolveId? stx "pattern") with
+    match (← resolveId? stx "pattern" (withInfo := true)) with
     | none   => processVar stx
     | some f => match f with
       | Expr.const fName _ _ =>
@@ -480,7 +480,7 @@ where
       | `($fId:ident)  => pure (fId, false)
       | `(@$fId:ident) => pure (fId, true)
       | _              => throwError "identifier expected"
-    let some (Expr.const fName _ _) ← resolveId? fId "pattern" | throwCtorExpected
+    let some (Expr.const fName _ _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected
     let fInfo ← getConstInfo fName
     let paramDecls ← forallTelescopeReducing fInfo.type fun xs _ => xs.mapM fun x => do
       let d ← getFVarLocalDecl x
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index ba073d2cf0..3d7e6900d9 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -98,7 +98,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
 -/
 def elabTermForApply (stx : Syntax) : TacticM Expr := do
   if stx.isIdent then
-    match (← Term.resolveId? stx) with
+    match (← Term.resolveId? stx (withInfo := true)) with
     | some e => return e
     | _      => pure ()
   elabTerm stx none (mayPostpone := true)
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 1c5ac9d636..f8609346d2 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -102,7 +102,7 @@ where
   resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Expr) := do
     if simpArgTerm.isIdent then
       try
-        Term.resolveId? simpArgTerm
+        Term.resolveId? simpArgTerm (withInfo := true)
       catch _ =>
         return none
     else
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 1febd3053d..2565efcfff 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1475,7 +1475,7 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? :
         return (c, id, newFields.toList)
   | _ => throwError "identifier expected"
 
-def resolveId? (stx : Syntax) (kind := "term") : TermElabM (Option Expr) :=
+def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) :=
   match stx with
   | Syntax.ident _ _ val preresolved => do
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
@@ -1483,8 +1483,11 @@ def resolveId? (stx : Syntax) (kind := "term") : TermElabM (Option Expr) :=
     let fs := rs.map fun (f, _) => f
     match fs with
     | []  => pure none
-    | [f] => pure (some f)
-    | _   =>   throwError "ambiguous {kind}, use fully qualified name, possible interpretations {fs}"
+    | [f] =>
+      if withInfo then
+        addTermInfo stx f
+      pure (some f)
+    | _   => throwError "ambiguous {kind}, use fully qualified name, possible interpretations {fs}"
   | _ => throwError "identifier expected"
 
 @[builtinTermElab cdot] def elabBadCDot : TermElab := fun stx _ =>
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 59a8b74881..f20538dcdf 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -189,6 +189,7 @@
           | (z, w) =>
             let z1 : Nat := z + w;
             z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩
+            Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
             [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
             [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
             (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
new file mode 100644
index 0000000000..c02210f459
--- /dev/null
+++ b/tests/lean/interactive/hover.lean
@@ -0,0 +1,13 @@
+example : True := by
+  apply True.intro
+      --^ textDocument/hover
+
+example : True := by
+  simp [True.intro]
+      --^ textDocument/hover
+
+example (n : Nat) : True := by
+  match n with
+  | Nat.zero => _
+  --^ textDocument/hover
+  | n + 1 => _
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
new file mode 100644
index 0000000000..c0852be715
--- /dev/null
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -0,0 +1,15 @@
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 1, "character": 8}}
+{"range":
+ {"start": {"line": 1, "character": 8}, "end": {"line": 1, "character": 18}},
+ "contents": {"value": "```lean\nTrue.intro : True\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 5, "character": 8}}
+{"range":
+ {"start": {"line": 5, "character": 8}, "end": {"line": 5, "character": 18}},
+ "contents": {"value": "```lean\nTrue.intro : True\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 10, "character": 4}}
+{"range":
+ {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 12}},
+ "contents": {"value": "```lean\nNat.zero : Nat\n```", "kind": "markdown"}}