mathlib3

b4373e5a - feat(tactic/lint): linter for @[class] def (#6061)

feat(tactic/lint): linter for @[class] def (#6061) Also cleaning up some uses of `@[class] def` that were missed in #6028. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>