∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_1, u_5} C] {D : Type u_7}
  [inst_1 : CategoryTheory.Category.{u_3, u_7} D] {C' : Type u_6} [inst_2 : CategoryTheory.Category.{u_2, u_6} C']
  {D' : Type u_8} [inst_3 : CategoryTheory.Category.{u_4, u_8} D'] (S : CategoryTheory.Functor C D)
  (S' : CategoryTheory.Functor C' D') (T : D) (T' : D') (X : CategoryTheory.CostructuredArrow (S.prod S') (T, T')),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.prodFunctor S S' T T').map
        ((CategoryTheory.NatIso.ofComponents
                (fun f =>
                  CategoryTheory.Iso.refl
                    ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow (S.prod S') (T, T'))).obj f))
                ⋯).hom.app
          X))
      ((CategoryTheory.NatIso.ofComponents
              (fun f =>
                CategoryTheory.Iso.refl
                  (((CategoryTheory.CostructuredArrow.prodInverse S S' T T').comp
                        (CategoryTheory.CostructuredArrow.prodFunctor S S' T T')).obj
                    f))
              ⋯).hom.app
        ((CategoryTheory.CostructuredArrow.prodFunctor S S' T T').obj X)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.CostructuredArrow.prodFunctor S S' T T').obj X)