-- Module: Mathlib.Algebra.Homology.BifunctorShift
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
i j : ℤ
h_1 : (ComplexShape.up ℤ).Rel i j
h :
  ∀ (i_1 : ℤ),
    Eq (α :=
      X
          (X
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                K₂))
            i)
          i_1 ⟶
        X
          (X
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            j)
          i_1)
      (Hom.f
        (Iso.hom
            ((fun (i₁ : ℤ) ↦
                (Hom.isoOfComponents
                    (fun (x : ℤ) ↦
                      Iso.refl
                        (X
                          (X
                            (Functor.obj
                              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                                K₁)
                              (Functor.obj
                                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ))
                                  y)
                                K₂))
                            i₁)
                          x))
                    ⋯ :
                  Iso (C := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                    (X
                      (Functor.obj
                        (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
                      i₁)
                    (X
                      (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          K₂))
                      i₁)))
              i) ≫
          d
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            i j)
        i_1)
      (Hom.f
        (d
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                K₂))
            i j ≫
          Iso.hom
            ((fun (i₁ : ℤ) ↦
                (Hom.isoOfComponents
                    (fun (x : ℤ) ↦
                      Iso.refl
                        (X
                          (X
                            (Functor.obj
                              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                                K₁)
                              (Functor.obj
                                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ))
                                  y)
                                K₂))
                            i₁)
                          x))
                    ⋯ :
                  Iso (C := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                    (X
                      (Functor.obj
                        (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
                      i₁)
                    (X
                      (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          K₂))
                      i₁)))
              j))
        i_1)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
      (X
        (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
        i)
      (X
        (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
        j))
    (Iso.hom
        ((fun (i₁ : ℤ) ↦
            (Hom.isoOfComponents
                (fun (x : ℤ) ↦
                  Iso.refl
                    (X
                      (X
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          (Functor.obj
                            (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                            K₂))
                        i₁)
                      x))
                ⋯ :
              Iso (C := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                (X
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                    (Functor.obj
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
                  i₁)
                (X
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  i₁)))
          i) ≫
      d
        (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
        i j)
    (d
        (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
        i j ≫
      Iso.hom
        ((fun (i₁ : ℤ) ↦
            (Hom.isoOfComponents
                (fun (x : ℤ) ↦
                  Iso.refl
                    (X
                      (X
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          (Functor.obj
                            (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                            K₂))
                        i₁)
                      x))
                ⋯ :
              Iso (C := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                (X
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                    (Functor.obj
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
                  i₁)
                (X
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  i₁)))
          j))

Tactic:
ext