diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index ea442bb0c944..c9addf969e3e 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -66,8 +66,12 @@ syntax (name := «sorry») "sorry" : grind
 syntax anchor := "#" noWs hexnum
 syntax thm := anchor <|> grindLemma <|> grindLemmaMin
 
-/-- Instantiates theorems using E-matching. -/
-syntax (name := instantiate) "instantiate" (colGt thm),* : grind
+/--
+Instantiates theorems using E-matching.
+The `approx` modifier is just a marker for users to easily identify automatically generated `instantiate` tactics
+that may have redundant arguments.
+-/
+syntax (name := instantiate) "instantiate" (&" only")? (&" approx")? (" [" withoutPosition(thm,*,?) "]")? : grind
 
 -- **Note**: Should we rename the following tactics to `trace_`?
 /-- Shows asserted facts. -/
diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean
index d1825c59c811..2885f6a1d420 100644
--- a/src/Lean/Elab/Tactic/Grind/Basic.lean
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@@ -354,7 +354,7 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS
     -- **Note**: we discard changes to `Term.State`
     let (subgoals, grindState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do
       let (_, s) ← GrindTacticM.run
-            (ctx := { methods, ctx := grindCtx, params, elaborator })
+            (ctx := { recover := false, methods, ctx := grindCtx, params, elaborator })
             (s := { state := grindState, goals := [goal] }) do
         evalGrindTactic stx.raw
         pruneSolvedGoals
diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index e81c8feec140..e81ecb47679f 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -123,8 +123,8 @@ def logTheoremAnchor (proof : Expr) : TermElabM Unit := do
   let stx ← getRef
   Term.addTermInfo' stx proof
 
-def ematchThms (thms : Array EMatchTheorem) : GrindTacticM Unit := do
-  let progress ← liftGoalM <| if thms.isEmpty then ematch else ematchTheorems thms
+def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit := do
+  let progress ← liftGoalM <| if only then ematchOnly thms else ematch thms
   unless progress do
     throwError "`instantiate` tactic failed to instantiate new facts, use `show_patterns` to see active theorems and their patterns."
   let goal ← getMainGoal
@@ -142,15 +142,19 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
   return (numDigits, val)
 
 @[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do
-  let `(grind| instantiate $[$thmRefs:thm],*) := stx | throwUnsupportedSyntax
-  let mut thms := #[]
-  for thmRef in thmRefs do
-    match thmRef with
-    | `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
-    | `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
-    | `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)
-    | _ => throwErrorAt thmRef "unexpected theorem reference"
-  ematchThms thms
+  let `(grind| instantiate $[ only%$only ]? $[ approx ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax
+  let goal ← getMainGoal
+  let only := only.isSome
+  let initThms ← if only then goal.getActiveMatchEqTheorems else pure #[]
+  let mut thms := initThms
+  if let some thmRefs := thmRefs? then
+    for thmRef in thmRefs do
+      match thmRef with
+      | `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
+      | `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
+      | `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)
+      | _ => throwErrorAt thmRef "unexpected theorem reference"
+  ematchThms only thms
 where
   collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do
     let mut found : Std.HashSet Expr := {}
diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index d8c7fa4c8a87..ed3d57cef9c7 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -10,6 +10,7 @@ public import Lean.Meta.Tactic.TryThis
 public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Config
 import Lean.Meta.Tactic.Grind.SimpUtil
+import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.MutualDef
 meta import Lean.Meta.Tactic.Grind.Parser
@@ -292,37 +293,13 @@ def mkGrindOnly
   let mut foundFns : NameSet := {}
   for { origin, kind, minIndexable } in trace.thms.toList do
     if let .decl declName := origin then
