∀ {C : Type u_10} [inst : CategoryTheory.Category.{u_9, u_10} C] {D : Type u_12}
  [inst_1 : CategoryTheory.Category.{u_11, u_12} D] {A : Type u_4} [inst_2 : CategoryTheory.Category.{u_3, u_4} A]
  {B : Type u_2} [inst_3 : CategoryTheory.Category.{u_1, u_2} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {C' : Type u_6} [inst_4 : CategoryTheory.Category.{u_5, u_6} C'] {D' : Type u_8}
  [inst_5 : CategoryTheory.Category.{u_7, u_8} D'] {L'' : D'} {R'' : CategoryTheory.Functor C' D'}
  {F' : CategoryTheory.Functor C' C} {G' : CategoryTheory.Functor D' D} (α' : L ⟶ G'.obj L'')
  (β' : R''.comp G' ⟶ F'.comp R) (X : CategoryTheory.StructuredArrow L'' R''),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.StructuredArrow.map₂ α' β').comp (CategoryTheory.StructuredArrow.map₂ α β)).obj X).hom
      (R'.map
        (CategoryTheory.Iso.refl
            (((CategoryTheory.StructuredArrow.map₂ α' β').comp (CategoryTheory.StructuredArrow.map₂ α β)).obj
                X).right).hom) =
    ((CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.comp α (G.map α'))
            (CategoryTheory.CategoryStruct.comp (R''.associator G' G).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G)
                (CategoryTheory.CategoryStruct.comp (F'.associator R G).hom
                  (CategoryTheory.CategoryStruct.comp (F'.whiskerLeft β) (F'.associator F R').inv))))).obj
        X).hom