-- 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 : HasZeroMorphisms.{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.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₂ m : ℤ
hm₂ : m₂ = n₂ + y
hm : m = n + y
⊢ CategoryStruct.comp (Y :=
      X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
      (K₁.ιMapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F n₁ n₂ n
          h :
        (F.obj (K₁.X n₁)).obj
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂).X n₂) ⟶
          X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
      (Hom.f (Iso.hom (K₁.mapBifunctorShift₂Iso K₂ F y)) n :
        X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n ⟶
          X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F)) n) =
    HSMul.hSMul (β :=
      (F.obj (K₁.X n₁)).obj ((Functor.obj (shiftFunctor C₂ y) K₂).X n₂) ⟶
        X (Functor.obj (shiftFunctor D y) (K₁.mapBifunctor K₂ F)) n)
      (n₁ * y).negOnePow
      ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ Iso.inv (shiftFunctorObjXIso (K₁.mapBifunctor K₂ F) y n m hm))
have dsimp : CategoryStruct.comp (Y :=
    X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
    (K₁.ιMapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F n₁ n₂ n h :
      (F.obj (K₁.X n₁)).obj
          ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂).X n₂) ⟶
        X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
    (CategoryStruct.comp (Y :=
        X
          (HomologicalComplex₂.total
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            (ComplexShape.up ℤ))
          n)
        (Hom.f
            (HomologicalComplex₂.total.map (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y))
              (ComplexShape.up ℤ))
            n :
          X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n ⟶
            X
              (HomologicalComplex₂.total
                (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                (ComplexShape.up ℤ))
              n)
        (Hom.f
            (Iso.hom
              (HomologicalComplex₂.totalShift₂Iso
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)
                y))
            n :
          X
              (HomologicalComplex₂.total
                (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                (ComplexShape.up ℤ))
              n ⟶
            X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))
              n) :
      X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n ⟶
        X (K₁.mapBifunctor K₂ F) (n + y)) =
  HSMul.hSMul (β := (F.obj (K₁.X n₁)).obj (K₂.X (n₂ + y)) ⟶ X (K₁.mapBifunctor K₂ F) (n + y)) (n₁ * y).negOnePow
    ((F.obj (K₁.X n₁)).map (XIsoOfEq K₂ sorry).hom ≫
      K₁.ιMapBifunctor K₂ F n₁ m₂ m sorry ≫ Iso.inv (XIsoOfEq (K₁.mapBifunctor K₂ F) sorry))
Tactic: dsimp [mapBifunctorShift₂Iso]