-- 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
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)
rw₁ :
  coprod.inr ▷ 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)
rw₂ :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ 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))
        (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)
⊢ 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)
  (coprod.inr ▷ X) (coprod.inr ▷ X)
Tactic: rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_rightDistrib_hom]