∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] ⦃X Y : C × D⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (C × D)).map f) (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X)
      (((CategoryTheory.Prod.swap C D).comp (CategoryTheory.Prod.swap D C)).map f)