Mathlib3 lemma and file names in comments

Stream: mathlib4

[Michael Rothgang]

Did you wonder how many left-over mathlib3 lemma or file names are in comments? Well, I have a first answer: I cobbled together a syntax linter which checks strings enclosed in backticks.
Just doing the simplest thing finds about 500 hits, here. (I stopped running it somewhere in Tactic, so e.g. Topology is not covered yet.) Feel free to fix any number of them :-)

This linter flags all lines which contain something in backticks which either

• exactly matches a mathlib3 file name (as evidenced by an align_import)
• exactly matches a mathlib3 declaration (as evidences by an align)
  Relaxing this to also match just the file or lemma name or substrings is a natural follow-up, but perhaps let's fix the first wave of cases first :-)

[Michael Rothgang]

Code is on branch#MR-lint-old-comments. I pre-generated a list of all aligns resp. align_imports; once you did those and fixed the local paths, you can simply run this via ./script/lint-style.sh.

[Michael Rothgang]

I tweaked my script a bit and added an auto-fix mode. Filed #11948 (topology) and #11949 (tactics) with the first changes, split by directory.

[Michael Rothgang]

Filed #11950 for Analysis also. That's it for this week, happy reviewing :-)

[Michael Rothgang]

Actually, I was curious and also filed #11952 (a few misc directories) and #11953 (order).

[Michael Rothgang]

And #11955 for Algebra and AlgebriacGeometry.

[Michael Rothgang]

Comments addressed on that one.