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