feat: rewrite set_option style linter in lean

[grunweg]

Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.

---

Mentored by @digama0; thanks for all your help. Written at the HIM school on formalization of mathematics.

[grunweg]

Actually, this PR is blocked on #11807 (and adapting it accordingly).

[grunweg]

~~The CI failure is interesting: I have no idea where this is coming from. Help on this detail is welcome.~~ After rebasing, CI passes. I guess it was something intermittent.

[robertylewis]

I could see a case for generalizing this: the list of disallowed options should be customizable/extensible by downstream projects. But, future work. Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[grunweg]

Thanks for the review! I agree that making this list configurable could be useful - if somebody sees a specific use, I'm happy to look at PRs extending this!