diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index bd339f4a98..30f369fdc3 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -8,15 +8,15 @@ import Init.Tactics
 
 namespace Lean.Parser.Attr
 
-syntax grindEq     := "="
-syntax grindEqBoth := atomic("_" "=" "_")
-syntax grindEqRhs  := atomic("=" "_")
-syntax grindEqBwd  := atomic("←" "=")
-syntax grindBwd    := "←"
-syntax grindFwd    := "→"
-syntax grindUsr    := &"usr"
-syntax grindCases  := &"cases"
-syntax grindCasesEager := atomic(&"cases" &"eager")
+syntax grindEq     := "= "
+syntax grindEqBoth := atomic("_" "=" "_ ")
+syntax grindEqRhs  := atomic("=" "_ ")
+syntax grindEqBwd  := atomic("←" "= ")
+syntax grindBwd    := "← "
+syntax grindFwd    := "→ "
+syntax grindUsr    := &"usr "
+syntax grindCases  := &"cases "
+syntax grindCasesEager := atomic(&"cases" &"eager ")
 
 syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindUsr <|> grindCasesEager <|> grindCases
 
@@ -30,6 +30,8 @@ The configuration for `grind`.
 Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
 -/
 structure Config where
+  /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
+  trace : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
   splits : Nat := 8
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index fa1ce1d6de..d91b03cd06 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Tactics
 import Lean.Meta.Tactic.Grind
+import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Command
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Config
@@ -82,7 +83,7 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
     | _ => throwError "unexpected `grind` parameter{indentD p}"
   return params
 where
-  addEMatchTheorem (params : Grind.Params) (declName : Name) (kind : Grind.TheoremKind) : MetaM Grind.Params := do
+  addEMatchTheorem (params : Grind.Params) (declName : Name) (kind : Grind.EMatchTheoremKind) : MetaM Grind.Params := do
     let info ← getConstInfo declName
     match info with
     | .thmInfo _ =>
