awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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
apply :
  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))
⊢ Eq.{v + 1} (α :=
    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))
    (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))
    (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))

Tactic:
apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp

Premises used: CategoryTheory.leftDistrib, CategoryTheory.Iso.cancel_iso_hom_right, Iff.mp
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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} (α :=
    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)
    (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)
    (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ 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)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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) 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
      (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)))
    (coprod.inl ▷ X)
rw₁ rw₂ :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (coprod.inl ▷ X) (coprod.inl ▷ X)
⊢ 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)
    (coprod.inl ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)

Tactic:
rw [rightDistrib_hom, coprod.inl_desc]

Premises used: CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.rightDistrib_hom
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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 :=
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) coprod.inr
      (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)))
    (coprod.inr ▷ X)
rw₁ 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)
⊢ 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))
        (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)
    (coprod.inr ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)

Tactic:
rw [rightDistrib_hom, coprod.inr_desc]

Premises used: CategoryTheory.Limits.coprod.inr_desc, CategoryTheory.rightDistrib_hom
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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
apply :
  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))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
            (coprod.inl ▷ X :
              tensorObj.{v, u_1} (𝒞 := inst) Y 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) 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 :
          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)
⊢ Eq.{v + 1} (α :=
    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))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
        (coprod.inl ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Y 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) Y X ⟶
        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))

Tactic:
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp

Premises used: CategoryTheory.Iso.cancel_iso_hom_right, Iff.mp, CategoryTheory.rightDistrib
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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
apply :
  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)
⊢ Eq.{v + 1} (α :=
    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))
    (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))
    (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))

Tactic:
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp

Premises used: CategoryTheory.Iso.cancel_iso_hom_right, Iff.mp, CategoryTheory.rightDistrib
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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 : BraidedCategory.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    coprod.{v, u_1} (Functor.obj.{v, v, u_1, u_1} (tensorLeft X) Y) (Functor.obj.{v, v, u_1, u_1} (tensorLeft X) Z) ⟶
      tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (coprodComparison (tensorLeft X) Y Z ≫ hom (β_ X (coprod.{v, u_1} Y Z)))
    (CategoryStruct.comp (Y :=
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (coprod.map (hom (β_ X Y)) (hom (β_ X Z))) (coprodComparison (tensorRight X) Y Z))

Tactic:
simp [coprodComparison]

Premises used: CategoryTheory.Limits.coprodComparison
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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
X Y Z : C
⊢ Eq.{v + 1} (α :=
    coprod.{v, u_1} (Functor.obj.{v, v, u_1, u_1} (tensorRight X) Y) (Functor.obj.{v, v, u_1, u_1} (tensorRight X) Z) ⟶
      tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (coprodComparison (tensorRight X) Y Z ≫ hom (β_ (coprod.{v, u_1} Y Z) X))
    (CategoryStruct.comp (Y :=
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (coprod.map (hom (β_ Y X)) (hom (β_ Z X))) (coprodComparison (tensorLeft X) Y Z))

Tactic:
simp [coprodComparison]

Premises used: CategoryTheory.Limits.coprodComparison
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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} (α := 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:
simp [leftDistrib_hom, rightDistrib_hom]

Premises used: CategoryTheory.leftDistrib_hom, CategoryTheory.rightDistrib_hom
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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} (α := 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)
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) coprod.inr
        (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) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)

Tactic:
simp [leftDistrib_hom, rightDistrib_hom]

Premises used: CategoryTheory.leftDistrib_hom, CategoryTheory.rightDistrib_hom
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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 : MonoidalClosed.{v, u_1} C
X : C
⊢ PreservesColimitsOfShape.{0, 0, v, v, u_1, u_1} (Discrete WalkingPair) (tensorLeft X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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 : MonoidalClosed.{v, u_1} C
⊢ IsMonoidalDistrib.{v, u_1} C

Tactic:
apply SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib

Premises used: CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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 : MonoidalClosed.{v, u_1} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    coprod.{v, u_1} Y Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (curry (Iso.inv (∂L X Y Z)) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (coprod.desc (curry coprod.inl) (curry coprod.inr) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
⊢ Eq.{v + 1} (α :=
    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))
    (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))
    (uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      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))

Tactic:
rw [← curry_eq_iff]

Premises used: CategoryTheory.MonoidalClosed.curry_eq_iff