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.





leanprover-community/mathlib,leanprover-community/mathlib