-      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)
+      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 decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-        let param ← match kind, minIndexable with
-          | .eqLhs false,   _     => `(Parser.Tactic.grindParam| = $decl:ident)
-          | .eqLhs true,    _     => `(Parser.Tactic.grindParam| = gen $decl:ident)
-          | .eqRhs false,   _     => `(Parser.Tactic.grindParam| =_ $decl:ident)
-          | .eqRhs true,    _     => `(Parser.Tactic.grindParam| =_ gen $decl:ident)
-          | .eqBoth false,  _     => `(Parser.Tactic.grindParam| _=_ $decl:ident)
-          | .eqBoth true,   _     => `(Parser.Tactic.grindParam| _=_ gen $decl:ident)
-          | .eqBwd,         _     => `(Parser.Tactic.grindParam| ←= $decl:ident)
-          | .user,          _     => `(Parser.Tactic.grindParam| usr $decl:ident)
-          | .bwd false,     false => `(Parser.Tactic.grindParam| ← $decl:ident)
-          | .bwd true,      false => `(Parser.Tactic.grindParam| ← gen $decl:ident)
-          | .fwd,           false => `(Parser.Tactic.grindParam| → $decl:ident)
-          | .leftRight,     false => `(Parser.Tactic.grindParam| => $decl:ident)
-          | .rightLeft,     false => `(Parser.Tactic.grindParam| <= $decl:ident)
-          | .default false, false => `(Parser.Tactic.grindParam| $decl:ident)
-          | .default true,  false => `(Parser.Tactic.grindParam| gen $decl:ident)
-          | .bwd false,     true  => `(Parser.Tactic.grindParam| ! ← $decl:ident)
-          | .bwd true,      true  => `(Parser.Tactic.grindParam| ! ← gen $decl:ident)
-          | .fwd,           true  => `(Parser.Tactic.grindParam| ! → $decl:ident)
-          | .leftRight,     true  => `(Parser.Tactic.grindParam| ! => $decl:ident)
-          | .rightLeft,     true  => `(Parser.Tactic.grindParam| ! <= $decl:ident)
-          | .default false, true  => `(Parser.Tactic.grindParam| ! $decl:ident)
-          | .default true,  true  => `(Parser.Tactic.grindParam| ! gen $decl:ident)
+        let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
   for declName in trace.eagerCases.toList do
     unless Grind.isBuiltinEagerCases declName do
diff --git a/src/Lean/Elab/Tactic/Grind/ShowState.lean b/src/Lean/Elab/Tactic/Grind/ShowState.lean
index 526114944ca1..efef401ed43f 100644
--- a/src/Lean/Elab/Tactic/Grind/ShowState.lean
+++ b/src/Lean/Elab/Tactic/Grind/ShowState.lean
@@ -8,6 +8,7 @@ prelude
 public import Lean.Elab.Tactic.Grind.Basic
 public import Lean.Elab.Tactic.Grind.Filter
 import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.Split
 namespace Lean.Elab.Tactic.Grind
@@ -118,30 +119,11 @@ public def showState (filter : Filter) (isSilent := false) : GrindTacticM Unit :
 
 @[builtin_grind_tactic showLocalThms] def evalShowLocalThms : GrindTactic := fun _ => withMainContext do
   let goal ← getMainGoal
-  let entries ← liftGrindM do
-    let (found, entries) ← go {} {} goal.ematch.thms
-    let (_, entries) ← go found entries goal.ematch.newThms
-    pure entries
+  let entries ← liftGrindM <| getLocalTheoremAnchors goal
   let numDigits := getNumDigitsForAnchors entries
   let msgs := entries.map fun { anchor, e } =>
     .trace { cls := `thm } m!"#{anchorToString numDigits anchor} := {e}" #[]
   let msg := MessageData.trace { cls := `thms, collapsed := false } "Local theorems" msgs
   logInfo msg
-where
-  go (found : Std.HashSet Grind.Origin) (result : Array ExprWithAnchor) (thms : PArray EMatchTheorem)
-      : GrindM (Std.HashSet Grind.Origin × Array ExprWithAnchor) := do
-    let mut found := found
-    let mut result := result
-    for thm in thms do
-      -- **Note**: We only display local theorems
-      if thm.origin matches .local _ | .fvar _ then
-      unless found.contains thm.origin do
-        found := found.insert thm.origin
-        let type ← inferType thm.proof
-        -- **Note**: Evaluate how stable these anchors are.
-        let anchor ← getAnchor type
-        result := result.push { anchor, e := type }
-        pure ()
-    return (found, result)
 
 end Lean.Elab.Tactic.Grind
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index e4ebaa386de2..efc7f6595227 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -43,6 +43,7 @@ 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.EMatchTheoremParam
 public import Lean.Meta.Tactic.Grind.EMatchAction
 public section
 namespace Lean
