From acb179e3c343e288069ea6c0fd6a6bd7e5a2bb34 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 11:40:31 -0700
Subject: [PATCH 01/12] feat: add `EMatchTheoremParam.lean`

---
 src/Lean/Elab/Tactic/Grind/Main.lean          | 35 ++------
 src/Lean/Meta/Tactic/Grind.lean               |  1 +
 .../Meta/Tactic/Grind/EMatchTheoremParam.lean | 88 +++++++++++++++++++
 3 files changed, 95 insertions(+), 29 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean

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/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/EMatchTheoremParam.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean
new file mode 100644
index 000000000000..99736f1b4647
--- /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 .local _ | .fvar _ 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

From 7e7c2601aedb5033aea08fc7ece4040076d82e16 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 11:47:16 -0700
Subject: [PATCH 02/12] refactor: use `getLocalTheoremAnchors`

---
 src/Lean/Elab/Tactic/Grind/ShowState.lean | 22 ++--------------------
 1 file changed, 2 insertions(+), 20 deletions(-)

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

From e2e7b6fa35f8bb685e87aa4fb1e2764b1923ab83 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 12:49:10 -0700
Subject: [PATCH 03/12] feat: `instantiate` action with tracing

---
 src/Lean/Meta/Tactic/Grind/Action.lean        | 27 ++++--
 src/Lean/Meta/Tactic/Grind/EMatch.lean        | 57 +++++++++++--
 src/Lean/Meta/Tactic/Grind/EMatchAction.lean  | 82 +++++++++++++++++--
 .../Meta/Tactic/Grind/EMatchTheoremParam.lean |  2 +-
 4 files changed, 147 insertions(+), 21 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean
index 574b51cf0236..2c5c74c67ac8 100644
--- a/src/Lean/Meta/Tactic/Grind/Action.lean
+++ b/src/Lean/Meta/Tactic/Grind/Action.lean
@@ -251,21 +251,34 @@ 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 ← mkGrindNext seq
+  Lean.withoutModifyingState do
+    s.restore
+    let subgoals ← evalTactic goal tac
+    return subgoals.isEmpty
+
 /--
 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..141077e40ed2 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -67,10 +67,36 @@ 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 InstanceProofMap := 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, entries of the form `proof ↦ thm` are stored in `instancesMap`.
+  This mapping is later used to determine which theorem instantiations were actually
+  used in the final proof term. Here, `proof` refers to the proof of the theorem instantiation.
+  -/
+  instanceProofMap : InstanceProofMap := {}
   deriving Inhabited
 
 abbrev M := ReaderT Context $ StateRefT SearchState GoalM
@@ -78,6 +104,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 +482,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 instanceProofMap := s.instanceProofMap.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,26 +739,36 @@ 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 : GoalM InstanceProofMap := 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
   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.instanceProofMap
 
-/-- 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' : GoalM (Bool × InstanceProofMap) := do
   let numInstances := (← get).ematch.numInstances
-  ematchCore
-  return (← get).ematch.numInstances != numInstances
+  let map ← ematchCore
+  return ((← get).ematch.numInstances != numInstances, map)
+
+/--
+Performs one round of E-matching, and returns `true` if new instances were generated.
+-/
+def ematch : GoalM Bool :=
+  return (← ematch').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
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
index 64be0ae69653..134373934b5c 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -8,18 +8,88 @@ 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
 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.InstanceProofMap) : Array EMatchTheorem :=
+  let (_, s) := go e |>.run {}
+  s.thms
+where
+  go (e : Expr) : StateM CollectState Unit := do
+    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.
+Remark: assumes `usedThms` is not empty.
+-/
+def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) : 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
+    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
+  `(grind| instantiate $params,*)
+
+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 ← if usedThms.isEmpty then
+          pure seq
+        else
+          pure ((← mkInstantiateTactic goal usedThms) :: seq)
+        if (← checkSeqAt s goal newSeq) then
+          return .closed newSeq
+        else
+          let tac ← `(grind| instantiate)
+          return .closed (tac :: seq)
+      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
index 99736f1b4647..89c2fc9f5898 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheoremParam.lean
@@ -23,7 +23,7 @@ where
     let mut found := found
     let mut result := result
     for thm in thms do
