-- 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 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f₁ : K₁ ⟶ L₁
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₁).PreservesZeroMorphisms
x : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
i j : ℤ
h : (ComplexShape.up ℤ).Rel i j
i_1 : ℤ
⊢ Eq (α :=
    X
        (X
          (Functor.obj
            (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                K₁))
            K₂)
          i)
        i_1 ⟶
      X
        (X
          (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              K₂))
          j)
        i_1)
    (Hom.f
      (Iso.hom
          ((fun (x_1 : ℤ) ↦
              (Iso.refl
                  (X
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                      K₂)
                    x_1) :
                Iso (C := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                  (X
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                      K₂)
                    x_1)
                  (X
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                      K₂)
                    x_1)))
            i) ≫
        d
          (Functor.obj (HomologicalComplex₂.shiftFunctor₁ D x)
            (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
              K₂))
          i j)
      i_1)
    (Hom.f
      (d
          (Functor.obj
            (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                K₁))
            K₂)
          i j ≫
        Iso.hom
          ((fun (x_1 : ℤ) ↦
              (Iso.refl
                  (X
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                      K₂)
                    x_1) :
                Iso (C := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                  (X
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                      K₂)
                    x_1)
                  (X
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ))
                        (Functor.obj
                          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁))
                      K₂)
                    x_1)))
            j))
      i_1)
have h : 𝟙 ((F.obj (K₁.X (i + x))).obj (K₂.X i_1)) ≫
    HSMul.hSMul (β := (F.obj (K₁.X (i + x))).obj (K₂.X i_1) ⟶ (F.obj (K₁.X (j + x))).obj (K₂.X i_1)) x.negOnePow
      (NatTrans.app (F.map (K₁.d (i + x) (j + x))) (K₂.X i_1)) =
  (F.map (HSMul.hSMul (β := K₁.X (i + x) ⟶ K₁.X (j + x)) x.negOnePow (K₁.d (i + x) (j + x)))).app (K₂.X i_1) ≫
    𝟙 ((F.obj (K₁.X (j + x))).obj (K₂.X i_1))
Tactic: dsimp