@@ -113,11 +114,12 @@ def grind
     (mvarId : MVarId) (config : Grind.Config)
     (only : Bool)
     (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
-    (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
+    (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Grind.Trace := do
   let params ← mkGrindParams config only ps
   let result ← Grind.main mvarId params mainDeclName fallback
   if result.hasFailures then
     throwError "`grind` failed\n{← result.toMessageData}"
+  return result.trace
 
 private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
   let some fallback := fallback? | return (pure ())
@@ -142,26 +144,80 @@ private def evalGrindCore
     (only : Option Syntax)
     (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
     (fallback? : Option Term)
-    (_trace : Bool) -- TODO
-    : TacticM Unit := do
+    (trace : Bool)
+    : TacticM Grind.Trace := do
   let fallback ← elabFallback fallback?
   let only := only.isSome
   let params := if let some params := params then params.getElems else #[]
   logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
   let declName := (← Term.getDeclName?).getD `_grind
-  let config ← elabGrindConfig config
-  withMainContext do liftMetaFinishingTactic (grind · config only params declName fallback)
+  let mut config ← elabGrindConfig config
+  if trace then
+    config := { config with trace }
+  withMainContext do
+    let result ← grind (← getMainGoal) config only params declName fallback
+    replaceMainGoal []
+    return result
+
+private def mkGrindOnly
+    (config : TSyntax `Lean.Parser.Tactic.optConfig)
+    (fallback? : Option Term)
+    (trace : Grind.Trace)
+    : MetaM (TSyntax `tactic) := do
+  let mut params := #[]
+  let mut foundFns : NameSet := {}
+  for { origin, kind } in trace.thms.toList do
+    if let .decl declName := origin then
+      unless Match.isMatchEqnTheorem (← getEnv) declName do
+        if let some declName ← isEqnThm? declName then
+          unless foundFns.contains declName do
+            foundFns := foundFns.insert declName
+            let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+            let param ← `(Parser.Tactic.grindParam| $decl:ident)
+            params := params.push param
+        else
+          let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+          let param ← match kind with
+            | .eqLhs   => `(Parser.Tactic.grindParam| = $decl)
+            | .eqRhs   => `(Parser.Tactic.grindParam| =_ $decl)
+            | .eqBoth  => `(Parser.Tactic.grindParam| _=_ $decl)
+            | .eqBwd   => `(Parser.Tactic.grindParam| ←= $decl)
+            | .bwd     => `(Parser.Tactic.grindParam| ← $decl)
+            | .fwd     => `(Parser.Tactic.grindParam| → $decl)
+            | .user    => `(Parser.Tactic.grindParam| usr $decl)
+            | .default => `(Parser.Tactic.grindParam| $decl:ident)
+          params := params.push param
+  for declName in trace.eagerCases.toList do
+    let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+    let param ← `(Parser.Tactic.grindParam| cases eager $decl)
+    params := params.push param
+  for declName in trace.cases.toList do
+    unless trace.eagerCases.contains declName do
+      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+      let param ← `(Parser.Tactic.grindParam| cases $decl)
+      params := params.push param
+  let result ← if let some fallback := fallback? then
+    `(tactic| grind $config:optConfig only on_failure $fallback)
+  else
+    `(tactic| grind $config:optConfig only)
+  if params.isEmpty then
+    return result
+  else
+    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
+    return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩
 
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
   match stx with
   | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    evalGrindCore stx config only params fallback? false
+    discard <| evalGrindCore stx config only params fallback? false
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind? $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    evalGrindCore stx config only params fallback? true
+  | `(tactic| grind?%$tk $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    let trace ← evalGrindCore stx config only params fallback? true
+    let stx ← mkGrindOnly config fallback? trace
+    Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index 8f354bf8aa..8dea070be4 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -33,6 +33,7 @@ namespace Lean
 
 /-! Trace options for `grind` users -/
 builtin_initialize registerTraceClass `grind
+builtin_initialize registerTraceClass `grind.trace
 builtin_initialize registerTraceClass `grind.assert
 builtin_initialize registerTraceClass `grind.eqc
 builtin_initialize registerTraceClass `grind.internalize
diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean
index ee9f06501b..8572d7d57e 100644
--- a/src/Lean/Meta/Tactic/Grind/Attr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Attr.lean
@@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Grind.Cases
 namespace Lean.Meta.Grind
 
 inductive AttrKind where
-  | ematch (k : TheoremKind)
+  | ematch (k : EMatchTheoremKind)
   | cases (eager : Bool)
   | infer
 
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 925f5180b4..d7dcc1f982 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -242,17 +242,17 @@ private def annotateMatchEqnType (prop : Expr) (initApp : Expr) : M Expr := do
 Stores new theorem instance in the state.
 Recall that new instances are internalized later, after a full round of ematching.
 -/
-private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) : M Unit := do
+private def addNewInstance (thm : EMatchTheorem) (proof : Expr) (generation : Nat) : M Unit := do
   let proof ← instantiateMVars proof
   if grind.debug.proofs.get (← getOptions) then
     check proof
   let mut prop ← inferType proof
-  if Match.isMatchEqnTheorem (← getEnv) origin.key then
+  if Match.isMatchEqnTheorem (← getEnv) thm.origin.key then
     prop ← annotateMatchEqnType prop (← read).initApp
-  else if (← isEqnThm origin.key) then
+  else if (← isEqnThm thm.origin.key) then
     prop ← annotateEqnTypeConds prop
-  trace_goal[grind.ematch.instance] "{← origin.pp}: {prop}"
-  addTheoremInstance proof prop (generation+1)
+  trace_goal[grind.ematch.instance] "{← thm.origin.pp}: {prop}"
+  addTheoremInstance thm proof prop (generation+1)
 
 /--
 After processing a (multi-)pattern, use the choice assignment to instantiate the proof.
@@ -301,13 +301,13 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
-    addNewInstance thm.origin proof c.gen
+    addNewInstance thm proof c.gen
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
       reportIssue m!"failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
-    addNewInstance thm.origin proof c.gen
+    addNewInstance thm proof c.gen
 
 /-- Process choice stack until we don't have more choices to be processed. -/
 private def processChoices : M Unit := do
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index de7334bd99..639351c272 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -92,11 +92,11 @@ instance : BEq Origin where
 instance : Hashable Origin where
   hash a := hash a.key
 
-inductive TheoremKind where
+inductive EMatchTheoremKind where
   | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | default | user /- pattern specified using `grind_pattern` command -/
-  deriving Inhabited, BEq, Repr
+  deriving Inhabited, BEq, Repr, Hashable
 
-private def TheoremKind.toAttribute : TheoremKind → String
+private def EMatchTheoremKind.toAttribute : EMatchTheoremKind → String
   | .eqLhs   => "[grind =]"
   | .eqRhs   => "[grind =_]"
   | .eqBoth  => "[grind _=_]"
@@ -106,7 +106,7 @@ private def TheoremKind.toAttribute : TheoremKind → String
   | .default => "[grind]"
   | .user    => "[grind]"
 
-private def TheoremKind.explainFailure : TheoremKind → String
+private def EMatchTheoremKind.explainFailure : EMatchTheoremKind → String
   | .eqLhs   => "failed to find pattern in the left-hand side of the theorem's conclusion"
   | .eqRhs   => "failed to find pattern in the right-hand side of the theorem's conclusion"
   | .eqBoth  => unreachable! -- eqBoth is a macro
@@ -131,7 +131,7 @@ structure EMatchTheorem where
   symbols     : List HeadIndex
   origin      : Origin
   /-- The `kind` is used for generating the `patterns`. We save it here to implement `grind?`. -/
-  kind        : TheoremKind
+  kind        : EMatchTheoremKind
   deriving Inhabited
 
 /-- Set of E-matching theorems. -/
@@ -534,7 +534,7 @@ private def ppParamsAt (proof : Expr) (numParams : Nat) (paramPos : List Nat) :
 Creates an E-matching theorem for a theorem with proof `proof`, `numParams` parameters, and the given set of patterns.
 Pattern variables are represented using de Bruijn indices.
 -/
-def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : TheoremKind): MetaM EMatchTheorem := do
+def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM EMatchTheorem := do
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
   if symbols.isEmpty then
     throwError "invalid pattern for `{← origin.pp}`{indentD (patterns.map ppPattern)}\nthe pattern does not contain constant symbols for indexing"
@@ -557,7 +557,7 @@ private def getProofFor (declName : Name) : CoreM Expr := do
 Creates an E-matching theorem for `declName` with `numParams` parameters, and the given set of patterns.
 Pattern variables are represented using de Bruijn indices.
 -/
-def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : TheoremKind) : MetaM EMatchTheorem := do
+def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM EMatchTheorem := do
   mkEMatchTheoremCore (.decl declName) #[] numParams (← getProofFor declName) patterns kind
 
 /--
@@ -602,7 +602,7 @@ def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Boo
 Adds an E-matching theorem to the environment.
 See `mkEMatchTheorem`.
 -/
-def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : TheoremKind) : MetaM Unit := do
+def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM Unit := do
   ematchTheoremsExt.add (← mkEMatchTheorem declName numParams patterns kind)
 
 /--
