chore: turn off pp.mvars in apply? results (#6108)

Per request on
[zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/apply.3F.20using.20tombstones/near/482895588).

src/Lean/Meta/Tactic/TryThis.lean

@@ -430,11 +430,13 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
   logInfoAt ref m!"{header}{msgs}"
   addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
 
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
+  withOptions (pp.mvars.set · false) do
   let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
   let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
+  let pp ← ppExpr e
+  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do

tests/lean/librarySearch.lean

@@ -15,6 +15,8 @@
 -- 1. update the comment using the code action on `#guard_msgs`
 -- 2. (optional) add `(drop info)` after `#guard_msgs` and change the doc-comment to a comment
 
+set_option linter.unusedVariables false
+
 noncomputable section
 
 /-- info: Try this: exact Nat.lt_add_one x -/
@@ -253,7 +255,7 @@ theorem Bool_eq_iff2 {A B : Bool} : (A = B) = (A ↔ B) := by
 --   | exact? says exact ge_antisymm hyx hxy
 
 /--
-info: Try this: refine Int.mul_ne_zero ?a0 h
+info: Try this: refine Int.mul_ne_zero ?_ h
 ---
 warning: declaration uses 'sorry'
 -/

tests/lean/run/3922.lean

@@ -18,9 +18,9 @@ axiom r.symm {a b : Nat} : r a b → r b a
 axiom r.trans {a b c : Nat} : r a b → r b c → r a c
 
 /--
-info: Try this: refine r.symm ?a✝
+info: Try this: refine r.symm ?_
 ---
-info: Try this: refine r.trans ?a✝ ?a✝¹
+info: Try this: refine r.trans ?_ ?_
 ---
 warning: declaration uses 'sorry'
 -/

tests/lean/run/show_term.lean

@@ -11,7 +11,7 @@ Authors: Kim Morrison
     exact n
     exact 37
 
-/-- info: Try this: refine (?fst, ?snd) -/
+/-- info: Try this: refine (?_, ?_) -/
 #guard_msgs in example : Nat × Nat := by
   show_term constructor
   repeat exact 42