-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (hypothesis)
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 : ℤ
⊢ 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₂))))
have this : 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)