∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ]
  {X Y : (CategoryTheory.ShortComplex C)ᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShortComplex.leftHomologyFunctor C).op.map f)
      ((fun S => (Opposite.unop S).rightHomologyOpIso.symm) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun S => (Opposite.unop S).rightHomologyOpIso.symm) X).hom
      (((CategoryTheory.ShortComplex.opFunctor C).comp (CategoryTheory.ShortComplex.rightHomologyFunctor Cᵒᵖ)).map f)