From 00d41d64e5699cc822ffca813cdafd464d693516 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 31 Oct 2025 14:00:33 +1100
Subject: [PATCH] feat: remove `+premises` from `grind?` output (#11028)

This PR ensures that `grind? +premises` removes `+premises` from the
"Try this" suggestion.
---
 src/Lean/Elab/Tactic/Grind/Main.lean           | 18 +++++++++++++++++-
 .../lean/run/grind_question_mark_premises.lean | 12 ++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_question_mark_premises.lean

diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index a383a58c77..a252093241 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -201,6 +201,21 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
+/-- Filter out `+premises` from the config syntax -/
+def filterPremisesFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
+  let configItems := config.raw.getArgs
+  let filteredItems := configItems.filter fun item =>
+    -- Keep all items except +premises
+    -- Structure: null node -> configItem -> posConfigItem -> ["+", ident]
+    match item[0]? with
+    | some configItem => match configItem[0]? with
+      | some posConfigItem => match posConfigItem[1]? with
+        | some ident => !(posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `premises)
+        | none => true
+      | none => true
+    | none => true
+  ⟨config.raw.setArgs filteredItems⟩
+
 def mkGrindOnly
     (config : TSyntax ``Lean.Parser.Tactic.optConfig)
     (trace : Grind.Trace)
@@ -217,7 +232,8 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let result ← `(tactic| grind $config:optConfig only)
+  let filteredConfig := filterPremisesFromConfig config
+  let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 
 private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (interactive : Bool) : TacticM Grind.Config := do
diff --git a/tests/lean/run/grind_question_mark_premises.lean b/tests/lean/run/grind_question_mark_premises.lean
new file mode 100644
index 0000000000..a329bf8cd3
--- /dev/null
+++ b/tests/lean/run/grind_question_mark_premises.lean
@@ -0,0 +1,12 @@
+import Lean
+
+set_premise_selector Lean.PremiseSelection.sineQuaNonSelector
+
+-- Test that grind? +premises does NOT include +premises in its output
+/--
+info: Try this:
+  [apply] grind only
+-/
+#guard_msgs in
+example {x y : Nat} (h : x = y) : y = x := by
+  grind? +premises