∀ {X Y : CompleteLat} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CompleteLat.dual.comp CompleteLat.dual).map f)
      ((fun X => CompleteLat.Iso.mk (OrderIso.dualDual ↑X)) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun X => CompleteLat.Iso.mk (OrderIso.dualDual ↑X)) X).hom
      ((CategoryTheory.Functor.id CompleteLat).map f)