mathlib

fa5d9d61 - feat(tactic/lint/misc): unused haves and suffices linters (#9310)

feat(tactic/lint/misc): unused haves and suffices linters (#9310) A linter for unused term mode have and suffices statements. Based on initial work by @robertylewis https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for.20teaching/topic/linter.20for.20helping.20grading/near/209243601 but hopefully with less false positives now.