fix: show deprecation warnings for grind theorem arguments (#11593)

This PR fixes an issue where `grind` did not display deprecation
warnings when deprecated lemmas were used in its argument list.

The fix adds explicit calls to `Linter.checkDeprecated` after resolving
theorem names in both `processParam` (for theorem arguments) and
`elabGrindParams` (for the `-` erase syntax).

Closes #11582

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <[email protected]>

Author: kim-em

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

@@ -96,6 +96,7 @@ def processParam (params : Grind.Params)
       throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
     else
       throw err
+  Linter.checkDeprecated declName
   let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
   match kind with
   | .ematch .user =>
@@ -221,6 +222,7 @@ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.T
         if incremental then
           throwErrorAt p "invalid `-` occurrence, it can only used at the `grind` tactic entry point"
         let declName ← realizeGlobalConstNoOverloadWithInfo id
+        Linter.checkDeprecated declName
         if let some declName ← Grind.isCasesAttrCandidate? declName false then
           Grind.ensureNotBuiltinCases declName
           params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }

tests/lean/run/grindDeprecated.lean

@@ -0,0 +1,27 @@
+/-!
+Test that `grind` flags deprecated theorems.
+See https://github.com/leanprover/lean4/issues/11582
+-/
+set_option backward.grind.inferPattern true  -- Use old pattern inference (no suggestions)
+set_option linter.deprecated true  -- Enable the deprecated linter (test framework disables all linters)
+
+def foo : Nat := 0
+
+@[deprecated "use foo_eq_zero' instead" (since := "2025-01-01")]
+theorem foo_eq_zero : foo = 0 := rfl
+
+/-- warning: `foo_eq_zero` has been deprecated: use foo_eq_zero' instead -/
+#guard_msgs in
+example : foo = foo := by grind [foo_eq_zero]
+
+-- Also test the `-` syntax for erasing theorems
+@[grind]
+theorem bar_eq_zero : foo = 0 := rfl
+
+-- This theorem is deprecated AND marked with @[grind], so we can erase it
+@[deprecated bar_eq_zero (since := "2025-01-01"), grind]
+theorem bar_eq_zero' : foo = 0 := rfl
+
+/-- warning: `bar_eq_zero'` has been deprecated: Use `bar_eq_zero` instead -/
+#guard_msgs in
+example : foo = foo := by grind [- bar_eq_zero']