∀ {C₁ : Type u_8} {C₂ : Type u_6} {C₃ : Type u_1} {C₄ : Type u_3} {C₁₂ : Type u_10}
  [inst : CategoryTheory.Category.{u_7, u_8} C₁] [inst_1 : CategoryTheory.Category.{u_5, u_6} C₂]
  [inst_2 : CategoryTheory.Category.{u_4, u_1} C₃] [inst_3 : CategoryTheory.Category.{u_2, u_3} C₄]
  [inst_4 : CategoryTheory.Category.{u_9, u_10} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  {G G' : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} (φ : G ⟶ G') (X₁ : C₁) (X₂ Y₂ : C₂) (f : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.bifunctorComp₁₂ F₁₂ G).obj X₁).map f)
      { app := fun X₃ => (φ.app ((F₁₂.obj X₁).obj Y₂)).app X₃, naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp { app := fun X₃ => (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ }
      (((CategoryTheory.bifunctorComp₁₂ F₁₂ G').obj X₁).map f)