fix: grind? dropping options (#11481)

This PR fixes a bug in `grind?`. The suggestion using the `grind`
interactive mode was dropping the configuration options provided by the
user. In the following account, the third suggestion was dropping the
`-reducible` option.

```lean
/--
info: Try these:
  [apply] grind -reducible only [Equiv.congr_fun, #5103]
  [apply] grind -reducible only [Equiv.congr_fun]
  [apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
-/
example :
    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
  grind? -reducible [Equiv.congr_fun]
```

Author: leodemoura

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

@@ -342,10 +342,10 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
         -- let saved ← saveState
         match (← finish.run goal) with
         | .closed seq =>
-          let configCtx' := filterSuggestionsFromGrindConfig configStx
-          let tacs ← Grind.mkGrindOnlyTactics configCtx' seq
+          let configStx' := filterSuggestionsFromGrindConfig configStx
+          let tacs ← Grind.mkGrindOnlyTactics configStx' seq
           let seq := Grind.Action.mkGrindSeq seq
-          let tac ← `(tactic| grind => $seq:grindSeq)
+          let tac ← `(tactic| grind $configStx':optConfig => $seq:grindSeq)
           let tacs := tacs.push tac
           return tacs
         | .stuck gs =>

tests/lean/run/grind_reducible.lean

@@ -48,3 +48,15 @@ example :
     (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
     = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
   grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
+
+/--
+info: Try these:
+  [apply] grind -reducible only [Equiv.congr_fun, #5103]
+  [apply] grind -reducible only [Equiv.congr_fun]
+  [apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
+-/
+#guard_msgs in
+example :
+    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
+    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
+  grind? -reducible [Equiv.congr_fun]