-- 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
⊢ 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))
  (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))
Tactic: rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_leftDistrib_hom]