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