-- 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
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
w :
  Eq (α :=
    HomologicalComplex.X
        (obj
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          x)
        i ⟶
      HomologicalComplex.X
        (obj
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
          x)
        i)
    (HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso 0)) x) i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)
    (HomologicalComplex.Hom.f
        (map (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ℤ)) x) ≫
          NatTrans.app (Iso.inv (shiftFunctorZero (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) ℤ))
            (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)
⊢ Eq (α :=
    HomologicalComplex.X
        (obj
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          x)
        i ⟶
      HomologicalComplex.X
        (obj
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
          x)
        i)
    (HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso 0)) x) i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)
    (HomologicalComplex.Hom.f
        (NatTrans.app (Iso.hom (CommShift.isoZero (F.mapHomologicalComplex (ComplexShape.up ℤ)) ℤ)) x) i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)

Tactic:
rw [CommShift.isoZero_hom_app]

Premises used: CategoryTheory.Functor.CommShift.isoZero_hom_app