@@ -696,7 +696,7 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
     | return none
   return some (ps, s.symbols.toList)
 
-def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
     return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true))
   else if kind == .eqRhs then
@@ -726,7 +726,7 @@ where
       levelParams, origin, kind
     }
 
-def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do
+def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) : MetaM EMatchTheorem := do
   let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
     | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
   return thm
@@ -736,7 +736,7 @@ def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchThe
   eqns.mapM fun eqn => do
     mkEMatchEqTheorem eqn (normalizePattern := true)
 
-private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do
+private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (useLhs := true) : MetaM Unit := do
   if (← getConstInfo declName).isTheorem then
     ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind
   else if let some thms ← mkEMatchEqTheoremsForDef? declName then
@@ -763,7 +763,7 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat
       throwErr
     return s.erase <| .decl declName
 
-def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do
+def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) : MetaM Unit := do
   if thmKind == .eqLhs then
     addGrindEqAttr declName attrKind thmKind (useLhs := true)
   else if thmKind == .eqRhs then
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index 0482985432..dcdaea8f59 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -53,7 +53,7 @@ private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
   return some fvarId
 
 /-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/
-private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
+private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : EMatchTheoremKind) : MetaM (Option EMatchTheorem) := do
   try
     mkEMatchTheoremWithKind? origin #[] proof kind
   catch _ =>
diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean
index 5617f7f391..fcb5632610 100644
--- a/src/Lean/Meta/Tactic/Grind/Intro.lean
+++ b/src/Lean/Meta/Tactic/Grind/Intro.lean
@@ -74,12 +74,15 @@ private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := d
   else
     return .done
 
-def isEagerCasesCandidate (goal : Goal) (type : Expr) : Bool := Id.run do
+private def isEagerCasesCandidate (goal : Goal) (type : Expr) : Bool := Id.run do
   let .const declName _ := type.getAppFn | return false
   return goal.casesTypes.isEagerSplit declName
 
-private def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do
-  if isEagerCasesCandidate goal (← fvarId.getType) then
+private def applyCases? (goal : Goal) (fvarId : FVarId) : GrindM (Option (List Goal)) := goal.mvarId.withContext do
+  let type ← whnfD (← fvarId.getType)
+  if isEagerCasesCandidate goal type then
+    if let .const declName _ := type.getAppFn then
+      saveCases declName true
     let mvarIds ← cases goal.mvarId (mkFVar fvarId)
     return mvarIds.map fun mvarId => { goal with mvarId }
   else
diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean
index 8f5251d581..8057092d44 100644
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@@ -93,6 +93,7 @@ structure Result where
   skipped  : List Goal
   issues   : List MessageData
   config   : Grind.Config
+  trace    : Trace
 
 def Result.hasFailures (r : Result) : Bool :=
   !r.failures.isEmpty
@@ -113,7 +114,8 @@ def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : F
     let (failures, skipped) ← solve goals fallback
     trace[grind.debug.final] "{← ppGoals goals}"
     let issues := (← get).issues
-    return { failures, skipped, issues, config := params.config }
+    let trace := (← get).trace
+    return { failures, skipped, issues, config := params.config, trace }
   go.run mainDeclName params fallback
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index 2931e1941e..8cd91ece0e 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -190,6 +190,9 @@ def splitNext : GrindTactic := fun goal => do
       casesMatch (← get).mvarId c
     else
       let major ← mkCasesMajor c
+      if (← getConfig).trace then
+        if let .const declName _ := (← whnfD (← inferType major)).getAppFn then
+          saveCases declName false
       cases (← get).mvarId major
     let goal ← get
     let goals := mvarIds.map fun mvarId => { goal with mvarId }
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 6aeddb164a..e9122c1189 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -65,6 +65,23 @@ instance : BEq CongrTheoremCacheKey where
 instance : Hashable CongrTheoremCacheKey where
   hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs)
 
+structure EMatchTheoremTrace where
+  origin : Origin
+  kind   : EMatchTheoremKind
+  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.
+-/
+structure Trace where
+  thms       : PHashSet EMatchTheoremTrace := {}
+  eagerCases : PHashSet Name := {}
+  cases      : PHashSet Name := {}
+  deriving Inhabited
+
 /-- State for the `GrindM` monad. -/
 structure State where
   /-- `ShareCommon` (aka `Hashconsing`) state. -/
@@ -91,6 +108,8 @@ structure State where
   users when `grind` fails.
   -/
   issues     : List MessageData := []
+  /-- `trace` for `grind?` -/
+  trace      : Trace := {}
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 private def MethodsRef : Type := MethodsRefPointed.type
@@ -117,6 +136,17 @@ def getNatZeroExpr : GrindM Expr := do
 def getMainDeclName : GrindM Name :=
   return (← readThe Context).mainDeclName
 