diff --git a/src/Lean/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean
index 574b51cf0236..26d9f745ca76 100644
--- a/src/Lean/Meta/Tactic/Grind/Action.lean
+++ b/src/Lean/Meta/Tactic/Grind/Action.lean
@@ -163,6 +163,20 @@ def mkGrindNext (s : List TGrind) : CoreM TGrind := do
   let s := mkGrindSeq s
   `(grind| next => $s:grindSeq)
 
+/--
+Given `[t₁, ..., tₙ]`, returns
+```
+(t₁
+ ...
+ tₙ)
+```
+If the list is empty, it returns `(skip)`.
+-/
+private def mkGrindParen (s : List TGrind) : CoreM TGrind := do
+  let s ← if s == [] then pure [← `(grind| skip)] else pure s
+  let s := mkGrindSeq s
+  `(grind| ($s:grindSeq))
+
 /--
 If tracing is enabled and continuation produced `.closed [t₁, ..., tₙ]`,
 returns the singleton sequence `[t]` where `t` is
@@ -251,21 +265,39 @@ def solverAction (check : GoalM CheckResult) (mkTac : GrindM (TSyntax `grind)) :
       concatTactic (← kp goal') mkTac
   | .closed     => closeWith mkTac
 
+def saveStateIfTracing : GrindM (Option SavedState) := do
+  if (← getConfig).trace then
+    return some (← saveState)
+  else
+    return none
+/--
+Returns `true` if the tactic sequence `seq` closes `goal` starting at saved state `s?`.
+If `s?` is `none` just returns `true`.
+-/
+def checkSeqAt (s? : Option SavedState) (goal : Goal) (seq : List TGrind) : GrindM Bool := do
+  let some s := s? | return true
+  let tac ← mkGrindParen seq
+  Lean.withoutModifyingState do
+    s.restore
+    -- **Note**: Ensure tracing is disabled.
+    withTheReader Grind.Context (fun ctx => { ctx with config.trace := false }) do
+      try
+        let subgoals ← evalTactic goal tac
+        return subgoals.isEmpty
+      catch _  =>
+        return false
+
 /--
 Helper action that checks whether the resulting tactic script produced by its continuation
 can close the original goal.
 -/
 def checkTactic : Action := fun goal _ kp => do
-  let s ← saveState
+  let s ← saveStateIfTracing
   let r ← kp goal
   match r with
   | .closed seq =>
-    let tac ← mkGrindNext seq
-    Lean.withoutModifyingState do
-      s.restore
-      let subgoals ← evalTactic goal tac
-      unless subgoals.isEmpty do
-        throwError "generated tactic cannot close the goal{indentD tac}\nInitial goal\n{goal.mvarId}\nPending subgoals\n{subgoals.map (·.mvarId)}"
+    unless (← checkSeqAt s goal seq) do
+      throwError "generated tactic cannot close the goal{indentD (← mkGrindNext seq)}\nInitial goal\n{goal.mvarId}"
     return r
   | _ => return r
 
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index eb8b4abdb5a1..bbeadcde3307 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -67,10 +67,34 @@ structure Context where
   initApp : Expr := default
   deriving Inhabited
 
+/--
+A mapping `uniqueId ↦ thm`, where `uniqueId` is an auxiliary marker used to wrap a theorem instantiation proof of `thm`
+using a `Expr.mdata`. The `uniqueId`s are created using `mkFreshId`.
+-/
+abbrev InstanceMap := Std.HashMap Name EMatchTheorem
+
+private def thmInstanceKey := `_grind_thm_instance
+
+private def markTheoremInstanceProof (proof : Expr) (uniqueId : Name) : Expr :=
+  Expr.mdata (KVMap.empty.insert thmInstanceKey uniqueId) proof
+
+/-- Returns `some uniqueId` if `proof` was marked using `markTheoremInstanceProof` -/
+def isTheoremInstanceProof? (proof : Expr) : Option Name :=
+  match proof with
+  | .mdata d _ =>
+    match d.find thmInstanceKey with
+    | some (DataValue.ofName uniqueId) => some uniqueId
+    | _ => none
+  | _ => none
+
 /-- State for the E-matching monad -/
 structure SearchState where
   /-- Choices that still have to be processed. -/
   choiceStack  : List Choice := []
+  /--
+  When tracing is enabled track instances here. See comment at `InstanceMap`
+  -/
+  instanceMap : InstanceMap := {}
   deriving Inhabited
 
 abbrev M := ReaderT Context $ StateRefT SearchState GoalM
@@ -78,6 +102,9 @@ abbrev M := ReaderT Context $ StateRefT SearchState GoalM
 def M.run' (x : M α) : GoalM α :=
   x {} |>.run' {}
 
+def M.run (x : M α) : GoalM (α × SearchState) :=
+  x {} |>.run {}
+
 @[inline] private abbrev withInitApp (e : Expr) (x : M α) : M α :=
   withReader (fun ctx => { ctx with initApp := e }) x
 
@@ -453,6 +480,10 @@ where
   go (proof prop : Expr) : M Unit := do
     let mut proof := proof
     let mut prop := prop
+    if (← getConfig).trace then
+      let uniqueId ← mkFreshId
+      proof := markTheoremInstanceProof proof uniqueId
+      modify fun s => { s with instanceMap := s.instanceMap.insert uniqueId thm }
     if (← isMatchEqLikeDeclName thm.origin.key) then
       prop ← annotateMatchEqnType prop (← read).initApp
       -- We must add a hint here because `annotateMatchEqnType` introduces `simpMatchDiscrsOnly` and
@@ -706,29 +737,41 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-private def ematchCore : GoalM Unit := do profileitM Exception "grind ematch" (← getOptions) do
+private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceMap := do profileitM Exception "grind ematch" (← getOptions) do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
-    withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
+    withReader (fun ctx => { ctx with useMT := false }) do
+      ematchTheorems newThms
+      extraThms.forM ematchTheorem
   if (← checkMaxInstancesExceeded <||> checkMaxEmatchExceeded) then
-    return ()
+    return {}
   else
-    go (← get).ematch.thms (← get).ematch.newThms |>.run'
+    let (_, s) ← go (← get).ematch.thms (← get).ematch.newThms |>.run
     modify fun s => { s with
       ematch.thms      := s.ematch.thms ++ s.ematch.newThms
       ematch.newThms   := {}
       ematch.gmt       := s.ematch.gmt + 1
       ematch.num       := s.ematch.num + 1
     }
+    return s.instanceMap
 
-/-- Performs one round of E-matching, and returns `true` if new instances were generated. -/
-def ematch : GoalM Bool := do
+/--
+Performs one round of E-matching, and returns `true` if new instances were generated.
+Recall that the mapping is nonempty only if tracing is enabled.
+-/
+def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceMap) := do
   let numInstances := (← get).ematch.numInstances
-  ematchCore
-  return (← get).ematch.numInstances != numInstances
+  let map ← ematchCore extraThms
+  return ((← get).ematch.numInstances != numInstances, map)
+
+/--
+Performs one round of E-matching, and returns `true` if new instances were generated.
+-/
+def ematch (extraThms : Array EMatchTheorem := #[]) : GoalM Bool :=
+  return (← ematch' extraThms).1
 
 /-- Performs one round of E-matching using the giving theorems, and returns `true` if new instances were generated. -/
-def ematchTheorems (thms : Array EMatchTheorem) : GoalM Bool := do
+def ematchOnly (thms : Array EMatchTheorem) : GoalM Bool := do
   let numInstances := (← get).ematch.numInstances
   go |>.run'
   return (← get).ematch.numInstances != numInstances
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
index 64be0ae69653..fe4cdb23b723 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -8,18 +8,106 @@ prelude
 public import Lean.Meta.Tactic.Grind.Action
 public import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
-public section
+import Lean.Meta.Tactic.Grind.EMatchTheoremParam
+import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
 namespace Lean.Meta.Grind.Action
 
-def instantiate' : Action := fun goal kna kp => do
-  let (progress, goal') ← GoalM.run goal ematch
-  -- **TODO**: filter relevant instances
+structure CollectState where
+  visited       : Std.HashSet ExprPtr := {}
+  collectedThms : Std.HashSet (Origin × EMatchTheoremKind) := {}
+  thms          : Array EMatchTheorem := #[]
+
+def collect (e : Expr) (map : EMatch.InstanceMap) : Array EMatchTheorem :=
+  let (_, s) := go e |>.run {}
+  s.thms
+where
+  go (e : Expr) : StateM CollectState Unit := do
+    if isMarkedSubsingletonApp e then
+      /-
+      **Note**: We can ignore nested proofs and decidable instances.
+      They are not part of current `grind` proof.
+      -/
+      return ()
+    if (← get).visited.contains { expr := e } then
+      return ()
+    modify fun s => { s with visited := s.visited.insert { expr := e } }
+    if let some uniqueId := EMatch.isTheoremInstanceProof? e then
+      if let some thm := map[uniqueId]? then
+        let key := (thm.origin, thm.kind)
+        unless (← get).collectedThms.contains key do
+          modify fun s => { s with collectedThms := s.collectedThms.insert key, thms := s.thms.push thm }
+    match e with
+    | .lam _ d b _
+    | .forallE _ d b _ => go d; go b
+    | .proj _ _ b
+    | .mdata _ b       => go b
+    | .letE _ t v b _  => go t; go v; go b
+    | .app f a         => go f; go a
+    | _ => return ()
+
+/--
+Creates an `instantiate` tactic that takes the `usedThms` as parameters.
+-/
+def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) (approx : Bool) : GrindM TGrind := goal.withContext do
+  let numDigits ← getNumDigitsForLocalTheoremAnchors goal
+  let mut params : Array (TSyntax ``Parser.Tactic.Grind.thm) := #[]
+  let mut foundFns : NameSet := {}
+  let mut foundLocals : Std.HashSet Grind.Origin := {}
+  for thm in usedThms do
+    unless (← isMatchEqLikeDeclName thm.origin.key) do
+      match thm.origin with
+      | .decl declName =>
+        if let some fnName ← isEqnThm? declName then
+          unless foundFns.contains fnName do
+            foundFns := foundFns.insert fnName
+            let param ← Grind.globalDeclToInstantiateParamSyntax declName thm.kind thm.minIndexable
+            params := params.push param
+        else
+          let param ← Grind.globalDeclToInstantiateParamSyntax declName thm.kind thm.minIndexable
+          params := params.push param
+      | _ => unless foundLocals.contains thm.origin do
+        foundLocals := foundLocals.insert thm.origin
+        let anchor ← getAnchor (← inferType thm.proof)
+        let param ← `(Parser.Tactic.Grind.thm| $(← mkAnchorSyntax numDigits anchor):anchor)
+        params := params.push param
+  match params.isEmpty, approx with
+  | true,  false => `(grind| instantiate only)
+  | false, false => `(grind| instantiate only [$params,*])
+  | true,  true  => `(grind| instantiate approx)
+  | false, true  => `(grind| instantiate approx [$params,*])
+
+def mkNewSeq (goal : Goal) (thms : Array EMatchTheorem) (seq : List TGrind) (approx : Bool) : GrindM (List TGrind) := do
+  if thms.isEmpty then
+    return seq
+  else
+    return ((← mkInstantiateTactic goal thms approx) :: seq)
+
+def getAllTheorems (map : EMatch.InstanceMap) : Array EMatchTheorem :=
+  map.toArray.map (·.2)
+
+public def instantiate' : Action := fun goal kna kp => do
+  let s ← saveStateIfTracing
+  let ((progress, map), goal') ← GoalM.run goal ematch'
   if progress then
-    concatTactic (← kp goal') `(grind| instantiate)
+    match (← kp goal') with
+    | .closed seq =>
+      if (← getConfig).trace then
+        let proof ← instantiateMVars (mkMVar goal.mvarId)
+        let usedThms := collect proof map
+        let newSeq ← mkNewSeq goal usedThms seq (approx := false)
+        if (← checkSeqAt s goal newSeq) then
+          return .closed newSeq
+        else
+          let allThms := getAllTheorems map
+          let newSeq ← mkNewSeq goal allThms seq (approx := true)
+          return .closed newSeq
+      else
+        return .closed []
+    | r => return r
   else
     kna goal
 
-def instantiate : Action :=
+public def instantiate : Action :=
   instantiate' >> assertAll
 
 end Lean.Meta.Grind.Action
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean
new file mode 100644
index 000000000000..89c2fc9f5898
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean
@@ -0,0 +1,88 @@
+/-
+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.Anchor
+public import Lean.Meta.Tactic.Grind.EMatchTheorem
+import Lean.Meta.Eqns
+namespace Lean.Meta.Grind
+/--
+Returns pairs `(type, anchor)` where `type` is the type of a local theorem,
+and `anchor` the anchor associated with it.
+-/
+public def getLocalTheoremAnchors (goal : Goal) : GrindM (Array ExprWithAnchor) := do
+  let (found, entries) ← go {} {} goal.ematch.thms
+  let (_, entries) ← go found entries goal.ematch.newThms
+  return entries
+where
+  go (found : Std.HashSet Grind.Origin) (result : Array ExprWithAnchor) (thms : PArray EMatchTheorem)
+      : GrindM (Std.HashSet Grind.Origin × Array ExprWithAnchor) := do
+    let mut found := found
+    let mut result := result
+    for thm in thms do
+      if !thm.origin matches .decl _ then
+      unless found.contains thm.origin do
+        found := found.insert thm.origin
+        let type ← inferType thm.proof
+        let anchor ← getAnchor type
+        result := result.push { anchor, e := type }
+        pure ()
+    return (found, result)
+
+/--
+Returns the number of digits needed to distinguish between different anchors.
+-/
+public def getNumDigitsForLocalTheoremAnchors (goal : Goal) : GrindM Nat := do
+  return getNumDigitsForAnchors (← getLocalTheoremAnchors goal)
+
+def globalDeclToGrindLemmaSyntax (declName : Name) (kind : EMatchTheoremKind) (minIndexable : Bool)
+    : MetaM (TSyntax [``Parser.Tactic.grindLemma, ``Parser.Tactic.grindLemmaMin]) := do
+  if let some declName ← isEqnThm? declName then
+    let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+    `(Parser.Tactic.grindLemma| $decl:ident)
+  else
+    let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+    let param ← match kind, minIndexable with
+      | .eqLhs false,   _     => `(Parser.Tactic.grindLemma| = $decl:ident)
+      | .eqLhs true,    _     => `(Parser.Tactic.grindLemma| = gen $decl:ident)
+      | .eqRhs false,   _     => `(Parser.Tactic.grindLemma| =_ $decl:ident)
+      | .eqRhs true,    _     => `(Parser.Tactic.grindLemma| =_ gen $decl:ident)
+      | .eqBoth false,  _     => `(Parser.Tactic.grindLemma| _=_ $decl:ident)
+      | .eqBoth true,   _     => `(Parser.Tactic.grindLemma| _=_ gen $decl:ident)
+      | .eqBwd,         _     => `(Parser.Tactic.grindLemma| ←= $decl:ident)
+      | .user,          _     => `(Parser.Tactic.grindLemma| usr $decl:ident)
+      | .bwd false,     false => `(Parser.Tactic.grindLemma| ← $decl:ident)
+      | .bwd true,      false => `(Parser.Tactic.grindLemma| ← gen $decl:ident)
+      | .fwd,           false => `(Parser.Tactic.grindLemma| → $decl:ident)
+      | .leftRight,     false => `(Parser.Tactic.grindLemma| => $decl:ident)
+      | .rightLeft,     false => `(Parser.Tactic.grindLemma| <= $decl:ident)
+      | .default false, false => `(Parser.Tactic.grindLemma| $decl:ident)
+      | .default true,  false => `(Parser.Tactic.grindLemma| gen $decl:ident)
+      | .bwd false,     true  => `(Parser.Tactic.grindLemmaMin| ! ← $decl:ident)
+      | .bwd true,      true  => `(Parser.Tactic.grindLemmaMin| ! ← gen $decl:ident)
+      | .fwd,           true  => `(Parser.Tactic.grindLemmaMin| ! → $decl:ident)
+      | .leftRight,     true  => `(Parser.Tactic.grindLemmaMin| ! => $decl:ident)
+      | .rightLeft,     true  => `(Parser.Tactic.grindLemmaMin| ! <= $decl:ident)
+      | .default false, true  => `(Parser.Tactic.grindLemmaMin| ! $decl:ident)
+      | .default true,  true  => `(Parser.Tactic.grindLemmaMin| ! gen $decl:ident)
+
+def toGrindParam (stx : TSyntax [``Parser.Tactic.grindLemma, ``Parser.Tactic.grindLemmaMin])
+    : TSyntax ``Parser.Tactic.grindParam :=
+  mkNode ``Parser.Tactic.grindParam #[stx]
+
+public def globalDeclToGrindParamSyntax (declName : Name) (kind : EMatchTheoremKind) (minIndexable : Bool)
+    : MetaM (TSyntax ``Parser.Tactic.grindParam) := do
+  return toGrindParam (← globalDeclToGrindLemmaSyntax declName kind minIndexable)
+
+def toInstantiateParam (stx : TSyntax [``Parser.Tactic.grindLemma, ``Parser.Tactic.grindLemmaMin])
+    : TSyntax ``Parser.Tactic.Grind.thm :=
+  mkNode ``Parser.Tactic.Grind.thm #[stx]
+
+public def globalDeclToInstantiateParamSyntax (declName : Name) (kind : EMatchTheoremKind) (minIndexable : Bool)
+    : MetaM (TSyntax ``Parser.Tactic.Grind.thm) := do
+  return toInstantiateParam (← globalDeclToGrindLemmaSyntax declName kind minIndexable)
+
+end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 2a49954ca755..933032afbc2d 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -1831,4 +1831,17 @@ def anchorPrefixToString (numDigits : Nat) (anchorPrefix : UInt64) : String :=
 def anchorToString (numDigits : Nat) (anchor : UInt64) : String :=
   anchorPrefixToString numDigits (anchor >>> (64 - 4*numDigits.toUInt64))
 
+/--
+Returns activated `match`-declaration equations.
+Recall that in tactics such as `instantiate only [...]`, `match`-declarations are always instantiated.
+-/
+def Goal.getActiveMatchEqTheorems (goal : Goal) : CoreM (Array EMatchTheorem) := do
+  let k (thms : Array EMatchTheorem) (thm : EMatchTheorem) : CoreM (Array EMatchTheorem) := do
+    if (← isMatchEqLikeDeclName thm.origin.key) then
+      return thms.push thm
+    else
+      return thms
+  let result ← goal.ematch.newThms.foldlM k #[]
+  goal.ematch.thms.foldlM k result
+
 end Lean.Meta.Grind
diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
index cbfed722cc4a..72b250fef6fc 100644
--- a/tests/lean/run/grind_finish_trace.lean
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -45,8 +45,8 @@ example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutativ
 /--
 info: Try this:
   [apply] ⏎
-    instantiate
-    instantiate
+    instantiate only [= Array.getElem_set]
+    instantiate only [= Array.getElem_set]
 -/
 #guard_msgs in
 example (as bs cs : Array α) (v₁ v₂ : α)
diff --git a/tests/lean/run/grind_interactive.lean b/tests/lean/run/grind_interactive.lean
index 927c761bbcfc..455d53b14295 100644
--- a/tests/lean/run/grind_interactive.lean
+++ b/tests/lean/run/grind_interactive.lean
@@ -401,8 +401,8 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind =>
-    instantiate Array.getElem_set | gen > 0
-    instantiate Array.getElem_set
+    instantiate only [Array.getElem_set] | gen > 0
+    instantiate only [Array.getElem_set]
 
 example (as bs cs : Array α) (v₁ v₂ : α)
         (i₁ i₂ j : Nat)
@@ -415,8 +415,8 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind =>
-    instantiate = Array.getElem_set
-    instantiate ← Array.getElem_set
+    instantiate only [= Array.getElem_set]
+    instantiate only [← Array.getElem_set]
 
 example (as bs cs : Array α) (v₁ v₂ : α)
         (i₁ i₂ j : Nat)
@@ -429,7 +429,7 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind =>
-    repeat instantiate =Array.getElem_set
+    repeat instantiate only [= Array.getElem_set]
 
 opaque p : Nat → Prop
 opaque q : Nat → Prop
@@ -441,7 +441,7 @@ axiom fInj : finv (f x) = x
 
 example : f x = f y → p x → q y := by
   grind =>
-    instantiate →pq, !fInj
+    instantiate only [→pq, !fInj]
 
 /--
 trace: [thms] Local theorems
@@ -452,18 +452,18 @@ trace: [thms] Local theorems
 example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by
   grind =>
     show_local_thms
-    instantiate #bfb8
+    instantiate only [#bfb8]
 
 example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by
   grind =>
     show_local_thms
-    instantiate #bfb8
+    instantiate only [#bfb8]
 
 /-- error: no local theorems -/
 #guard_msgs in
 example : (∀ x, q x) → (∀ x, p x → p (f x)) → p x → p (f (f x)) := by
   grind =>
-    instantiate #abcd
+    instantiate only [#abcd]
 
 /--
 error: unsolved goals
@@ -500,7 +500,7 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
   intro a
   grind =>
     cases #6ccb
-    instantiate pax
+    instantiate only [pax]
     show_cases
     rename_i y w _ -- Must reset cached anchors
     show_cases
@@ -511,7 +511,7 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
   intro a
   grind =>
     cases #6ccb
-    instantiate pax
+    instantiate only [pax]
     show_cases
     next y w _ =>
     show_cases