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