mathlib

5bff97f2 - chore(data/set/basic): reflow/golf some proofs (#17066)

chore(data/set/basic): reflow/golf some proofs (#17066) * reuse facts about `order_top`; * use `alias`; * add `set.ssubset_univ_iff`; * replace some proofs with `iff.rfl`/`rfl`.