From 1fc4768b687e55148f947b64938a0bdfd3ec7537 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 1 Dec 2025 23:04:04 -0800
Subject: [PATCH] fix: incorrect reducibility setting in `grind` interactive
 mode (#11471)

This PR fixes an incorrect reducibility setting when using `grind`
interactive mode.

Signed-off-by: Leonardo de Moura <leomoura@amazon.com>
---
 src/Lean/Elab/Tactic/Grind/Basic.lean  | 5 ++++-
 src/Lean/Meta/Tactic/Grind/EMatch.lean | 6 +++++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean
index ec8e4fc285..9db7eeebf5 100644
--- a/src/Lean/Elab/Tactic/Grind/Basic.lean
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@@ -282,7 +282,10 @@ def tryTactic (tac : GrindTacticM α) : GrindTacticM Bool := do
 
 open Grind
 
-def liftGrindM (k : GrindM α) : GrindTacticM α := do
+/-
+**Note**: Recall that `grind` uses `Reducible` setting to avoid expensive definitionally equality tests.
+-/
+def liftGrindM (k : GrindM α) : GrindTacticM α := withReducible do
   let ctx ← read
   let s ← get
   let (a, state) ← liftMetaM <| k ctx.methods.toMethodsRef ctx.ctx |>.run s.state
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index dd2e364cff..7fe767fb9b 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -499,7 +499,11 @@ where
       -- We must add a hint because `annotateEqnTypeConds` introduces `Grind.PreMatchCond`
       -- which is not reducible.
       proof := mkExpectedPropHint proof prop
-    addTheoremInstance thm proof prop (generation+1) guards
+    /-
+    **Note**: Must restore `reducible` setting because with use `withDefault` at `instantiateTheorem`.
+    -/
+    withReducible do
+      addTheoremInstance thm proof prop (generation+1) guards
 
 private def synthesizeInsts (mvars : Array Expr) (bis : Array BinderInfo) : OptionT M Unit := do
   let thm := (← read).thm