From 6dd8ad13e5bb79d4d4f4697c604f511852b0c8cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 18 Nov 2025 14:11:20 -0800
Subject: [PATCH] fix: `grind` minor issues (#11244)

This PR fixes minor issues in `grind`. In preparation for adding `grind
-revert`.
---
 src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean | 4 ++++
 src/Lean/Meta/Tactic/Grind/Types.lean                   | 8 ++++----
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean
index a00154c763..2580e5ba00 100644
--- a/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean
+++ b/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean
@@ -91,6 +91,10 @@ where
     return e'
 
   preprocess (e : Expr) : M Expr := do
+    /-
+    **Note**: We must use `instantiateMVars` here because this function is called using the result of `inferType`.
+    -/
+    let e ← instantiateMVars e
     /-
     We must unfold reducible constants occurring in `prop` because the congruence closure
     module in `grind` assumes they have been expanded.
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index c9b392e913..2f5084816a 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -1003,11 +1003,11 @@ def Goal.getENode? (goal : Goal) (e : Expr) : Option ENode :=
 def getENode? (e : Expr) : GoalM (Option ENode) :=
   return (← get).getENode? e
 
-def throwNonInternalizedExpr (e : Expr) : CoreM α :=
+def throwNonInternalizedExpr (e : Expr) : MetaM α :=
   throwError "internal `grind` error, term has not been internalized{indentExpr e}"
 
 /-- Returns node associated with `e`. It assumes `e` has already been internalized. -/
-def Goal.getENode (goal : Goal) (e : Expr) : CoreM ENode := do
+def Goal.getENode (goal : Goal) (e : Expr) : MetaM ENode := do
   let some n := goal.enodeMap.find? { expr := e }
     | throwNonInternalizedExpr e
   return n
@@ -1066,7 +1066,7 @@ def getRoot? (e : Expr) : GoalM (Option Expr) := do
   return (← get).getRoot? e
 
 /-- Returns the root element in the equivalence class of `e`. -/
-def Goal.getRoot (goal : Goal) (e : Expr) : CoreM Expr :=
+def Goal.getRoot (goal : Goal) (e : Expr) : MetaM Expr :=
   return (← goal.getENode e).root
 
 @[inline, inherit_doc Goal.getRoot]
@@ -1091,7 +1091,7 @@ def Goal.getNext? (goal : Goal) (e : Expr) : Option Expr := Id.run do
   return some n.next
 
 /-- Returns the next element in the equivalence class of `e`. -/
-def Goal.getNext (goal : Goal) (e : Expr) : CoreM Expr :=
+def Goal.getNext (goal : Goal) (e : Expr) : MetaM Expr :=
   return (← goal.getENode e).next
 
 @[inline, inherit_doc Goal.getRoot]