-- 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)
      (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₂ ⋯).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ Iso.inv (XIsoOfEq (K₁.mapBifunctor K₂ F) ⋯))
have simp : Hom.f (Hom.f (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y)) n₁) n₂ ≫
    HSMul.hSMul (β :=
      X
          (X
            (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂))
            n₁)
          n₂ ⟶
        X
          (Functor.obj (shiftFunctor D y)
            (HomologicalComplex₂.total
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂)
              (ComplexShape.up ℤ)))
          n)
      (n₁ * y).negOnePow
      (Iso.hom
          (HomologicalComplex₂.shiftFunctor₂XXIso
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
            n₁ n₂ y m₂ hm₂) ≫
        HomologicalComplex₂.ιTotal
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
            (ComplexShape.up ℤ) n₁ m₂ m sorry ≫
          Iso.inv
            (shiftFunctorObjXIso
              (HomologicalComplex₂.total
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)
                (ComplexShape.up ℤ))
              y n m hm)) =
  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: simp only [HomologicalComplex₂.ιTotal_map_assoc,
    HomologicalComplex₂.ι_totalShift₂Iso_hom_f _ _ _ _ _ _ _ hm₂ _ hm]