feat: lint `attribute [instance] instName in`

[grunweg]

Contrary to what users would expect, this defines a global instance.

This linter would have caught #13144 and #13170. Zulip discussion

Co-authored by: @adomani

---

[grunweg]

I wrote a test yesterday (of course!), but forgot to commit it :facepalm: I've updated it to use your example instance now (and added you as an author of the tests), since this avoid mathlib imports.

[grunweg]

I just tried the logic you proposed. It works, so I switched to it (and added you an an author). I tweaked one test to consider nested syntax (which worked), so I guess attributes are always the first syntax.

[grunweg]

!bench

[leanprover-bot]

Here are the benchmark results for commit 627bf3ad22c5bc22738e391fcc2e8f85ff6dfc8d. There were no significant changes against commit 49e1c29de1b78922c62e6e0cd04280bc742897f6.

[kim-em]

Two minor requests, otherwise

bors d+

[mathlib-bors[bot]]

:v: grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Thanks for the fast review. bors r+

[mathlib-bors[bot]]

Build failed:

• Build

[grunweg]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

[collares]

@grunweg Future idea for this linter: Catch #7678 as well.