∀ {C₁ : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C₁] [inst_1 : CategoryTheory.Abelian C₁] {C₂ : Type u_4}
  [inst_2 : CategoryTheory.Category.{u_3, u_4} C₂] [inst_3 : CategoryTheory.Abelian C₂]
  (F : CategoryTheory.Functor C₁ C₂) [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F],
  autoParam
    (∀ (a b : ℤ),
      CategoryTheory.Functor.instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism._aux_1
          F (a + b) =
        CategoryTheory.Functor.CommShift.isoAdd
          (CategoryTheory.Functor.instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism._aux_1
            F a)
          (CategoryTheory.Functor.instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism._aux_1
            F b))
    CategoryTheory.Functor.CommShift.commShiftIso_add._autoParam