mathlib3

542471fd - feat(data/set/function): Congruence lemmas for `monotone_on` and friends (#10817)

feat(data/set/function): Congruence lemmas for `monotone_on` and friends (#10817) Congruence lemmas for `monotone_on`, `antitone_on`, `strict_mono_on`, `strict_anti_on` using `set.eq_on`. `data.set.function` imports `order.monotone` so we must put them here.