DeprecateMe

Stream: mathlib4

[Kim Morrison]

@Damiano Testa, would you mind:

• renaming the files DeprecateMe to something else ("me" appears only in the filenames)
• reduce MathlibTest/DeprecateMe to something with minimal imports, so it is possible to quickly test? (This broke on nightly-testing and I'm having to compile half of Mathlib to see if fixes are working.)
• should this command start with #, since it should never persist in committed code? I'm uncertain where exactly our conventions have landed here.

[Damiano Testa]

I probably won't have time to get to this for several hours: feel free to comment out whatever is needed to get the build to work and I'll fix the issues when I'm back at a computer.

[Damiano Testa]

Ok, I think that this was much easier than expected! #19151

[Damiano Testa]

If it works as is, great, otherwise, I'll try to fix later! :smile: