`@[deprecated]` on a structure field projection does not warn when constructing the field

Prerequisites

• 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

@[deprecated] on a structure/class field deprecates the projection constant, so it warns on reads of the field, but it does not warn when the field is provided by name in an anonymous constructor { … } or a where block. This makes it impossible to fully deprecate a field name: the construction side, which is exactly where instance/structure authors need the migration nudge, stays silent.

Steps to Reproduce

structure Point where
  x : Nat
  y : Nat

attribute [deprecated Point.x (since := "2026-01-01")] Point.y

-- (1) Provide the deprecated field `y` by name in an anonymous constructor / `where`.
def p₁ : Point := { x := 1, y := 2 }
def p₂ : Point where
  x := 1
  y := 2

-- (2) Reference the deprecated projection `Point.y`.
example : Nat := Point.y p₁

Expected behavior: Deprecation warning on y := 2

Actual behavior: No deprecation warning on y := 2. Only a warning on the use Point.y.

Versions

Lean 4.36.0-nightly-2026-09-17
Target: x86_64-unknown-linux-gnu Linux

Additional Information

Orthogonally, it would be nice if we could provide the deprecation attribute when declaring the field. That's #13221, but that issue it otherwise unrelated.

Impact

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

Start with the minimal self-contained reproduction in the issue and inspect elaboration of named fields in anonymous constructors and where blocks, focusing on how deprecation diagnostics are triggered for projections. Add a regression test covering both construction forms, then verify that y := 2 emits a deprecation warning while the existing projection warning remains intact.