fix: only fall back to term elaboration for compound identifiers

The previous implementation swallowed all constant lookup errors and fell
back to term elaboration. This caused:
1. Deprecated warnings not being shown (missing checkDeprecated call)
2. Wrong error messages for unknown simple identifiers

Now only fall back to term elaboration for compound identifiers like
`foo.le` where dot notation is plausible.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

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

@@ -80,73 +80,6 @@ public def addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Nam
   | _ =>
     throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
 
-def processParam (params : Grind.Params)
-    (p : TSyntax `Lean.Parser.Tactic.grindParam)
-    (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod))
-    (id : TSyntax `ident)
-    (minIndexable : Bool)
-    (only : Bool)
-    (incremental : Bool)
-    : MetaM Grind.Params := do
-  let mut params := params
-  let declName ← try
-    realizeGlobalConstNoOverloadWithInfo id
-  catch err =>
-    if (← resolveLocalName id.getId).isSome then
-      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 =>
-    unless only do
-      withRef p <| Grind.throwInvalidUsrModifier
-    ensureNoMinIndexable minIndexable
-    let s ← Grind.getEMatchTheorems
-    let thms := s.find (.decl declName)
-    let thms := thms.filter fun thm => thm.kind == .user
-    if thms.isEmpty then
-      throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
-    for thm in thms do
-      params := { params with extra := params.extra.push thm }
-  | .ematch kind =>
-    params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
-  | .cases eager =>
-    if incremental then throwError "`cases` parameter are not supported here"
-    ensureNoMinIndexable minIndexable
-    withRef p <| Grind.validateCasesAttr declName eager
-    params := { params with casesTypes := params.casesTypes.insert declName eager }
-  | .intro =>
-    if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
-      if incremental then throwError "`cases` parameter are not supported here"
-      for ctor in info.ctors do
-        params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
-    else
-      throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
-  | .inj =>
-    let thm ← Grind.mkInjectiveTheorem declName
-    params := { params with extraInj := params.extraInj.push thm }
-  | .ext =>
-    throwError "`[grind ext]` cannot be set using parameters"
-  | .infer =>
-    if let some declName ← Grind.isCasesAttrCandidate? declName false then
-      params := { params with casesTypes := params.casesTypes.insert declName false }
-      if let some info ← isInductivePredicate? declName then
-        -- If it is an inductive predicate,
-        -- we also add the constructors (intro rules) as E-matching rules
-        for ctor in info.ctors do
-          -- **Note**: We should not warn if `declName` is an inductive
-          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
-    else
-      params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
-  | .symbol prio =>
-    ensureNoMinIndexable minIndexable
-    params := { params with symPrios := params.symPrios.insert declName prio }
-  | .funCC =>
-    params := { params with funCCs := params.funCCs.insert declName }
-  return params
-
 def processAnchor (params : Grind.Params) (val : TSyntax `hexnum) : CoreM Grind.Params := do
   let anchorRefs := params.anchorRefs?.getD #[]
   let anchorRef ← Grind.elabAnchorRef val
@@ -207,6 +140,76 @@ def processTermParam (params : Grind.Params)
       throwError "invalid `grind` parameter, parameter type is not a `forall` and is universe polymorphic{indentExpr type}"
     return { params with extraFacts := params.extraFacts.push proof }
 
+def processParam (params : Grind.Params)
+    (p : TSyntax `Lean.Parser.Tactic.grindParam)
+    (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod))
+    (id : TSyntax `ident)
+    (minIndexable : Bool)
+    (only : Bool)
+    (incremental : Bool)
+    : TermElabM Grind.Params := do
+  let mut params := params
+  let declName ← try
+    realizeGlobalConstNoOverloadWithInfo id
+  catch err =>
+    if (← resolveLocalName id.getId).isSome then
+      throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
+    else if !id.getId.getPrefix.isAnonymous then
+      -- Fall back to term elaboration for compound identifiers like `foo.le` (dot notation on declarations)
+      return ← processTermParam params p mod? id minIndexable
+    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 =>
+    unless only do
+      withRef p <| Grind.throwInvalidUsrModifier
+    ensureNoMinIndexable minIndexable
+    let s ← Grind.getEMatchTheorems
+    let thms := s.find (.decl declName)
+    let thms := thms.filter fun thm => thm.kind == .user
+    if thms.isEmpty then
+      throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
+    for thm in thms do
+      params := { params with extra := params.extra.push thm }
+  | .ematch kind =>
+    params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
+  | .cases eager =>
+    if incremental then throwError "`cases` parameter are not supported here"
+    ensureNoMinIndexable minIndexable
+    withRef p <| Grind.validateCasesAttr declName eager
+    params := { params with casesTypes := params.casesTypes.insert declName eager }
+  | .intro =>
+    if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
+      if incremental then throwError "`cases` parameter are not supported here"
+      for ctor in info.ctors do
+        params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
+    else
+      throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
+  | .inj =>
+    let thm ← Grind.mkInjectiveTheorem declName
+    params := { params with extraInj := params.extraInj.push thm }
+  | .ext =>
+    throwError "`[grind ext]` cannot be set using parameters"
+  | .infer =>
+    if let some declName ← Grind.isCasesAttrCandidate? declName false then
+      params := { params with casesTypes := params.casesTypes.insert declName false }
+      if let some info ← isInductivePredicate? declName then
+        -- If it is an inductive predicate,
+        -- we also add the constructors (intro rules) as E-matching rules
+        for ctor in info.ctors do
+          -- **Note**: We should not warn if `declName` is an inductive
+          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
+    else
+      params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
+  | .symbol prio =>
+    ensureNoMinIndexable minIndexable
+    params := { params with symPrios := params.symPrios.insert declName prio }
+  | .funCC =>
+    params := { params with funCCs := params.funCCs.insert declName }
+  return params
+
 /--
 Elaborates `grind` parameters.
 `incremental = true` for tactics such as `finish`, in this case, we disable some kinds of parameters

tests/lean/run/grind_11690.lean

@@ -0,0 +1,26 @@
+/-!
+# Test for issue #11690: grind should support dot notation on declarations
+
+When using `grind only [foo.le]` where `foo.le` is dot notation applying
+`LT.lt.le` to a theorem `foo`, grind should elaborate it as a term rather
+than failing with "Unknown constant `foo.le`".
+-/
+
+class Preorder (α : Type) extends LE α, LT α where
+
+theorem le_of_lt [Preorder α] {a b : α} (hab : a < b) : a ≤ b := sorry
+
+variable [Preorder α]
+
+def LT.lt.le := @le_of_lt
+
+axiom α : Type
+axiom a : α
+axiom b : α
+axiom bar : a < b
+
+example : a ≤ b := bar.le  -- works (term elaboration)
+
+#guard_msgs in
+example : a ≤ b := by
+  grind only [bar.le]