mathlib3

83225b3d - feat(order/monovary): Add missing `monovary` lemmas (#13243)

feat(order/monovary): Add missing `monovary` lemmas (#13243) Add lemmas for postcomposing monovarying functions with monotone/antitone functions. Protect lemmas that needed it. Fix typos. Co-authored-by: YaelDillies <yael.dillies@gmail.com>