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

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.

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

@@ -229,9 +229,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]