∀ (J : Type u_2) (C : Type u_4) [inst : CategoryTheory.Category.{u_1, u_2} J]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (x : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) {X Y : J} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.id (CategoryTheory.ShortComplex (CategoryTheory.Functor J C))).obj x).X₁.map f)
      ((fun x_1 =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.Functor.id (CategoryTheory.ShortComplex (CategoryTheory.Functor J C))).obj x).X₁.obj
                x_1))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x_1 =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.Functor.id (CategoryTheory.ShortComplex (CategoryTheory.Functor J C))).obj x).X₁.obj
                x_1))
          X).hom
      ((((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).comp
                  (CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C)).obj
              x).X₁.map
        f)