-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : IsMonoidalRightDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
            (coprod.inr ▷ X :
              tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
            (Iso.inv (∂R X Y Z) :
              tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
                coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) :
          tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (hom (∂R X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
      tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (hom (∂R X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
      tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
have rw : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
      (coprod.inr ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
      (CategoryStruct.comp (Y :=
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
          (Iso.inv (∂R X Y Z) :
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
              coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
          (hom (∂R X Y Z) :
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
              tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
        tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
    tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (coprod.inr :
        tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (hom (∂R X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
    tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
Tactic: rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_rightDistrib_hom]