mathlib3

be4c5aa4 - feat(scripts/lint_mathlib): implement github annotations for mathlib linters (#11345)

feat(scripts/lint_mathlib): implement github annotations for mathlib linters (#11345) Resolves the last part of #5863 This causes `lean --run lint_mathlib --github` to produce error messages understood by github actions, which will tag the lines causing linter failures with annotations in the files changed tab