mathlib

365e30de - chore(data/set/*,order/*): add missing lemmas about `monotone_on` etc (#14943)

chore(data/set/*,order/*): add missing lemmas about `monotone_on` etc (#14943) * Add `monotone_on`/`antitone`/`antitone_on` versions of existing `monotone` lemmas for `id`/`const`, `inf`/`sup`/`min`/`max`, `inter`/`union`, and intervals. * Drop `set.monotone_prod`, leave `monotone.set_prod` only. * Golf some proofs that were broken by removal of `set.monotone_prod`.