fix: handle dot notation on local variables in grind parameters (#11573)

This PR fixes `grind` rejecting dot notation terms, mistaking them for
local hypotheses.

When a grind parameter like `n.triv` is given, where `n` is a local
variable and `triv` is a theorem that takes `n` as an argument (so
`n.triv` means `Nat.triv n`), grind was incorrectly rejecting it with
"redundant parameter" because it detected that the identifier resolved
to a local variable via `resolveLocalName`.

The fix checks if `resolveLocalName` returns field projections
(non-empty list), indicating dot notation. In that case, we process the
parameter as a term expression to let elaboration resolve the dot
notation properly, rather than trying to resolve it as a global constant
name.

### Minimal reproducer

```lean
theorem Nat.triv (n : Nat) : n = n := rfl

example (n : Nat) : n = n := by
  grind [n.triv]  -- Previously: "redundant parameter `n.triv`"
```

This also fixes the issue where `grind [x.exp_pos]` was rejected even
though `x.exp_pos` elaborates to `Real.exp_pos x`, a valid theorem
application.

🤖 Prepared with Claude Code

Author: kim-em

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

@@ -231,9 +231,17 @@ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.T
         else
           params := { params with ematch := (← params.ematch.eraseDecl declName) }
       | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
-        params ← processParam params p mod? id (minIndexable := false) (only := only) (incremental := incremental)
+        -- Check if this is dot notation on a local variable (e.g., `n.triv` for `Nat.triv n`).
+        -- If so, process as term to let elaboration resolve the dot notation properly.
+        if let some (_, _ :: _) := (← resolveLocalName id.getId) then
+          params ← processTermParam params p mod? id (minIndexable := false)
+        else
+          params ← processParam params p mod? id (minIndexable := false) (only := only) (incremental := incremental)
       | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) =>
-        params ← processParam params p mod? id (minIndexable := true) (only := only) (incremental := incremental)
+        if let some (_, _ :: _) := (← resolveLocalName id.getId) then
+          params ← processTermParam params p mod? id (minIndexable := true)
+        else
+          params ← processParam params p mod? id (minIndexable := true) (only := only) (incremental := incremental)
       | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $e:term) =>
         params ← processTermParam params p mod? e (minIndexable := false)
       | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $e:term) =>

tests/lean/run/grind_local_hyps.lean

@@ -38,3 +38,10 @@ example : 0 = 0 := by
 example : 0 = 0 := by
   have h : 1 = 1 := rfl
   grind only [h]
+
+-- Checks that dot notation on a local variable for a global theorem is accepted.
+-- `n.triv` means `Nat.triv n`, not a local hypothesis.
+theorem Nat.triv (n : Nat) : n = n := rfl
+
+example (n : Nat) : n = n := by
+  grind [n.triv]