feat: set_option tactic in grind interactive mode

src/Init/Grind/Interactive.lean

@@ -189,5 +189,10 @@ generated `grind` tactic scripts.
 -/
 syntax (name := exposeNames) "expose_names" : grind
 
+/--
+`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,
+but it sets the option only within the tactics `tacs`. -/
+syntax (name := setOption) "set_option " ident ppSpace optionValue " in " grindSeq : grind
+
 end Grind
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -25,6 +25,7 @@ import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.RenameInaccessibles
 import Lean.Elab.Tactic.Grind.Filter
 import Lean.Elab.Tactic.Grind.ShowState
+import Lean.Elab.SetOption
 namespace Lean.Elab.Tactic.Grind
 
 def showStateAt (ref : Syntax) (filter : Filter) : GrindTacticM Unit := do
@@ -424,4 +425,8 @@ where
   liftGrindM <| resetAnchors
   replaceMainGoal [{ goal with mvarId }]
 
+@[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do
+  let options ← Elab.elabSetOption stx[1] stx[2]
+  withOptions (fun _ => options) do evalGrindTactic stx[4]
+
 end Lean.Elab.Tactic.Grind

tests/lean/run/grind_interactive.lean

@@ -431,6 +431,25 @@ example (as bs cs : Array α) (v₁ v₂ : α)
   grind =>
     repeat instantiate only [= Array.getElem_set]
 
+/--
+trace: [grind.ematch.instance] Array.getElem_set: (as.set i₁ v₁ ⋯)[j] = if i₁ = j then v₁ else as[j]
+-/
+#guard_msgs in
+example (as bs cs : Array α) (v₁ v₂ : α)
+        (i₁ i₂ j : Nat)
+        (h₁ : i₁ < as.size)
+        (h₂ : bs = as.set i₁ v₁)
+        (h₃ : i₂ < bs.size)
+        (h₃ : cs = bs.set i₂ v₂)
+        (h₄ : i₁ ≠ j ∧ i₂ ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind =>
+    instantiate
+    set_option trace.grind.ematch.instance true in
+    instantiate
+
 opaque p : Nat → Prop
 opaque q : Nat → Prop
 opaque f : Nat → Nat