fix: set_option auto-completion in grind mode

This PR fixes auto-completion for `set_option` in `grind` interactive mode.

src/Init/Grind/Interactive.lean

@@ -192,7 +192,7 @@ 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
+syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind
 
 end Grind
 end Lean.Parser.Tactic

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

@@ -426,7 +426,7 @@ where
   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]
+  let options ← Elab.elabSetOption stx[1] stx[3]
+  withOptions (fun _ => options) do evalGrindTactic stx[5]
 
 end Lean.Elab.Tactic.Grind