mathlib3

0b8a858f - feat(tactic/lint): minor linter improvements (#8934)

feat(tactic/lint): minor linter improvements (#8934) * Change `#print foo` with `#check @foo` in the output of the linter * Include the number of linters in the output message * add `attribute [nolint syn_taut] rfl`