feat: remove redundant deprecation warnings

[wkrozowski]

This PR silences the Linter.deprecated warnings inside of definitions that are themselves deprecated.

Closes #8942.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-05-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-01 17:02:56)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6998af1850c34dc9699505caeeed620c84f09a3a --onto dae325700c89e23c453b1d6d5ed5432d87880062. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-05 16:51:59)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-01 17:02:57)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6998af1850c34dc9699505caeeed620c84f09a3a --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-05 16:52:02)