mathlib

dffc243a - feat(order/complete_lattice): add `equiv.supr_congr` and `equiv.supr_comp` lemmas (#15852)

feat(order/complete_lattice): add `equiv.supr_congr` and `equiv.supr_comp` lemmas (#15852) Adds these lemmas as easy consequences of the `function.surjective` versions in order to aid in discovery.