fix: deprecated warning position at simp arguments (#4484)

closes #4452

src/Lean/Elab/Term.lean

@@ -1836,9 +1836,9 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? :
       return (c, ids.head!, ids.tail!)
   | _ => throwError "identifier expected"
 
-def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) :=
+def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) := withRef stx do
   match stx with
-  | .ident _ _ val preresolved => do
+  | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
     let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f

tests/lean/4452.lean

@@ -0,0 +1,29 @@
+def a := 1
+
+@[deprecated]
+theorem hi : a = 1 := rfl
+
+attribute [simp] hi
+
+example (h : 1 = b) : a = b := by
+  simp
+  guard_target =ₛ 1 = b
+  exact h
+
+set_option linter.all true
+
+example (h : 1 = b) : a = b := by
+  simp[
+    hi
+  ]
+  guard_target =ₛ 1 = b
+  exact h
+
+@[deprecated]
+theorem hi' : True := .intro
+
+example : True := by
+  -- the warning is on `simp`
+  simp [
+    hi'  -- warning should be logged here
+  ]

tests/lean/4452.lean.expected.out

@@ -0,0 +1,2 @@
+4452.lean:17:4-17:6: warning: `hi` has been deprecated
+4452.lean:28:4-28:7: warning: `hi'` has been deprecated