mathlib3

ef22a33f - feat(slim_check/errors): improve error messages and add useful instances (#4022)