diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index 3c9571dafa..ea442bb0c9 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -100,6 +100,9 @@ syntax (name := done) "done" : grind
 /-- `finish` tries to close the current goal using `grind`'s default strategy -/
 syntax (name := finish) "finish" : grind
 
+/-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script. -/
+syntax (name := finishTrace) "finish?" : grind
+
 syntax (name := «have») "have" letDecl : grind
 
 /-- Executes the given tactic block to close the current goal. -/
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index d0e403e847..973cd14519 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -10,3 +10,4 @@ public import Lean.Elab.Tactic.Grind.Basic
 public import Lean.Elab.Tactic.Grind.BuiltinTactic
 public import Lean.Elab.Tactic.Grind.ShowState
 public import Lean.Elab.Tactic.Grind.Have
+public import Lean.Elab.Tactic.Grind.Trace
diff --git a/src/Lean/Elab/Tactic/Grind/Trace.lean b/src/Lean/Elab/Tactic/Grind/Trace.lean
new file mode 100644
index 0000000000..022cb2ce02
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Grind/Trace.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Elab.Tactic.Grind.Basic
+import Init.Grind.Interactive
+import Lean.Meta.Tactic.TryThis
+import Lean.Meta.Tactic.Grind.Action
+import Lean.Meta.Tactic.Grind.EMatchAction
+import Lean.Meta.Tactic.Grind.Split
+namespace Lean.Elab.Tactic.Grind
+open Meta
+open Meta.Grind
+
+def withTracing (x : GrindTacticM α) : GrindTacticM α := do
+  withReader (fun ctx => { ctx with ctx.config.trace := true }) x
+
+def mkFinish (maxIterations : Nat) : IO Action := do
+  let solvers ← Solvers.mkAction
+  return Action.checkTactic >> (Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext).loop maxIterations
+
+def maxIterations := 1000 -- **TODO**: Add option
+
+@[builtin_grind_tactic finishTrace] def evalFinishTrace : GrindTactic := fun stx => do
+  let a ← mkFinish maxIterations
+  let goal ← getMainGoal
+  withTracing do
+  match (← liftGrindM <| a.run goal) with
+  | .closed seq =>
+    replaceMainGoal []
+    let seq := Action.mkGrindSeq seq
+    Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax seq }
+  | .stuck gs =>
+    let goal :: _ := gs | throwError "`finish?` failed, but resulting goal is not available"
+    let params := (← read).params
+    let result ← liftGrindM do mkResult params (some goal)
+    throwError "`finish?` failed\n{← result.toMessageData}"
+
+end Lean.Elab.Tactic.Grind
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index d1dbda90cd..e4ebaa386d 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -43,9 +43,8 @@ public import Lean.Meta.Tactic.Grind.PropagateInj
 public import Lean.Meta.Tactic.Grind.Order
 public import Lean.Meta.Tactic.Grind.Anchor
 public import Lean.Meta.Tactic.Grind.Action
-
+public import Lean.Meta.Tactic.Grind.EMatchAction
 public section
-
 namespace Lean
 
 /-! Trace options for `grind` users -/
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
new file mode 100644
index 0000000000..64be0ae696
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Action
+public import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.EMatch
+public section
+namespace Lean.Meta.Grind.Action
+
+def instantiate' : Action := fun goal kna kp => do
+  let (progress, goal') ← GoalM.run goal ematch
+  -- **TODO**: filter relevant instances
+  if progress then
+    concatTactic (← kp goal') `(grind| instantiate)
+  else
+    kna goal
+
+def instantiate : Action :=
+  instantiate' >> assertAll
+
+end Lean.Meta.Grind.Action
diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
new file mode 100644
index 0000000000..cbfed722cc
--- /dev/null
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -0,0 +1,62 @@
+open Lean Grind
+
+/--
+info: Try this:
+  [apply] cases #c4b6 <;> ring <;> cases #4c68 <;> ring
+-/
+#guard_msgs in
+example {α : Type} [CommRing α] (a b c d e : α) :
+    (a * a = b * c ∨ a^2 = c * b) →
+    (a^2 = c * b ∨ e^2 = d * c) →
+    (b^2 = d*c ∨ b^2 = c*d) →
+    a*b*(b*a) = c^2*b*d := by
+ grind => finish?
+
+
+/--
+info: Try this:
+  [apply] ⏎
+    cases #b0f4
+    next => cases #50fc
+    next => cases #50fc <;> lia
+-/
+#guard_msgs in
+example (p : Nat → Prop) (x y z w : Int) :
+    (x = 1 ∨ x = 2) →
+    (w = 1 ∨ w = 4) →
+    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
+    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
+  grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    ac
+    cases #5c4b <;> cases #896f <;> ac
+-/
+#guard_msgs in
+example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d e : α) :
+    (op a a = op b c ∨ op a a = op c b) →
+    (op a a = op c b ∨ op e e = op d c) →
+    (op b b = op d c ∨ op b b = op c d) →
+    op (op a b) (op b a) = op (op c c) (op b d) := by
+  grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    instantiate
+    instantiate
+-/
+#guard_msgs in
+example (as bs cs : Array α) (v₁ v₂ : α)
+        (i₁ i₂ j : Nat)
+        (h₁ : i₁ < as.size)
+        (h₂ : bs = as.set i₁ v₁)
+        (h₃ : i₂ < bs.size)
+        (h₃ : cs = bs.set i₂ v₂)
+        (h₄ : i₁ ≠ j ∧ i₂ ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind => finish?