-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
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 : ℤ
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)
have w : 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
      (map (F.mapHomologicalComplex (ComplexShape.up ℤ))
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a b)) x) ≫
        CategoryStruct.comp (Y :=
          obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) b)
            (obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a) x))
          (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso b))
              (obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a) x) :
            Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
              (obj
                (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) b ⋙
                  F.mapHomologicalComplex (ComplexShape.up ℤ))
                (obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a) x))
              (obj
                (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                  shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) b)
                (obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a) x)))
          (map (shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) b)
                (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso a)) x) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) a b))
                (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x) :
            Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
              (obj
                (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                  shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) b)
                (obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a) x))
              (obj (shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (a + b))
                (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) 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)
Tactic: rw [CommShift.isoAdd_hom_app]