chore(order/galois_connection): Make lifting instances reducible (#12559)
chore(order/galois_connection): Make lifting instances reducible (#12559)

and provide `infi₂` and `supr₂` versions of the lemmas.





leanprover-community/mathlib,leanprover-community/mathlib