+def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
+  if (← getConfig).trace then
+    modify fun s => { s with trace.thms := s.trace.thms.insert { origin := thm.origin, kind := thm.kind } }
+
+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 }
+
 @[inline] def getMethodsRef : GrindM MethodsRef :=
   read
 
@@ -138,9 +168,9 @@ Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
 been hash-consed. We perform this step before we internalize expressions.
 -/
 def shareCommon (e : Expr) : GrindM Expr := do
-  modifyGet fun { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues } =>
+  modifyGet fun { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues, trace } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues })
+    (e, { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues, trace })
 
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=
@@ -458,7 +488,8 @@ def addNewFact (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := d
   modify fun s => { s with newFacts := s.newFacts.enqueue { proof, prop, generation } }
 
 /-- Adds a new theorem instance produced using E-matching. -/
-def addTheoremInstance (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
+def addTheoremInstance (thm : EMatchTheorem) (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
+  saveEMatchTheorem thm
   addNewFact proof prop generation
   modify fun s => { s with numInstances := s.numInstances + 1 }
 
diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean
new file mode 100644
index 0000000000..a701b4149c
--- /dev/null
+++ b/tests/lean/run/grind_trace.lean
@@ -0,0 +1,81 @@
+attribute [grind =] List.length_cons
+attribute [grind →] List.getElem?_eq_getElem
+attribute [grind =] List.length_replicate
+attribute [grind =] List.getElem_replicate
+attribute [grind =] List.getElem?_eq_none
+attribute [grind =] List.getElem?_eq_some_iff
+attribute [grind =] getElem!_pos
+
+attribute [grind =] Option.map_some' Option.map_none'
+attribute [grind =] List.getElem?_map
+attribute [grind =] List.getElem?_replicate
+
+attribute [grind =] List.getLast?_eq_some_iff
+attribute [grind] List.mem_concat_self
+
+attribute [grind =] List.getElem_cons_zero in
+attribute [grind =] List.getElem?_cons_zero in
+
+/--
+info: Try this: grind only [= List.getElem?_replicate, = List.getElem?_eq_none]
+-/
+#guard_msgs (info) in
+theorem getElem?_replicate' : (List.replicate n a)[m]? = if m < n then some a else none := by
+  grind?
+
+/--
+info: Try this: grind only [= List.length_cons]
+-/
+#guard_msgs (info) in
+example : 0 < (x :: t).length := by
+  grind?
+
+/--
+info: Try this: grind only [= List.getElem?_replicate, = List.getElem?_eq_some_iff, = List.getElem?_map, =
+  List.getElem_replicate, = List.getElem?_eq_none, = Option.map_some', = Option.map_none', = List.length_replicate, →
+  List.getElem?_eq_getElem, cases And, cases Or, cases Exists]
+-/
+#guard_msgs (info) in
+theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) := by
+  grind?
+
+/--
+info: Try this: grind only [= List.getLast?_eq_some_iff, List.mem_concat_self, cases Exists]
+-/
+#guard_msgs (info) in
+theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
+  grind?
+
+def f : Nat → Nat
+  | 0 => 1
+  | _ => 2
+
+/--
+info: Try this: grind only
+-/
+#guard_msgs (info) in
+example : x = 0 → f x = 1 := by
+  unfold f
+  grind? -- should not include match equations
+
+attribute [grind] f
+
+/--
+info: Try this: grind only [f]
+-/
+#guard_msgs (info) in
+example : x = 0 → f x = 1 := by
+  grind? [f]
+
+opaque g : Nat → Nat
+
+theorem gthm : g (g x) = g x := sorry
+
+grind_pattern gthm => g (g x)
+
+/--
+info: Try this: grind only [usr gthm]
+-/
+#guard_msgs (info) in
+example : g (g (g x)) = g x := by
+  grind?