-      if thm.origin matches .local _ | .fvar _ then
+      if !thm.origin matches .decl _ then
       unless found.contains thm.origin do
         found := found.insert thm.origin
         let type ← inferType thm.proof

From 44c2790af962a025c732b985f33acbc90b65ad29 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 13:24:47 -0700
Subject: [PATCH 04/12] feat: improve `instantiate` tactic notation

---
 src/Init/Grind/Interactive.lean               |  2 +-
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 22 ++++++++++---------
 src/Lean/Meta/Tactic/Grind/EMatch.lean        | 16 ++++++++------
 src/Lean/Meta/Tactic/Grind/EMatchAction.lean  |  2 +-
 4 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index ea442bb0c944..d7f8f41098cc 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -67,7 +67,7 @@ syntax anchor := "#" noWs hexnum
 syntax thm := anchor <|> grindLemma <|> grindLemmaMin
 
 /-- Instantiates theorems using E-matching. -/
-syntax (name := instantiate) "instantiate" (colGt thm),* : grind
+syntax (name := instantiate) "instantiate" (&" only")? (" [" withoutPosition(thm,*,?) "]")? : grind
 
 -- **Note**: Should we rename the following tactics to `trace_`?
 /-- Shows asserted facts. -/
diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index e81c8feec140..1f674f94029c 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,17 @@ 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 `(grind| instantiate $[ only%$only ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax
+  let only := only.isSome
   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
+  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/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 141077e40ed2..e7c48f8c3be9 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -739,10 +739,12 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-private def ematchCore : GoalM InstanceProofMap := do profileitM Exception "grind ematch" (← getOptions) do
+private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceProofMap := 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 {}
   else
@@ -759,19 +761,19 @@ private def ematchCore : GoalM InstanceProofMap := do profileitM Exception "grin
 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' : GoalM (Bool × InstanceProofMap) := do
+def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceProofMap) := do
   let numInstances := (← get).ematch.numInstances
-  let map ← ematchCore
+  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 : GoalM Bool :=
-  return (← ematch').1
+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 134373934b5c..3b9bfb8b0bfa 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -63,7 +63,7 @@ def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) : GrindM
       let anchor ← getAnchor (← inferType thm.proof)
       let param ← `(Parser.Tactic.Grind.thm| $(← mkAnchorSyntax numDigits anchor):anchor)
       params := params.push param
-  `(grind| instantiate $params,*)
+  `(grind| instantiate only [$params,*])
 
 public def instantiate' : Action := fun goal kna kp => do
   let s ← saveStateIfTracing

From a0254642dc1158f3641bdda5c93eac58b5c00137 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 13:51:02 -0700
Subject: [PATCH 05/12] feat: `match` equations are implicit at `instantiate`

