mathlib3

6fe81bd5 - chore(*): remove `plift` from some lemmas about `infi`/`supr` (#3503)

chore(*): remove `plift` from some lemmas about `infi`/`supr` (#3503) Now `supr_eq_supr_finset` etc assume `ι` is a `Type*` and don't use `plift`. If you want to apply it to a `Sort*`, rewrite on `equiv.plift.surjective.supr_comp` first. ## Full list of API changes: ### `data/equiv/basic` * `equiv.ulift`: change the order of universe arguments to match `ulift`; * add `coe_ulift`, `coe_plift`, `coe_ulift_symm`, `coe_plift_symm`; ### `data/finset/lattice` * `supr_eq_supr_finset`, `infi_eq_infi_finset`: assume `ι` is a `Type*`, avoid `plift`; * `Union_eq_Union_finset`, `Inter_eq_Inter_finset`: same as above; ### `data/set/basic` * `function.surjective.range_comp`: generalize to `Sort*` for 2 of 3 arguments; ### `order/complete_lattice` * remove `supr_congr` and `infi_congr`; * add `function.surjective.supr_comp` and `function.surjective.infi_comp`.