∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (X_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).map
        ((CategoryTheory.NatIso.ofComponents
                (fun x =>
                  CategoryTheory.Iso.refl
                    ((CategoryTheory.Functor.id
                          (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X)).obj
                      x))
                ⋯).hom.app
          X_1))
      ((CategoryTheory.NatIso.ofComponents
              (fun x =>
                CategoryTheory.Iso.refl
                  (((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).comp
                        (CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X)).obj
                    x))
              ⋯).hom.app
        ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj X_1)) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj X_1)