∀ {X Y : CategoryTheory.Cat} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Cat.opFunctor.comp CategoryTheory.Cat.opFunctor).map f)
      ((fun C =>
            { hom := (CategoryTheory.unopUnop ↑C).toCatHom, inv := (CategoryTheory.opOp ↑C).toCatHom, hom_inv_id := ⋯,
              inv_hom_id := ⋯ })
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun C =>
            { hom := (CategoryTheory.unopUnop ↑C).toCatHom, inv := (CategoryTheory.opOp ↑C).toCatHom, hom_inv_id := ⋯,
              inv_hom_id := ⋯ })
          X).hom
      ((CategoryTheory.Functor.id CategoryTheory.Cat).map f)