-- 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 : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
x : X ⟶ Y
h :
  ∀ (i : ℤ),
    Eq (α :=
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            X)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
            Y)
          i)
      (HomologicalComplex.Hom.f
        (map
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x ≫
          Iso.hom
            ((fun (K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ↦
                (HomologicalComplex.Hom.isoOfComponents
                    (fun (x : ℤ) ↦
                      Iso.refl
                        (HomologicalComplex.X
                          (obj
                            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                              F.mapHomologicalComplex (ComplexShape.up ℤ))
                            K)
                          x))
                    ⋯ :
                  Iso (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                    (obj
                      (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ))
                      K)
                    (obj
                      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                        shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
                      K)))
              Y))
        i)
      (HomologicalComplex.Hom.f
        (Iso.hom
            ((fun (K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ↦
                (HomologicalComplex.Hom.isoOfComponents
                    (fun (x : ℤ) ↦
                      Iso.refl
                        (HomologicalComplex.X
                          (obj
                            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                              F.mapHomologicalComplex (ComplexShape.up ℤ))
                            K)
                          x))
                    ⋯ :
                  Iso (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                    (obj
                      (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ))
                      K)
                    (obj
                      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                        shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
                      K)))
              X) ≫
          map
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
            x)
        i)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
      (obj
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
          F.mapHomologicalComplex (ComplexShape.up ℤ))
        X)
      (obj
        (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
        Y))
    (map
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
          F.mapHomologicalComplex (ComplexShape.up ℤ))
        x ≫
      Iso.hom
        ((fun (K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ↦
            (HomologicalComplex.Hom.isoOfComponents
                (fun (x : ℤ) ↦
                  Iso.refl
                    (HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x))
                ⋯ :
              Iso (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                (obj
                  (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                    F.mapHomologicalComplex (ComplexShape.up ℤ))
                  K)
                (obj
                  (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                    shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
                  K)))
          Y))
    (Iso.hom
        ((fun (K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ↦
            (HomologicalComplex.Hom.isoOfComponents
                (fun (x : ℤ) ↦
                  Iso.refl
                    (HomologicalComplex.X
                      (obj
                        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                          F.mapHomologicalComplex (ComplexShape.up ℤ))
                        K)
                      x))
                ⋯ :
              Iso (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                (obj
                  (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                    F.mapHomologicalComplex (ComplexShape.up ℤ))
                  K)
                (obj
                  (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                    shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
                  K)))
          X) ≫
      map
        (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
        x)

Tactic:
ext