Old deprecations

Stream: mathlib4

[Yaël Dillies]

Should we start removing old @[deprecated] attributes along with their corresponding declaration? Eg there is currently 163 declarations that were deprecated in 2023 and 4 in 2022.

[Yaël Dillies]

Tentatively pinging @Damiano Testa to see whether he has written a tool to automatically remove them

[Damiano Testa]

I have not, but that should be fairly easy.

[Michael Rothgang]

Let me cross-link mathlib4>Deprecation policy: it's on my list to wrap up that thread.

One of the loose ends in there was agreeing on a time-frame for "delete this". Older than a year seemed extremely safe to delete.