∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] (X : T × T)
  (X_1 : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).map
        ((CategoryTheory.NatIso.ofComponents
                (fun x =>
                  CategoryTheory.Iso.refl
                    ((CategoryTheory.Functor.id
                          (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X)).obj
                      x))
                ⋯).hom.app
          X_1))
      ((CategoryTheory.NatIso.ofComponents
              (fun x =>
                CategoryTheory.Iso.refl
                  (((CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse X).comp
                        (CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X)).obj
                    x))
              ⋯).hom.app
        ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj X_1)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj X_1)