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 <[email protected]>

Author: leodemoura

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

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