∀ (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 : C × D × E),
  CategoryTheory.Prod.mkHom
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X).1 (CategoryTheory.CategoryStruct.id X).2.1)
      (CategoryTheory.CategoryStruct.id X).2.2 =
    CategoryTheory.CategoryStruct.id ((X.1, X.2.1), X.2.2)