-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
a b : ℤ
w :
  ∀ (x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (i : ℤ),
    Eq (α :=
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (a + b) ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b))
            x)
          i)
      (HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso (a + b))) x) i :
        HomologicalComplex.X
            (obj
              (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (a + b) ⋙
                F.mapHomologicalComplex (ComplexShape.up ℤ))
              x)
            i ⟶
          HomologicalComplex.X
            (obj
              (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b))
              x)
            i)
      (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapCochainComplexShiftIso a) (F.mapCochainComplexShiftIso b))) x)
          i :
        HomologicalComplex.X
            (obj
              (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (a + b) ⋙
                F.mapHomologicalComplex (ComplexShape.up ℤ))
              x)
            i ⟶
          HomologicalComplex.X
            (obj
              (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b))
              x)
            i)
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) ⥤ HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
      (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (a + b) ⋙
        F.mapHomologicalComplex (ComplexShape.up ℤ))
      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b)))
    (F.mapCochainComplexShiftIso (a + b) :
      Iso (C :=
        HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) ⥤ HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (a + b) ⋙
          F.mapHomologicalComplex (ComplexShape.up ℤ))
        (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b)))
    (CommShift.isoAdd (F.mapCochainComplexShiftIso a) (F.mapCochainComplexShiftIso b) :
      Iso (C :=
        HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) ⥤ HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (a + b) ⋙
          F.mapHomologicalComplex (ComplexShape.up ℤ))
        (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b)))

Tactic:
ext