refactor(lint-style): various small clean-ups

[grunweg]

• alphabetise imports
• ensure errors are distinct
• convert the list of style errors to an enum
• use this to deduplicate and simplify printing errors and parsing exceptions

---

See individual commit messages for details. Each commit can be reviewed independently.

[Ruben-VandeVelde]

I'm not sure I agree with the first commit: if the script can produce an error, we should be able to except it

[grunweg]

I see your point, but I would argue that the particular errors I'm removing should never land in mathlib anyway - so I don't see why excepting them would be useful! (If there's the need to make the build pass, commenting that linter is another option.)

(FWIW, the script currently doesn't implement excepting all errors, so the current logic is already different.)

[grunweg]

I pushed a few more commits, refactoring the script further: in particular, parsing style-exceptions now truly recognises all possible errors, in fewer lines of code than before.

[grunweg]

This removes some variants; a later commit implements parsing all exception types (making this obsolete).
(I didn't feel like editing history again to edit this part out.)

[grunweg]

For the record: #13199 will make this PR obsolete. If you'd like to review this, reviewing the PRs split off #13199 might be more useful long-term.

[grunweg]

Let me close this PR in favour of #13199 (and its pieces).