-- 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
n : ℤ
K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      Eq (α :=
        HomologicalComplex.X
            (obj
              (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                F.mapHomologicalComplex (ComplexShape.up ℤ))
              K)
            i ⟶
          HomologicalComplex.X
            (obj
              (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
              K)
            j)
        (Iso.hom
            ((fun (x : ℤ) ↦
                (Iso.refl
                    (HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x) :
                  HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x ≅
                    HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x))
              i) ≫
          HomologicalComplex.d
            (obj
              (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
              K)
            i j)
        (HomologicalComplex.d
            (obj
              (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                F.mapHomologicalComplex (ComplexShape.up ℤ))
              K)
            i j ≫
          Iso.hom
            ((fun (x : ℤ) ↦
                (Iso.refl
                    (HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x) :
                  HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x ≅
                    HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x))
              j))

Tactic:
simp