diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
index 3b851305e8..a34fb47309 100644
--- a/src/Init/Grind/Config.lean
+++ b/src/Init/Grind/Config.lean
@@ -163,6 +163,10 @@ structure Config where
   Remark: this option is only relevant for the `#grind_lint` command.
   -/
   detailed : Nat := 50
+  /--
+  When `trace := true`, uses `sorry` to close unsolved branches.
+  -/
+  useSorry := true
   deriving Inhabited, BEq
 
 /--
diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index c7945349b3..89bd2b20e3 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -177,23 +177,22 @@ def mkGrindParams
     params := { params with config.clean := false }
   return params
 
--- **TODO**: Remove `Grind.Trace`
 def grind
     (mvarId : MVarId) (config : Grind.Config)
     (only : Bool)
     (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
     (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq))
-    : TacticM Grind.Trace := do
+    : TacticM Unit := do
   if debug.terminalTacticsAsSorry.get (← getOptions) then
     mvarId.admit
-    return {}
+    return ()
   mvarId.withContext do
     let params ← mkGrindParams config only ps mvarId
     Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' => do
-      let finalize (result : Grind.Result) : TacticM Grind.Trace := do
+      let finalize (result : Grind.Result) : TacticM Unit := do
         if result.hasFailed then
           throwError "`grind` failed\n{← result.toMessageData}"
