∀ (X Y : CategoryTheory.Cat) (x : CategoryTheory.Limits.BinaryFan X Y),
  CategoryTheory.CategoryStruct.comp (x.fst.toFunctor.prod' x.snd.toFunctor).toCatHom
      (CategoryTheory.Prod.fst ↑X ↑Y).toCatHom =
    CategoryTheory.CategoryStruct.comp (x.fst.toFunctor.prod' x.snd.toFunctor).toCatHom
      (CategoryTheory.Prod.fst ↑X ↑Y).toCatHom