feat(tactic/lint): reducible non-instance linter (#8540)
* This linter checks that if an instances uses a non-instance with as type a class, the non-instances is reducible.
* There are many false positives to this rule, which we probably want to allow (that are unlikely to cause problems). To cut down on the many many false positives, the linter currently only consider classes that have either an `add` or a `mul` field. Maybe we want to also include order-structures, but there are (for example) a bunch of `complete_lattice` structures that are derived using Galois insertions that haven't ever caused problems (I think).