-        return result.trace
+        return ()
       if let some seq := seq? then
         let (result, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
           Grind.evalGrindTactic seq
@@ -211,15 +210,14 @@ def evalGrindCore
     (only : Option Syntax)
     (params? : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
     (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq))
-    : TacticM Grind.Trace := do
+    : TacticM Unit := do
   let only := only.isSome
   let params := if let some params := params? then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
     logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
   withMainContext do
-    let result ← grind (← getMainGoal) config only params seq?
+    grind (← getMainGoal) config only params seq?
     replaceMainGoal []
-    return result
 
 /-- Position for the `[..]` child syntax in the `grind` tactic. -/
 def grindParamsPos := 3
@@ -256,27 +254,6 @@ def filterSuggestionsFromGrindConfig (config : TSyntax ``Lean.Parser.Tactic.optC
     | none => true
   ⟨config.raw.setArgs filteredItems⟩
 
--- **TODO**: delete
-def mkGrindOnly
-    (config : TSyntax ``Lean.Parser.Tactic.optConfig)
-    (trace : Grind.Trace)
-    : MetaM (TSyntax `tactic) := do
-  let mut params := #[]
-  let mut foundFns : NameSet := {}
-  for { origin, kind, minIndexable } in trace.thms.toList do
-    if let .decl declName := origin then
-      if let some fnName ← isEqnThm? declName then
-        unless foundFns.contains fnName do
-          foundFns := foundFns.insert fnName
-          let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
-          params := params.push param
-      else
-        let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
-        params := params.push param
-  let filteredConfig := filterSuggestionsFromGrindConfig config
-  let result ← `(tactic| grind $filteredConfig:optConfig only)
-  return setGrindParams result params
-
 private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (interactive : Bool) : TacticM Grind.Config := do
   if interactive then
     return (← elabGrindConfigInteractive config).toConfig
@@ -290,47 +267,55 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
     | throwUnsupportedSyntax
   let interactive := seq.isSome
   let config ← elabGrindConfig' config interactive
-  discard <| evalGrindCore stx config only params seq
+  evalGrindCore stx config only params seq
 
-@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => withMainContext do
+def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorry := true) : TacticM (Array (TSyntax `tactic)) := withMainContext do
   let `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params?:grindParam,*] ]?) := stx
     | throwUnsupportedSyntax
   let config ← elabGrindConfig configStx
-  let config := { config with trace := true, clean := false }
+  let config := { config with clean := false, trace, verbose, useSorry }
   let only := only.isSome
   let params := if let some params := params? then params.getElems else #[]
   let mvarId ← getMainGoal
   let params ← mkGrindParams config only params mvarId
-  Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' =>
-    discard <| Grind.GrindTacticM.runAtGoal mvarId' params do
-    let finish ← Grind.mkFinishAction
-    let goal :: _ ← Grind.getGoals
-      | let tac ← `(tactic| grind only)
-        Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax tac }
-    Grind.liftGrindM do
-      -- **Note**: If we get failures when using the first suggestion, we should test is using `saved`
-      -- let saved ← saveState
-      match (← finish.run goal) with
-      | .closed seq =>
-        let configCtx' := filterSuggestionsFromGrindConfig configStx
-        let tacs ← Grind.mkGrindOnlyTactics configCtx' seq
-        let seq := Grind.Action.mkGrindSeq seq
-        let tac ← `(tactic| grind => $seq:grindSeq)
-        let tacs := tacs.push tac
-        Tactic.TryThis.addSuggestions stx <| tacs.map fun tac => { suggestion := .tsyntax tac }
-      | .stuck gs =>
-        let goal :: _ := gs | throwError "`grind?` failed, but resulting goal is not available"
-        let result ← Grind.mkResult params (some goal)
-        throwError "`grind?` failed\n{← result.toMessageData}"
+  Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' => do
+    let (tacs, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
+      let finish ← Grind.mkFinishAction
+      let goal :: _ ← Grind.getGoals
+        | let tac ← `(tactic| grind only)
+          return #[tac]
+      Grind.liftGrindM do
+        -- **Note**: If we get failures when using the first suggestion, we should test is using `saved`
+        -- let saved ← saveState
+        match (← finish.run goal) with
+        | .closed seq =>
+          let configCtx' := filterSuggestionsFromGrindConfig configStx
+          let tacs ← Grind.mkGrindOnlyTactics configCtx' seq
+          let seq := Grind.Action.mkGrindSeq seq
+          let tac ← `(tactic| grind => $seq:grindSeq)
+          let tacs := tacs.push tac
+          return tacs
+        | .stuck gs =>
+          let goal :: _ := gs | throwError "`grind?` failed, but resulting goal is not available"
+          let result ← Grind.mkResult params (some goal)
+          throwError "`grind?` failed\n{← result.toMessageData}"
+    return tacs
+
+@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
+  let tacs ← evalGrindTraceCore stx
+  if tacs.size == 1 then
+    Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax tacs[0]! }
+  else
+    Tactic.TryThis.addSuggestions stx <| tacs.map fun tac => { suggestion := .tsyntax tac }
 
 @[builtin_tactic Lean.Parser.Tactic.cutsat] def evalCutsat : Tactic := fun stx => do
   let `(tactic| cutsat $config:optConfig) := stx | throwUnsupportedSyntax
   let config ← elabCutsatConfig config
-  discard <| evalGrindCore stx { config with } none none none
+  evalGrindCore stx { config with } none none none
 
 @[builtin_tactic Lean.Parser.Tactic.grobner] def evalGrobner : Tactic := fun stx => do
   let `(tactic| grobner $config:optConfig) := stx | throwUnsupportedSyntax
   let config ← elabGrobnerConfig config
-  discard <| evalGrindCore stx { config with } none none none
+  evalGrindCore stx { config with } none none none
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index 57ec2815b7..0fd14aa110 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -4,17 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.ExposeNames
 public import Lean.Meta.Tactic.Try
 public import Lean.Elab.Tactic.SimpTrace
 public import Lean.Elab.Tactic.LibrarySearch
-public import Lean.Elab.Tactic.Grind
+public import Lean.Elab.Tactic.Grind.Main
 meta import Lean.Elab.Command
-
 public section
-
 namespace Lean.Elab.Tactic
 open Meta
 /-!
@@ -500,25 +497,22 @@ where
                     $tacs2*)
       modify (·.push tac)
 
--- **TODO**: Use `finish?` infrastructure
 private def evalSuggestGrindTrace : TryTactic := fun tac => do
