-- 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 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
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₁).Additive
x y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
w :
  ∀ (a b : ℤ),
    Eq (α :=
      X
          (X
            (Functor.obj
              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
            a)
          b ⟶
        X
          (X
            (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            a)
          b)
      (Hom.f
          (Hom.f
            (CategoryStruct.comp (Y :=
              Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)))
              (CategoryStruct.comp (Y :=
                  Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂)))
                  (Iso.hom
                      (K₁.mapBifunctorHomologicalComplexShift₁Iso
                        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F x) :
                    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                      (Functor.obj
                        (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                          (Functor.obj
                            (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                            K₁))
                        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
                      (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))))
                  (CategoryTheory.Functor.map (HomologicalComplex₂.shiftFunctor₁ D x)
                      (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y)) :
                    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                      (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂)))
                      (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                        (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                          (Functor.obj
                            (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                            K₂)))) :
                Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                      (Functor.obj
                        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                    (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                      (Functor.obj
                        (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                        K₂))))
              (NatTrans.app (Iso.hom (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y))
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂) :
                Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y ⋙ HomologicalComplex₂.shiftFunctor₁ D x)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))))
            a)
          b :
        X
            (X
              (Functor.obj
                (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
              a)
            b ⟶
          X
            (X
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              a)
            b)
      (Hom.f
          (Hom.f
            (CategoryStruct.comp (Y :=
              Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj
                  (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                  K₂))
              (Iso.hom
                  ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x)
                        K₁).mapBifunctorHomologicalComplexShift₂Iso
                    K₂ F y) :
                Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                    (Functor.obj
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                      K₂)))
              (CategoryTheory.Functor.map (HomologicalComplex₂.shiftFunctor₂ D y)
                  (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x)) :
                Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                      K₂))
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                      (Functor.obj
                        (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                        K₂)))))
            a)
          b :
        X
            (X
              (Functor.obj
                (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
              a)
            b ⟶
          X
            (X
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              a)
            b)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
      (Functor.obj
        (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
      (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
        (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
          (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              K₂)))
        (CategoryStruct.comp (Y :=
            Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂)))
            (Iso.hom
                (K₁.mapBifunctorHomologicalComplexShift₁Iso
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F x) :
              Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                (Functor.obj
                  (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                    (Functor.obj
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
                (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))))
            (CategoryTheory.Functor.map (HomologicalComplex₂.shiftFunctor₁ D x)
                (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y)) :
              Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂)))
                (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                      K₂)))) :
          Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
            (Functor.obj
              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
            (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
              (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))))
        (NatTrans.app (Iso.hom (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y))
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              K₂) :
          Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y ⋙ HomologicalComplex₂.shiftFunctor₁ D x)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))) :
      Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
        (Functor.obj
          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
        (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj
            (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
            K₂))
        (Iso.hom
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x)
                  K₁).mapBifunctorHomologicalComplexShift₂Iso
              K₂ F y) :
          Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
            (Functor.obj
              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                K₂))
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj
                (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                K₂)))
        (CategoryTheory.Functor.map (HomologicalComplex₂.shiftFunctor₂ D y)
            (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x)) :
          Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj
                (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                K₂))
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)))) :
      Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, 0, 0} D (ComplexShape.up ℤ) (ComplexShape.up ℤ))
        (Functor.obj
          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂))
        (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              K₂))))

Tactic:
ext a b