-- 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 : Preadditive.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
x : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
inst_9 : L₁.HasMapBifunctor K₂ F
h :
  ∀ (n p q : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n),
    Eq (α :=
      (F.obj
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).X
                p)).obj
          (K₂.X q) ⟶
        X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)) n)
      (CategoryStruct.comp (Y :=
          X
            ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁).mapBifunctor
              K₂ F (ComplexShape.up ℤ))
            n)
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁).ιMapBifunctor
              K₂ F (ComplexShape.up ℤ) p q n h :
            (F.obj
                    ((Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                          K₁).X
                      p)).obj
                (K₂.X q) ⟶
              X
                ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      K₁).mapBifunctor
                  K₂ F (ComplexShape.up ℤ))
                n)
          (Hom.f
              (CategoryStruct.comp (Y :=
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      L₁).mapBifunctor
                  K₂ F (ComplexShape.up ℤ))
                (mapBifunctorMap
                    (CategoryTheory.Functor.map
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) f₁)
                    (𝟙 K₂) F (ComplexShape.up ℤ) :
                  Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                    ((Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                          K₁).mapBifunctor
                      K₂ F (ComplexShape.up ℤ))
                    ((Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                          L₁).mapBifunctor
                      K₂ F (ComplexShape.up ℤ)))
                (Iso.hom (L₁.mapBifunctorShift₁Iso K₂ F x) :
                  Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                    ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) L₁).mapBifunctor
                      K₂ F)
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                      (L₁.mapBifunctor K₂ F))))
              n :
            X
                ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      K₁).mapBifunctor
                  K₂ F (ComplexShape.up ℤ))
                n ⟶
              X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F))
                n) :
        (F.obj
                ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      K₁).X
                  p)).obj
            (K₂.X q) ⟶
          X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)) n)
      (CategoryStruct.comp (Y :=
          X
            ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁).mapBifunctor
              K₂ F (ComplexShape.up ℤ))
            n)
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁).ιMapBifunctor
              K₂ F (ComplexShape.up ℤ) p q n h :
            (F.obj
                    ((Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                          K₁).X
                      p)).obj
                (K₂.X q) ⟶
              X
                ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      K₁).mapBifunctor
                  K₂ F (ComplexShape.up ℤ))
                n)
          (Hom.f
              (CategoryStruct.comp (Y :=
                Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (K₁.mapBifunctor K₂ F))
                (Iso.hom (K₁.mapBifunctorShift₁Iso K₂ F x) :
                  Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                    ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
                      K₂ F)
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                      (K₁.mapBifunctor K₂ F)))
                (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                    (mapBifunctorMap f₁ (𝟙 K₂) F (ComplexShape.up ℤ)) :
                  Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                      (K₁.mapBifunctor K₂ F))
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                      (HomologicalComplex.mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)))))
              n :
            X
                ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      K₁).mapBifunctor
                  K₂ F (ComplexShape.up ℤ))
                n ⟶
              X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F))
                n) :
        (F.obj
                ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                      K₁).X
                  p)).obj
            (K₂.X q) ⟶
          X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)) n)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
      ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
            K₁).mapBifunctor
        K₂ F (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)))
    (CategoryStruct.comp (Y :=
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
              L₁).mapBifunctor
          K₂ F (ComplexShape.up ℤ))
        (mapBifunctorMap
            (CategoryTheory.Functor.map
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) f₁)
            (𝟙 K₂) F (ComplexShape.up ℤ) :
          Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
            ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁).mapBifunctor
              K₂ F (ComplexShape.up ℤ))
            ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  L₁).mapBifunctor
              K₂ F (ComplexShape.up ℤ)))
        (Iso.hom (L₁.mapBifunctorShift₁Iso K₂ F x) :
          Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) L₁).mapBifunctor K₂ F)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F))) :
      Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
        ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
              K₁).mapBifunctor
          K₂ F (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)))
    (CategoryStruct.comp (Y :=
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (K₁.mapBifunctor K₂ F))
        (Iso.hom (K₁.mapBifunctorShift₁Iso K₂ F x) :
          Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor K₂ F)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (K₁.mapBifunctor K₂ F)))
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (mapBifunctorMap f₁ (𝟙 K₂) F (ComplexShape.up ℤ)) :
          Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (K₁.mapBifunctor K₂ F))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
              (HomologicalComplex.mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)))) :
      Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
        ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor K₂ F)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
          (HomologicalComplex.mapBifunctor L₁ K₂ F (ComplexShape.up ℤ))))

Tactic:
ext n p q h