mathlib

78e48c02 - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter (#5330)

ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter (#5330) [As requested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/the.20word.20.22to.22/near/219370843), the reserved notation linter checks for `reserve` or `precedence` at the start of a non-comment, non-string literal line in any file other than `tactic.core`. The new set_option linter disallows `set_option pp`, `set_option profiler` and `set_option trace` at the start of a non-comment, non-string literal line. I also noticed that the `small_alpha_vrachy_check` linter added in #4802 wasn't actually called, so I added it to the main `lint` function.