-- 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 : ℤ
⊢ Iso.hom
      (Iso.trans (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))
        (K₁.mapBifunctorShift₁Iso (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) q) K₂) F p :
          Iso (C := 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)))
        (mapIso (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p) (K₁.mapBifunctorShift₂Iso K₂ F q) :
          Iso (C := 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 (β :=
        Iso (C := 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 ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
            (K₁.mapBifunctor K₂ F)))
        (p * q).negOnePow
        (Iso.trans (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))
            ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) p) K₁).mapBifunctorShift₂Iso K₂ F q :
              Iso (C := 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)))
            (Iso.trans (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)))
                (mapIso (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) q) (K₁.mapBifunctorShift₁Iso K₂ F p) :
                  Iso (C := 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))))
                (Iso.app (shiftFunctorComm (CochainComplex.{v_3, u_3, 0} D ℤ) p q) (K₁.mapBifunctor K₂ F) :
                  Iso (C := 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))) :
              Iso (C := 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 ⋙
                    shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
                  (K₁.mapBifunctor K₂ F))) :
          Iso (C := 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 ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) p)
              (K₁.mapBifunctor K₂ F)))).hom

Tactic:
have := congr_arg Iso.hom
      (CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso K₁ K₂ F p q)