-- 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 : SymmetricCategory.{v, u_1} C
inst_4 : IsMonoidalDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    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)
    (∂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)
    (Iso.trans (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.mapIso (β_ Y X) (β_ Z X) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ≅
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (Iso.trans (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
            (∂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))
            (β_ X (coprod.{v, u_1} Y Z) :
              tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ≅
                tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X 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) (coprod.{v, u_1} Y Z) X)
have w : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Y 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.inl :
        tensorObj.{v, u_1} (𝒞 := inst) Y 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) Y 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.inl
      (hom
        (Iso.trans (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
          (coprod.mapIso (β_ Y X) (β_ Z X) :
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ≅
              coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
          (Iso.trans (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
              (∂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))
              (β_ X (coprod.{v, u_1} Y Z) :
                tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ≅
                  tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ≅
              tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X))) :
    tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
Tactic: ext