-- 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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
rw :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
        (X ◁ coprod.inr : tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
        (CategoryStruct.comp (Y :=
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
            (Iso.inv (∂L X Y Z) :
              tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ⟶
                coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
            (hom (∂L X Y Z) :
              coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
                tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
          tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
rw₁ :
  X ◁ coprod.inr ≫ 𝟙 (tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) =
    CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (coprod.inr :
        tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (hom (∂L X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
rw₂ :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (X ◁ coprod.inr : tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
            (X ◁ coprod.inr :
              tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
            (Iso.inv (∂L X Y Z) :
              tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ⟶
                coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)) :
          tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
have rw₃ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (X ◁ coprod.inr) (X ◁ coprod.inr)
Tactic: rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_leftDistrib_hom]