-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : c.π c c (c.next i₁, i₂) = j
pos :
  HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (d (tensorUnit C c) i₁ (c.next i₁))) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₁ :
  HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) 0) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₂ :
  HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app 0 (K.X i₂) ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₃ :
  HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂)) (0 ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₄ :
  HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂)) 0 =
    0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0
have pos₅ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
    X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
  0 0
Tactic: rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, zero_comp, smul_zero]