mathlib

3b8d217c - refactor(order/upper_lower): Use `⨆` rather than `Sup` (#12644)

refactor(order/upper_lower): Use `⨆` rather than `Sup` (#12644) Turn `Sup (coe '' S)` into `⋃ s ∈ S, ↑s` and other similar changes. This greatly simplifies the proofs.