diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index e341cfcd69..941639b200 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/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 =>
diff --git a/tests/lean/run/grind_reducible.lean b/tests/lean/run/grind_reducible.lean
index f006d17a1f..b8a9b88dc7 100644
--- a/tests/lean/run/grind_reducible.lean
+++ b/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]