fix: handle dot notation on local variables in grind parameters

[kim-em]

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

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

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 19e1fe55f33a8aadc4243da32828b70a4b4677cc --onto 1d0d3915ca79d0875a757fc5061121ae9cd58543. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-10 04:58:58)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 19e1fe55f33a8aadc4243da32828b70a4b4677cc --onto 1d0d3915ca79d0875a757fc5061121ae9cd58543. You can force reference manual CI using the force-manual-ci label. (2025-12-10 04:58:59)