mathlib3

91a43e71 - feat(algebra/order/monoid): Co/contravariant classes for `with_bot`/`with_top` (#13369)

feat(algebra/order/monoid): Co/contravariant classes for `with_bot`/`with_top` (#13369) Add the `covariant_class (with_bot α) (with_bot α) (+) (≤)` and `contravariant_class (with_bot α) (with_bot α) (+) (<)` instances, as well as the lemmas that `covariant_class (with_bot α) (with_bot α) (+) (<)` and `contravariant_class (with_bot α) (with_bot α) (+) (≤)` almost hold. On the way, match the APIs for `with_bot`/`with_top` by adding missing lemmas. Co-authored-by: Wrenna Robson <wren.robson@gmail.com>