diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 0864cfa59fc9..e1cabbb3b1ba 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1542,7 +1542,7 @@ macro "get_elem_tactic" : tactic =>
 
 /--
 Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
+for `exact?%` to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
 
diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean
index 758e8fec2b05..cd28472823c4 100644
--- a/src/Lean/Elab/Tactic/LibrarySearch.lean
+++ b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -68,11 +68,8 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     let (_, introdGoal) ← goal.mvarId!.intros
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
-        reportOutOfHeartbeats `library_search stx
-        for suggestion in suggestions do
-          withMCtx suggestion.2 do
-            addTermSuggestion stx (← instantiateMVars goal).headBeta
-        if suggestions.isEmpty then logError "exact?# didn't find any relevant lemmas"
+        if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
+        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
         mkSorry expectedType (synthetic := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta
diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean
index 02a7cd5f26a7..3688efadb09d 100644
--- a/tests/lean/librarySearch.lean
+++ b/tests/lean/librarySearch.lean
@@ -43,6 +43,14 @@ example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
 #guard_msgs in
 example : x < x + 1 := exact?%
 
+/-- error: `exact?%` didn't find any relevant lemmas -/
+#guard_msgs in
+example {α : Sort u} (x y : α) : Eq x y := exact?%
+
+/-- error: `exact?%` could not close the goal. Try `by apply` to see partial suggestions. -/
+#guard_msgs in
+example (x y : Nat) : x ≤ y := exact?%
+
 /-- info: Try this: exact p -/
 #guard_msgs in
 example (P : Prop) (p : P) : P := by apply?