mathlib3

ac5a7cec - refactor(data/set/intervals/monotone): split (#17893)

refactor(data/set/intervals/monotone): split (#17893) Also generalize&golf `monotone_on.exists_monotone_extension` and rename `order.monotone` to `order.monotone.basic`. Lean 4 version is leanprover-community/mathlib4#947