deprecated produces its message on simp

[adomani]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

If a theorem is deprecated and used in simp or dsimp, the deprecation warning is attached to simp, rather than to the declaration itself.

Note: the warning message is correct, it is simply logged at the incorrect syntax node.

Context

This arose in the context of automatic replacement of deprecated declarations. See also this Zulip thread.

Steps to Reproduce

@[deprecated]
theorem hi : True := .intro

example : True := by
  -- the warning is on `simp`
  simp [
    hi  -- could the warning be logged at the syntax node of `hi`?
  ]

Expected behavior: The warning is on hi, not on simp

Actual behavior: The warning is on simp, not on hi.

Versions

#eval Lean.versionString: "4.9.0-rc1"
OS version: live.lean-lang.org, Linux

Additional Information

#4448 is already a PR to fix this issue.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.