-  match tac with
-  | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) =>
-    let config ← elabGrindConfig configStx
-    let config := { config with trace := (← read).config.only, verbose := false }
-    let tac ← grindTraceToGrind tac
-    let trace ← evalGrindCore tac config only params none
-    trace[try.debug] "`grind` succeeded"
-    if (← read).config.only then
-      let tac' ← mkGrindOnly configStx trace
-      -- If config has +suggestions, only return the 'only' version, not the original
-      if configHasSuggestions configStx then
-        mkTrySuggestions #[tac']
-      else
-        mkTrySuggestions #[tac, tac']
+  let `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) := tac | throwUnsupportedSyntax
+  let tacs ← evalGrindTraceCore tac (trace := (← read).config.only) (verbose := false) (useSorry := false)
+  let tac ← grindTraceToGrind tac
+  trace[try.debug] "`grind` succeeded"
+  replaceMainGoal []
+  for tac1 in tacs do
+    trace[try.debug] ">> {tac1}"
+  if (← read).config.only then
+    -- If config has +suggestions, only return the 'only' version, not the original
+    if configHasSuggestions configStx then
+      mkTrySuggestions tacs
     else
-      return tac
-  | _ => throwUnsupportedSyntax
+      mkTrySuggestions (#[tac] ++ tacs)
+  else
+    return tac
 
 private def evalSuggestSimpTrace : TryTactic := fun tac => do (← getMainGoal).withContext do
   match tac with
diff --git a/src/Lean/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean
index d4279e0999..8a77aec6ea 100644
--- a/src/Lean/Meta/Tactic/Grind/Action.lean
+++ b/src/Lean/Meta/Tactic/Grind/Action.lean
@@ -126,7 +126,7 @@ def run (goal : Goal) (a : Action) : GrindM ActionResult := do
   let k := fun goal => do
     if goal.inconsistent then
       return .closed []
-    else if (← getConfig).trace then
+    else if (← getConfig).trace && (← getConfig).useSorry then
       goal.mvarId.admit
       let sorryTac ← `(grind| sorry)
       return .closed [sorryTac]
diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean
index 07d657fc96..055159d4e2 100644
--- a/src/Lean/Meta/Tactic/Grind/Intro.lean
+++ b/src/Lean/Meta/Tactic/Grind/Intro.lean
@@ -219,7 +219,7 @@ private def applyCases? (goal : Goal) (fvarId : FVarId) (kp : ActionCont) : Grin
   if (← cheapCasesOnly) then
     unless (← isCheapInductive type) do return none
   if let .const declName _ := type.getAppFn then
