Adding dates to remaining deprecations

Stream: PR reviews

[Michael Rothgang]

PRs #12334, #12335, #12336 and #12337 work towards labelling all deprecated theorems or aliasses with a date. The first two are just reformatting existing labels, the last two only add dates.

These four PRs fully handle the Analysis and parts of the Data directory; a WIP branch has some more instance. But let's get these reviewed first :-)

(Once lean4#3968 is available in mathlib, one can mass-convert these dates into readable form, and a metaprogramm could automatically delete declarations which have been deprecated for a long time.)

[Kim Morrison]

(To link to lean4 PRs you can use lean4#3968.)