∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_6, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_7, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_8, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_9, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E)
  (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F₁.curry₃ObjProdComp F₂ F₃ G).inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.Functor.curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X_1).obj X_2)