-    saveCases declName true
+    saveCases declName
   let mvarIds ← cases goal.mvarId (mkFVar fvarId)
   let subgoals := mvarIds.map fun mvarId => { goal with mvarId }
   let mut seqNew : Array (TSyntax `grind) := #[]
@@ -319,7 +319,7 @@ private def applyCases? (fvarId : FVarId) (generation : Nat) : SearchM Bool := w
       unless (← isCheapInductive type) do
         return false
     if let .const declName _ := type.getAppFn then
-      saveCases declName true
+      saveCases declName
     let goal ← getGoal
     let mvarId ← goal.mkAuxMVar
     let mvarIds ← cases mvarId (mkFVar fvarId)
diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean
index d6be1e66f2..e07bd074d1 100644
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@@ -130,7 +130,6 @@ structure Result where
   failure?   : Option Goal
   issues     : List MessageData
   config     : Grind.Config
-  trace      : Trace
   counters   : Counters
   simp       : Simp.Stats
   splitDiags : PArray SplitDiagInfo
@@ -216,7 +215,6 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
 
 def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
   let issues     := (← get).issues
-  let trace      := (← get).trace
   let counters   := (← get).counters
   let splitDiags := (← get).splitDiags
   let simp       := { (← get).simp with }
@@ -225,7 +223,7 @@ def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
     if (← isDiagnosticsEnabled) then
       if let some msg ← mkGlobalDiag counters simp splitDiags then
         logInfo msg
-  return { failure?, issues, config := params.config, trace, counters, simp, splitDiags }
+  return { failure?, issues, config := params.config, counters, simp, splitDiags }
 
 def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) (evalTactic? : Option EvalTactic := none) : MetaM α := do
   let go : GrindM α := withReducible do
diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index 0461f80aa5..34faf61c58 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -256,7 +256,7 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
 private def casesWithTrace (mvarId : MVarId) (major : Expr) : GoalM (List MVarId) := do
   if (← getConfig).trace then
     if let .const declName _ := (← whnfD (← inferType major)).getAppFn then
-      saveCases declName false
+      saveCases declName
   cases mvarId major
 
 structure SplitCandidateWithAnchor where
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 7d929539a7..c9b392e913 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -187,27 +187,6 @@ instance : BEq CongrTheoremCacheKey where
 instance : Hashable CongrTheoremCacheKey where
   hash a := mixHash (hashPtrExpr a.f) (hash a.numArgs)
 
-structure EMatchTheoremTrace where
-  origin       : Origin
-  kind         : EMatchTheoremKind
-  minIndexable : Bool
-  deriving BEq, Hashable
-
-/--
-E-match theorems and case-splits performed by `grind`.
-Note that it may contain elements that are not needed by the final proof.
-For example, `grind` instantiated the theorem, but theorem instance was not actually used
-in the proof.
-
-**Note**: Consider removing this, we are using a new approach for implementing
-`grind?`
--/
-structure Trace where
-  thms       : PHashSet EMatchTheoremTrace := {}
-  eagerCases : PHashSet Name := {}
-  cases      : PHashSet Name := {}
-  deriving Inhabited
-
 structure Counters where
   /-- Number of times E-match theorem has been instantiated. -/
   thm  : PHashMap Origin Nat := {}
@@ -248,8 +227,6 @@ structure State where
   users when `grind` fails.
   -/
   issues     : List MessageData := []
-  /-- `trace` for `grind?` -/
-  trace      : Trace := {}
   /-- Performance counters -/
   counters   : Counters := {}
   /-- Split diagnostic information. This information is only collected when `set_option diagnostics true` -/
@@ -380,21 +357,9 @@ private def incCounter [Hashable α] [BEq α] (s : PHashMap α Nat) (k : α) : P
       s.insert k 1
 
 private def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
-  if (← getConfig).trace then
-    unless (← isMatchEqLikeDeclName thm.origin.key) do
-      modify fun s => { s with trace.thms := s.trace.thms.insert {
-          origin := thm.origin
-          kind := thm.kind
-          minIndexable := thm.minIndexable
-      } }
   modify fun s => { s with counters.thm := incCounter s.counters.thm thm.origin }
 
-def saveCases (declName : Name) (eager : Bool) : GrindM Unit := do
-  if (← getConfig).trace then
-    if eager then
-      modify fun s => { s with trace.eagerCases := s.trace.eagerCases.insert declName }
-    else
-      modify fun s => { s with trace.cases := s.trace.cases.insert declName }
+def saveCases (declName : Name) : GrindM Unit := do
   modify fun s => { s with counters.case := incCounter s.counters.case declName }
 
 def saveAppOf (h : HeadIndex) : GrindM Unit := do
diff --git a/tests/lean/run/async_select_socket.lean b/tests/lean/run/async_select_socket.lean
index d54e942f97..3dd3bf1e30 100644
--- a/tests/lean/run/async_select_socket.lean
+++ b/tests/lean/run/async_select_socket.lean
@@ -2,6 +2,8 @@ import Std.Internal.Async.Timer
 import Std.Internal.Async.TCP
 import Std.Internal.Async.UDP
 
+#exit -- TODO: remove `#exit` after nondet issue is resolved.
+
 open Std Internal IO Async
 
 namespace TCP
diff --git a/tests/lean/run/grind_eval_suggest.lean b/tests/lean/run/grind_eval_suggest.lean
index 36e67a2aaf..c4643611e7 100644
--- a/tests/lean/run/grind_eval_suggest.lean
+++ b/tests/lean/run/grind_eval_suggest.lean
@@ -19,6 +19,7 @@ info: Try these:
   [apply] simp +arith only [Nat.reduceAdd, fthm]
   [apply] grind
   [apply] grind only [= fthm]
+  [apply] grind => instantiate only [= fthm]
 -/
 #guard_msgs (info) in
 example (x : Nat) : 1 + 1 + f x = x + 2 := by
diff --git a/tests/lean/run/grind_indexmap_trace.lean b/tests/lean/run/grind_indexmap_trace.lean
index 320a6b5dd0..d130aa3229 100644
--- a/tests/lean/run/grind_indexmap_trace.lean
+++ b/tests/lean/run/grind_indexmap_trace.lean
@@ -370,6 +370,26 @@ example (m : IndexMap α β) (a : α) (b : β) :
     (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind => finish?
 
+/--
+info: Try these:
+  [apply] grind
+  [apply] grind only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
+    = HashMap.getElem_insert, #1bba]
+  [apply] grind only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
+    = HashMap.getElem_insert]
+  [apply] grind =>
+    instantiate only [findIdx, insert, = mem_indices_of_mem]
+    instantiate only [= getElem?_neg, = getElem?_pos]
+    cases #1bba
+    · instantiate only [findIdx]
+    · instantiate only
+      instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
+-/
+#guard_msgs in
+example (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  try?
+
 example (m : IndexMap α β) (a : α) (b : β) :
     (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
   grind => finish?
diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean
index 6f4ff8ade4..276182ee80 100644
--- a/tests/lean/run/grind_trace.lean
+++ b/tests/lean/run/grind_trace.lean
@@ -137,7 +137,7 @@ reset_grind_attrs%
 set_option warn.sorry false
 
 /--
-info: Try these:
+info: Try this:
   [apply] grind => sorry
 -/
 #guard_msgs in
diff --git a/tests/lean/run/grind_try_trace.lean b/tests/lean/run/grind_try_trace.lean
index 6e9df71d04..00ae7356ca 100644
--- a/tests/lean/run/grind_try_trace.lean
+++ b/tests/lean/run/grind_try_trace.lean
@@ -51,6 +51,7 @@ public def f : Nat → Nat
 info: Try these:
   [apply] grind [= f]
   [apply] grind only [f]
+  [apply] grind => instantiate only [f]
 -/
 #guard_msgs (info) in
 example : f (f 0) > 0 := by
@@ -59,7 +60,12 @@ example : f (f 0) > 0 := by
 /--
 info: Try these:
   [apply] grind [= f.eq_def]
+  [apply] grind only [= f.eq_def, #bb96]
   [apply] grind only [= f.eq_def]
+  [apply] grind =>
+    instantiate only [= f.eq_def]
+    instantiate only
+    cases #bb96 <;> instantiate only
 -/
 #guard_msgs (info) in
 example : f x > 0 := by
@@ -74,6 +80,10 @@ info: Try these:
   [apply] rfl
   [apply] grind [= app]
   [apply] grind only [app]
+  [apply] grind =>
+    instantiate only [app]
+    instantiate only [app]
+    instantiate only [app]
 -/
 #guard_msgs (info) in
 example : app [a, b] [c] = [a, b, c] := by
@@ -83,6 +93,7 @@ example : app [a, b] [c] = [a, b, c] := by
 info: Try these:
   [apply] (fun_induction app as bs) <;> grind [= app]
   [apply] (fun_induction app as bs) <;> grind only [app]
+  [apply] (fun_induction app as bs) <;> grind => instantiate only [app]
 -/
 #guard_msgs (info) in
 example : app (app as bs) cs = app as (app bs cs) := by
@@ -100,6 +111,7 @@ example : app (app as bs) cs = app as (app bs cs) := by
 info: Try these:
   [apply] · expose_names; fun_induction app as bs_1 <;> grind [= app]
   [apply] · expose_names; fun_induction app as bs_1 <;> grind only [app]
+  [apply] · expose_names; fun_induction app as bs_1 <;> grind => instantiate only [app]
 -/
 #guard_msgs (info) in
 example : app (app as bs) cs = app as (app bs cs) := by
@@ -110,6 +122,7 @@ example : app (app as bs) cs = app as (app bs cs) := by
 info: Try these:
   [apply] · expose_names; fun_induction app as bs <;> grind [= app]
   [apply] · expose_names; fun_induction app as bs <;> grind only [app]
+  [apply] · expose_names; fun_induction app as bs <;> grind => instantiate only [app]
 -/
 #guard_msgs (info) in
 example : app (app as bs) cs = app as (app bs cs) := by
@@ -153,6 +166,7 @@ def map (f : α → β) : List α → List β
 info: Try these:
   [apply] (fun_induction map f xs) <;> grind [= map]
   [apply] (fun_induction map f xs) <;> grind only [map]
+  [apply] (fun_induction map f xs) <;> grind => instantiate only [map]
 -/
 #guard_msgs (info) in
 theorem map_map (f : α → β) (g : β → γ) xs :
diff --git a/tests/lean/run/try_induction.lean b/tests/lean/run/try_induction.lean
index c6920c05c5..cdcb5dccb2 100644
--- a/tests/lean/run/try_induction.lean
+++ b/tests/lean/run/try_induction.lean
@@ -26,6 +26,10 @@ axiom MyListProp : MyList α → Prop
 info: Try these:
   [apply] (induction xs) <;> grind
   [apply] (induction xs) <;> grind only [mylist_nil, mylist_cons]
+  [apply] ·
+    induction xs
+    · grind => instantiate only [mylist_nil]
+    · grind => instantiate only [mylist_cons]
 -/
 #guard_msgs (info) in
 example (xs : MyList α) : MyListProp xs := by
@@ -47,6 +51,11 @@ axiom ExprProp : Expr → Prop
 info: Try these:
   [apply] (induction e) <;> grind
   [apply] (induction e) <;> grind only [expr_const, expr_add, expr_mul]
+  [apply] ·
+    induction e
+    · grind => instantiate only [expr_const]
+    · grind => instantiate only [expr_add]
+    · grind => instantiate only [expr_mul]
 -/
 #guard_msgs (info) in
 example (e : Expr) : ExprProp e := by
@@ -68,6 +77,7 @@ def add : MyNat → MyNat → MyNat
 info: Try these:
   [apply] (induction n) <;> grind [= add]
   [apply] (induction n) <;> grind only [add]
+  [apply] (induction n) <;> grind => instantiate only [add]
 -/
 #guard_msgs in
 @[grind =]
@@ -78,6 +88,7 @@ theorem add_zero (n : ℕ) : add n .zero = n := by
 info: Try these:
   [apply] (fun_induction add) <;> grind [= add]
   [apply] (fun_induction add) <;> grind only [add]
+  [apply] (fun_induction add) <;> grind => instantiate only [add]
 -/
 #guard_msgs in
 @[grind =]
@@ -97,6 +108,7 @@ attribute [local grind] hyperoperation add
 info: Try these:
   [apply] grind
   [apply] grind only [hyperoperation]
+  [apply] grind => instantiate only [hyperoperation]
 -/
 #guard_msgs in
 @[grind =]
@@ -107,6 +119,7 @@ theorem hyperoperation_zero (m k : ℕ) : hyperoperation .zero m k = .succ k :=
 info: Try these:
   [apply] grind
   [apply] grind only [hyperoperation]
+  [apply] grind => instantiate only [hyperoperation]
 -/
 #guard_msgs in
 @[grind =]
@@ -117,8 +130,14 @@ theorem hyperoperation_recursion (n m k : ℕ) :
 /--
 info: Try these:
   [apply] (induction k) <;> grind
-  [apply] (induction k) <;>
-    grind only [hyperoperation, = add_zero, = hyperoperation_zero, = hyperoperation_recursion, = add_succ]
+  [apply] (induction k) <;> grind only [hyperoperation, = add_zero, = add_succ, = hyperoperation_zero]
+  [apply] ·
+    induction k
+    · grind => instantiate only [hyperoperation, = add_zero]
+    ·
+      grind =>
+        instantiate only [hyperoperation, = add_succ]
+        instantiate only [= hyperoperation_zero]
 -/
 #guard_msgs in
 @[grind =]
diff --git a/tests/lean/run/try_library_suggestions.lean b/tests/lean/run/try_library_suggestions.lean
index 7779901a24..8415523116 100644
--- a/tests/lean/run/try_library_suggestions.lean
+++ b/tests/lean/run/try_library_suggestions.lean
@@ -28,8 +28,9 @@ set_library_suggestions (fun _ _ => pure #[{ name := `special_7, score := 1.0 }]
 
 -- Expected: try? should find grind only [special_7]
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [special_7]
+  [apply] grind => instantiate only [special_7]
 -/
 #guard_msgs in
 example : SpecialProperty 7 := by
@@ -46,8 +47,9 @@ set_library_suggestions (fun _ _ => pure #[{ name := `custom_comm, score := 1.0
 
 -- Expected: try? should find grind only [custom_comm]
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [custom_comm]
+  [apply] grind => instantiate only [custom_comm]
 -/
 #guard_msgs in
 example (a b : Nat) : CustomOp a b = CustomOp b a := by
@@ -55,8 +57,9 @@ example (a b : Nat) : CustomOp a b = CustomOp b a := by
 
 -- Test 4: With a hypothesis that needs library suggestions
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [custom_comm]
+  [apply] grind => instantiate only [custom_comm]
 -/
 #guard_msgs in
 example (a b c : Nat) (h : CustomOp a b = c) : CustomOp b a = c := by
@@ -77,8 +80,9 @@ set_library_suggestions (fun _ _ => pure #[
 
 -- Expected: try? should use the best applicable one
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [prop1_5]
+  [apply] grind => instantiate only [prop1_5]
 -/
 #guard_msgs in
 example : Property1 5 := by