---
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean |  4 ++-
 src/Lean/Meta/Tactic/Grind/EMatchAction.lean  | 31 ++++++++++---------
 src/Lean/Meta/Tactic/Grind/Types.lean         | 13 ++++++++
 3 files changed, 33 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index 1f674f94029c..cd2605bc3966 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -143,8 +143,10 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
 
 @[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do
   let `(grind| instantiate $[ only%$only ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax
+  let goal ← getMainGoal
   let only := only.isSome
-  let mut thms := #[]
+  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
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
index 3b9bfb8b0bfa..b8f7cb32e5c2 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -40,7 +40,6 @@ where
 
 /--
 Creates an `instantiate` tactic that takes the `usedThms` as parameters.
-Remark: assumes `usedThms` is not empty.
 -/
 def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) : GrindM TGrind := goal.withContext do
   let numDigits ← getNumDigitsForLocalTheoremAnchors goal
@@ -48,22 +47,26 @@ def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) : GrindM
   let mut foundFns : NameSet := {}
   let mut foundLocals : Std.HashSet Grind.Origin := {}
   for thm in usedThms do
-    match thm.origin with
-    | .decl declName =>
-      if let some fnName ← isEqnThm? declName then
-        unless foundFns.contains fnName do
-          foundFns := foundFns.insert fnName
+    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
-      else
-        let param ← Grind.globalDeclToInstantiateParamSyntax declName thm.kind thm.minIndexable
+      | _ => 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
-    | _ => 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
-  `(grind| instantiate only [$params,*])
+  if params.isEmpty then
+    `(grind| instantiate only)
+  else
+    `(grind| instantiate only [$params,*])
 
 public def instantiate' : Action := fun goal kna kp => do
   let s ← saveStateIfTracing
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

From 63fb7ccf9c70a4b970436dc4dea92afb8df482f6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 14:07:32 -0700
Subject: [PATCH 06/12] fix: `checkSeqAt`

`done` will swallow failures
---
 src/Lean/Meta/Tactic/Grind/Action.lean | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean
index 2c5c74c67ac8..ab14735c8097 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
@@ -262,11 +276,13 @@ 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 ← mkGrindNext seq
+  let tac ← mkGrindParen seq
   Lean.withoutModifyingState do
     s.restore
-    let subgoals ← evalTactic goal tac
-    return subgoals.isEmpty
+    -- **Note**: Ensure tracing is disabled.
+    withTheReader Grind.Context (fun ctx => { ctx with config.trace := false }) do
+      let subgoals ← evalTactic goal tac
+      return subgoals.isEmpty
 
 /--
 Helper action that checks whether the resulting tactic script produced by its continuation

From 97567359f1aa20145720865daf759dea39aead5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 14:57:29 -0700
Subject: [PATCH 07/12] feat: mark `instantiate` tactics that are approximate

---
 src/Init/Grind/Interactive.lean               |  8 +++--
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean |  2 +-
 src/Lean/Meta/Tactic/Grind/EMatch.lean        | 16 +++++-----
 src/Lean/Meta/Tactic/Grind/EMatchAction.lean  | 30 ++++++++++++-------
 4 files changed, 33 insertions(+), 23 deletions(-)

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index d7f8f41098cc..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" (&" only")? (" [" withoutPosition(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/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index cd2605bc3966..e81ecb47679f 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -142,7 +142,7 @@ 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 $[ only%$only ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax
+  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 #[]
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index e7c48f8c3be9..bbeadcde3307 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -71,7 +71,7 @@ structure Context where
 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 InstanceProofMap := Std.HashMap Name EMatchTheorem
+abbrev InstanceMap := Std.HashMap Name EMatchTheorem
 
 private def thmInstanceKey := `_grind_thm_instance
 
@@ -92,11 +92,9 @@ structure SearchState where
   /-- Choices that still have to be processed. -/
   choiceStack  : List Choice := []
   /--
-  When tracing is enabled, entries of the form `proof ↦ thm` are stored in `instancesMap`.
-  This mapping is later used to determine which theorem instantiations were actually
-  used in the final proof term. Here, `proof` refers to the proof of the theorem instantiation.
+  When tracing is enabled track instances here. See comment at `InstanceMap`
   -/
-  instanceProofMap : InstanceProofMap := {}
+  instanceMap : InstanceMap := {}
   deriving Inhabited
 
 abbrev M := ReaderT Context $ StateRefT SearchState GoalM
@@ -485,7 +483,7 @@ where
     if (← getConfig).trace then
       let uniqueId ← mkFreshId
       proof := markTheoremInstanceProof proof uniqueId
-      modify fun s => { s with instanceProofMap := s.instanceProofMap.insert uniqueId thm }
+      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
@@ -739,7 +737,7 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceProofMap := 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 }) do
@@ -755,13 +753,13 @@ private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceProofMa
       ematch.gmt       := s.ematch.gmt + 1
       ematch.num       := s.ematch.num + 1
     }
-    return s.instanceProofMap
+    return s.instanceMap
 
 /--
 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 × InstanceProofMap) := do
+def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceMap) := do
   let numInstances := (← get).ematch.numInstances
   let map ← ematchCore extraThms
   return ((← get).ematch.numInstances != numInstances, map)
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
index b8f7cb32e5c2..a53dfaa03242 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -16,7 +16,7 @@ structure CollectState where
   collectedThms : Std.HashSet (Origin × EMatchTheoremKind) := {}
   thms          : Array EMatchTheorem := #[]
 
-def collect (e : Expr) (map : EMatch.InstanceProofMap) : Array EMatchTheorem :=
+def collect (e : Expr) (map : EMatch.InstanceMap) : Array EMatchTheorem :=
   let (_, s) := go e |>.run {}
   s.thms
 where
@@ -41,7 +41,7 @@ where
 /--
 Creates an `instantiate` tactic that takes the `usedThms` as parameters.
 -/
-def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) : GrindM TGrind := goal.withContext do
+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 := {}
@@ -63,10 +63,20 @@ def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) : GrindM
         let anchor ← getAnchor (← inferType thm.proof)
         let param ← `(Parser.Tactic.Grind.thm| $(← mkAnchorSyntax numDigits anchor):anchor)
         params := params.push param
-  if params.isEmpty then
-    `(grind| instantiate only)
+  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
-    `(grind| instantiate only [$params,*])
+    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
@@ -77,15 +87,13 @@ public def instantiate' : Action := fun goal kna kp => do
       if (← getConfig).trace then
         let proof ← instantiateMVars (mkMVar goal.mvarId)
         let usedThms := collect proof map
-        let newSeq ← if usedThms.isEmpty then
-          pure seq
-        else
-          pure ((← mkInstantiateTactic goal usedThms) :: seq)
+        let newSeq ← mkNewSeq goal usedThms seq (approx := false)
         if (← checkSeqAt s goal newSeq) then
           return .closed newSeq
         else
-          let tac ← `(grind| instantiate)
-          return .closed (tac :: seq)
+          let allThms := getAllTheorems map
+          let newSeq ← mkNewSeq goal allThms seq (approx := true)
+          return .closed newSeq
       else
         return .closed []
     | r => return r

From 1a9d87674681ac758aad6a206218682597315e10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 15:28:52 -0700
Subject: [PATCH 08/12] test: fix

---
 tests/lean/run/grind_finish_trace.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
index cbfed722cc4a..85e8603055f2 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, = Array.size_set]
+    instantiate only [= Array.getElem_set]
 -/
 #guard_msgs in
 example (as bs cs : Array α) (v₁ v₂ : α)

From d848831fa96fa2cfc0ba0846eb8c3db5f0395402 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 15:48:33 -0700
Subject: [PATCH 09/12] test: fix

---
 tests/lean/run/grind_interactive.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

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

From 7856fdf62f13c5df893200737b77c5a2480d382d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 15:58:22 -0700
Subject: [PATCH 10/12] fix: do not visit subsingletons

---
 src/Lean/Meta/Tactic/Grind/EMatchAction.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
index a53dfaa03242..fe4cdb23b723 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchAction.lean
@@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.Action
 public import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
+import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
 namespace Lean.Meta.Grind.Action
 
 structure CollectState where
@@ -21,6 +22,12 @@ def collect (e : Expr) (map : EMatch.InstanceMap) : Array EMatchTheorem :=
   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 } }

From a81701fb0ebc6d8286e05114dbf652bda348666e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 15:59:00 -0700
Subject: [PATCH 11/12] chore: fix test

---
 tests/lean/run/grind_finish_trace.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
index 85e8603055f2..72b250fef6fc 100644
--- a/tests/lean/run/grind_finish_trace.lean
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -45,7 +45,7 @@ example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutativ
 /--
 info: Try this:
   [apply] ⏎
-    instantiate only [= Array.getElem_set, = Array.size_set]
+    instantiate only [= Array.getElem_set]
     instantiate only [= Array.getElem_set]
 -/
 #guard_msgs in

From 4a3638e0d0cccf6e281fc5d447d1eeae562db67b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 19 Oct 2025 16:04:14 -0700
Subject: [PATCH 12/12] feat: do not recover

---
 src/Lean/Elab/Tactic/Grind/Basic.lean  | 2 +-
 src/Lean/Meta/Tactic/Grind/Action.lean | 7 +++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

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/Meta/Tactic/Grind/Action.lean b/src/Lean/Meta/Tactic/Grind/Action.lean
index ab14735c8097..26d9f745ca76 100644
--- a/src/Lean/Meta/Tactic/Grind/Action.lean
+++ b/src/Lean/Meta/Tactic/Grind/Action.lean
@@ -281,8 +281,11 @@ def checkSeqAt (s? : Option SavedState) (goal : Goal) (seq : List TGrind) : Grin
     s.restore
     -- **Note**: Ensure tracing is disabled.
     withTheReader Grind.Context (fun ctx => { ctx with config.trace := false }) do
-      let subgoals ← evalTactic goal tac
-      return subgoals.isEmpty
+      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