mathlib

29d0a4e6 - feat(tactic/lint): add linter that type-checks statements (#7694)

feat(tactic/lint): add linter that type-checks statements (#7694) * Add linter that type-checks the statements of all declarations with the default reducibility settings. A statement might not type-check if locally a declaration was made not `@[irreducible]` while globally it is. * Fix an issue where `with_one.monoid.to_mul_one_class` did not unify with `with_one.mul_one_class`. * Fix some proofs in `category_theory.opposites` so that they work while keeping `quiver.opposite` irreducible.