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