-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (goal)
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
⊢ CategoryStruct.comp (Y :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
        (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F))
      (CategoryStruct.comp (Y :=
          HomologicalComplex₂.total
            (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₂)))
            (ComplexShape.up ℤ))
          (HomologicalComplex₂.total.map
              (Iso.hom
                (K₁.mapBifunctorHomologicalComplexShift₁Iso
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F x))
              (ComplexShape.up ℤ) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
              (HomologicalComplex₂.total
                (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₂))
                (ComplexShape.up ℤ))
              (HomologicalComplex₂.total
                (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₂)))
                (ComplexShape.up ℤ)))
          (Iso.hom
              (HomologicalComplex₂.totalShift₁Iso
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂))
                x) :
            Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
              (HomologicalComplex₂.total
                (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₂)))
                (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂)
                  F))) :
        Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
          ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)))
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
          (CategoryStruct.comp (Y :=
            HomologicalComplex₂.total
              (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              (ComplexShape.up ℤ))
            (HomologicalComplex₂.total.map (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y))
                (ComplexShape.up ℤ) :
              Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                (HomologicalComplex₂.total
                  (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₂))
                  (ComplexShape.up ℤ))
                (HomologicalComplex₂.total
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  (ComplexShape.up ℤ)))
            (Iso.hom
                (HomologicalComplex₂.totalShift₂Iso
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
                  y) :
              Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                (HomologicalComplex₂.total
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  (ComplexShape.up ℤ))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                  (K₁.mapBifunctor K₂ F)))) :
        Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F)))) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
        ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))))
      (x * y).negOnePow
      (CategoryStruct.comp (Y :=
          Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor K₂ F))
          (CategoryStruct.comp (Y :=
              HomologicalComplex₂.total
                (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₂))
                (ComplexShape.up ℤ))
              (HomologicalComplex₂.total.map
                  (Iso.hom
                    ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x)
                          K₁).mapBifunctorHomologicalComplexShift₂Iso
                      K₂ F y))
                  (ComplexShape.up ℤ) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                  (HomologicalComplex₂.total
                    (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₂))
                    (ComplexShape.up ℤ))
                  (HomologicalComplex₂.total
                    (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₂))
                    (ComplexShape.up ℤ)))
              (Iso.hom
                  (HomologicalComplex₂.totalShift₂Iso
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁))
                      K₂)
                    y) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (HomologicalComplex₂.total
                    (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₂))
                    (ComplexShape.up ℤ))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
                      K₂ F))) :
            Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
              ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor K₂
                  F)))
          (CategoryStruct.comp (Y :=
              Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                (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 ℤ) y)
                  (CategoryStruct.comp (Y :=
                    HomologicalComplex₂.total
                      (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                        (Functor.obj
                          (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                          K₂))
                      (ComplexShape.up ℤ))
                    (HomologicalComplex₂.total.map (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x))
                        (ComplexShape.up ℤ) :
                      Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                        (HomologicalComplex₂.total
                          (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₁))
                            K₂)
                          (ComplexShape.up ℤ))
                        (HomologicalComplex₂.total
                          (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                            (Functor.obj
                              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                                K₁)
                              K₂))
                          (ComplexShape.up ℤ)))
                    (Iso.hom
                        (HomologicalComplex₂.totalShift₁Iso
                          (Functor.obj
                            (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                            K₂)
                          x) :
                      Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                        (HomologicalComplex₂.total
                          (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                            (Functor.obj
                              (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                                K₁)
                              K₂))
                          (ComplexShape.up ℤ))
                        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                          (K₁.mapBifunctor K₂ F)))) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    ((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 ℤ) y)
                    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                      (K₁.mapBifunctor K₂ F))))
              (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_3, u_3, 0} D ℤ) x y)) (K₁.mapBifunctor K₂ F) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    (K₁.mapBifunctor K₂ F))
                  (Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                    (K₁.mapBifunctor K₂ F))) :
            Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                ((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)
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                  (K₁.mapBifunctor K₂ F)))) :
        Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
          ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))))
have w : Eq (α :=
  Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
    ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))))
  (CategoryStruct.comp (Y :=
      HomologicalComplex₂.total
        (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
        (ComplexShape.up ℤ))
      (HomologicalComplex₂.total.map
          (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₂))))
          (ComplexShape.up ℤ) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
          (HomologicalComplex₂.total
            (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₂))
            (ComplexShape.up ℤ))
          (HomologicalComplex₂.total
            (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            (ComplexShape.up ℤ)))
      (CategoryStruct.comp (Y :=
          Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ)) y)
            (HomologicalComplex₂.total
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              (ComplexShape.up ℤ)))
          (Iso.hom
            (HomologicalComplex₂.totalShift₂Iso
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              y))
          (CategoryTheory.Functor.map
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ)) y)
              (Iso.hom
                (HomologicalComplex₂.totalShift₁Iso
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
                  x)) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_3, u_3, 0} D ℤ) x y))
              (HomologicalComplex₂.total
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)
                (ComplexShape.up ℤ))) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
          (HomologicalComplex₂.total
            (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x ⋙ HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            (ComplexShape.up ℤ))
          (Functor.obj
            (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y ⋙
              CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (HomologicalComplex₂.total
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂)
              (ComplexShape.up ℤ)))) :
    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
      (HomologicalComplex₂.total
        (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₂))
        (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))))
  (CategoryStruct.comp (Y :=
      HomologicalComplex₂.total
        (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
          (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              K₂)))
        (ComplexShape.up ℤ))
      (HomologicalComplex₂.total.map
          (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₂)))))
          (ComplexShape.up ℤ) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
          (HomologicalComplex₂.total
            (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₂))
            (ComplexShape.up ℤ))
          (HomologicalComplex₂.total
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)))
            (ComplexShape.up ℤ)))
      (CategoryStruct.comp (Y :=
          Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ)) y)
            (HomologicalComplex₂.total
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              (ComplexShape.up ℤ)))
          (Iso.hom
            (HomologicalComplex₂.totalShift₂Iso
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              y))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
              (Iso.hom
                (HomologicalComplex₂.totalShift₁Iso
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
                  x)) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_3, u_3, 0} D ℤ) x y)) (K₁.mapBifunctor K₂ F)) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
          (HomologicalComplex₂.total
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)))
            (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F)))) :
    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
      (HomologicalComplex₂.total
        (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₂))
        (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))))
Tactic: rw [Functor.map_comp, Functor.map_comp, assoc, assoc, assoc,
    ← HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc,
    HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom,
    ← HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc,
    Linear.comp_units_smul, Linear.comp_units_smul,
    smul_left_cancel_iff,
    ← HomologicalComplex₂.total.map_comp_assoc,
    ← HomologicalComplex₂.total.map_comp_assoc,
    ← HomologicalComplex₂.total.map_comp_assoc]