mathlib3

a148d797 - chore(*): revert #17048 (#17733)

chore(*): revert #17048 (#17733) This had merge conflicts which I've been rather reckless about resolving. Let's see what CI says. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>