Commit 2021-10-24 03:33 e836a722

feat(order/galois_connection): add exists_eq_{l,u}, tidy up lemmas (#9904) This makes some arguments implicit to compose as these are inferrable from the other arguments, and changes u_l_u_eq_u and l_u_l_eq_l to be applied rather than unapplied, which shortens both the proof and the places where the lemma is used.