-- 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
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
p q : ℤ
this :
  CategoryStruct.comp (Y :=
      obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
        (K₁.mapBifunctor (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F))
      (Iso.hom (K₁.mapBifunctorShift₁Iso (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F p) :
        Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
          ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor
            (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F)
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
            (K₁.mapBifunctor (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F)))
      (map (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p) (Iso.hom (K₁.mapBifunctorShift₂Iso K₂ F q)) :
        Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
            (K₁.mapBifunctor (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F))
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
            (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q) (K₁.mapBifunctor K₂ F)))) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
        ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor
          (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F)
        (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q) (K₁.mapBifunctor K₂ F))))
      (p * q).negOnePow
      (CategoryStruct.comp (Y :=
          obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
            ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor K₂ F))
          (Iso.hom ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctorShift₂Iso K₂ F q) :
            Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
              ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor
                (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F)
              (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
                ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor K₂ F)))
          (CategoryStruct.comp (Y :=
              obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
                (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p) (K₁.mapBifunctor K₂ F)))
              (map (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q) (Iso.hom (K₁.mapBifunctorShift₁Iso K₂ F p)) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
                    ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor K₂ F))
                  (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
                    (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p) (K₁.mapBifunctor K₂ F))))
              (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_3, u_3, 0} D ℤ) p q)) (K₁.mapBifunctor K₂ F) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (obj
                    (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p ⋙
                      shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
                    (K₁.mapBifunctor K₂ F))
                  (obj
                    (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q ⋙
                      shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
                    (K₁.mapBifunctor K₂ F))) :
            Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
              (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
                ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor K₂ F))
              (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
                (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q) (K₁.mapBifunctor K₂ F)))) :
        Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
          ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctor
            (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F)
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
            (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q) (K₁.mapBifunctor K₂ F))))
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
      (obj
        (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q ⋙
          obj F.map₂CochainComplex (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁))
        K₂)
      (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
        (obj (obj (Functor.flip F.map₂CochainComplex) K₂ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p) K₁)))
    (CategoryStruct.comp (Y :=
      obj
        (obj F.map₂CochainComplex (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁) ⋙
          shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
        K₂)
      (NatTrans.app
        (Iso.hom
          (commShiftIso (obj F.map₂CochainComplex (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁)) q))
        K₂)
      (map (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
        (NatTrans.app (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) p)) K₁)))
    (NatTrans.app
        (Iso.hom
          (commShiftIso
            (obj (Functor.flip F.map₂CochainComplex) (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂)) p))
        K₁ ≫
      map (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
          (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) q)) K₂) ≫
        Iso.inv (shiftComm (obj (obj F.map₂CochainComplex K₁) K₂) p q) ≫
          CatCenter.app (↑(CommShift₂Setup.ε CommShift₂Setup.int p q) : CatCenter (CochainComplex D ℤ))
            (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q)
              (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p) (obj (obj F.map₂CochainComplex K₁) K₂))))

Tactic:
simp [commShiftIso_map₂CochainComplex_hom_app,
      commShiftIso_map₂CochainComplex_flip_hom_app,
      reassoc_of% this, smul_smul]

Premises used: CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app, smul_smul, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app