∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_4, u_1} C] (D : Type u_3)
  [inst_1 : CategoryTheory.Category.{u_5, u_3} D] (E : Type u_2) [inst_2 : CategoryTheory.Category.{u_6, u_2} E]
  {X Y Z : C × D × E} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Prod.mkHom
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.comp f g).1
        (CategoryTheory.CategoryStruct.comp f g).2.1)
      (CategoryTheory.CategoryStruct.comp f g).2.2 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1 f.2.1) f.2.2)
      (CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom g.1 g.2.1) g.2.2)