diff --git a/src/Lean/Elab/Tactic/Grind/Param.lean b/src/Lean/Elab/Tactic/Grind/Param.lean
index c502c5d15536..ec6c1c6e7dd6 100644
--- a/src/Lean/Elab/Tactic/Grind/Param.lean
+++ b/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) =>
diff --git a/tests/lean/run/grind_local_hyps.lean b/tests/lean/run/grind_local_hyps.lean
index ce57e409da07..1f95d4f67992 100644
--- a/tests/lean/run/grind_local_hyps.lean
+++ b/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]