awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight W)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight W) (tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.right) ⟶
      (X₁ □ Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left W) (X₂.hom ▷ W)).right)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight W)
        (pushout (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (map (tensorRight W) (pushout.inr (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (Iso.hom
          (Iso.trans (Y :=
            pushout (X := obj.{v, v, u, u} (tensorRight W) (tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left))
              (map (tensorRight W) (X₁.hom ▷ X₂.left)) (map (tensorRight W) (X₁.left ◁ X₂.hom)))
            (IsPushout.isoPushout ⋯)
            (HasColimit.isoOfNatIso
              (spanExt (α_ X₁.left X₂.left W) (α_ X₁.right X₂.left W) (α_ X₁.left X₂.right W) ⋯ ⋯))) ≫
        (X₁ □ Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left W) (X₂.hom ▷ W)).hom))
    (map (tensorRight W) (pushout.inr (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) (X₁ □ X₂).left W) ((X₁ □ X₂).hom ▷ W)).hom ≫
        Iso.hom (α_ X₁.right X₂.right W))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
F : Functor.{v, v, u, u} C C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) F
⊢ PreservesColimit
    (span (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
      (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    F

Tactic:
simpa only [curriedTensor_obj_obj, curriedTensor_map_app, curriedTensor_obj_map]

Premises used: CategoryTheory.MonoidalCategory.curriedTensor_obj_map, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.MonoidalCategory.curriedTensor_map_app
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
refine_1 : ((X₁ □ X₂) □ X₃).left ≅ (X₁ □ X₂ □ X₃).left
refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃

Tactic:
refine Arrow.isoMk ?_ (α_ _ _ _) ?_

Premises used: CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X₁.left)
        (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.right) (X₂.hom ▷ X₃.right)).left ⟶
      (X₁ □ X₂ □ X₃).left)
    (NatTrans.app (map (curriedTensor C) X₁.hom)
        (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.right) (X₂.hom ▷ X₃.right)).left ≫
      X₁.right ◁
          pushout.inr (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
            (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
        pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
          (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
    (map (obj (curriedTensor C) X₁.left)
        (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.right) (X₂.hom ▷ X₃.right)).hom ≫
      pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
        (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))

Tactic:
simp [Limits.pushout.associator_naturality_left_condition]

Premises used: CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ ((X₁ □ X₂) □ X₃).left ⟶ (X₁ □ X₂ □ X₃).left

Tactic:
exact pushout.desc ((α_ _ _ _).hom ≫ _ ◁ pushout.inl _ _ ≫ pushout.inl _ _)
        ((whiskerRightIso _ _).hom.left ≫
          pushout.desc (_ ◁ pushout.inr _ _ ≫ pushout.inl _ _) (pushout.inr _ _)
          (by simp [Limits.pushout.associator_naturality_left_condition]))
        (((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc])
          (by simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition]))

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso, CategoryTheory.Limits.pushout.desc, CategoryTheory.MonoidalCategory.tensorRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.Hom.left, CategoryTheory.Limits.pushout.inl, CategoryTheory.IsPushout.hom_ext, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom, CategoryTheory.Functor.map_isPushout, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ Eq (α :=
    obj.{v, v, u, u}
        (obj (curriedTensor C) (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₁.right X₂.left) (X₁.right ◁ X₂.hom)).left)
        X₃.left ⟶
      ((X₁ □ X₂) □ X₃).left)
    (NatTrans.app
        (map (curriedTensor C) (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₁.right X₂.left) (X₁.right ◁ X₂.hom)).hom)
        X₃.left ≫
      pushout.inl (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
    (map
        (obj (curriedTensor C) (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₁.right X₂.left) (X₁.right ◁ X₂.hom)).left)
        X₃.hom ≫
      pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
          X₃.right ≫
        pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
          (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))

Tactic:
simp [Limits.pushout.associator_inv_naturality_right_condition]

Premises used: CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorLeft X₁.left) (obj.{v, v, u, u} (obj (curriedTensor C) X₂.right) X₃.left) ⟶
      ((X₁ □ X₂) □ X₃).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorLeft X₁.left)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₂.left) X₃.left)
          (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left) (map (obj (curriedTensor C) X₂.left) X₃.hom)))
      (map (tensorLeft X₁.left)
        (pushout.inl (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
          (map (obj (curriedTensor C) X₂.left) X₃.hom)))
      (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left ≫
        Arrow.Hom.left (Iso.hom (whiskerLeftIso X₂ X₃)) ≫
          pushout.desc
            (pushout.inl (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                  (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
                X₃.right ≫
              pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
                (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            ⋯))
    (map (tensorLeft X₁.left)
        (pushout.inl (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
          (map (obj (curriedTensor C) X₂.left) X₃.hom)) ≫
      map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom ≫
        Iso.inv (α_ X₁.left X₂.right X₃.right) ≫
          pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
              X₃.right ≫
            pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))

Tactic:
simp [whisker_exchange_assoc,
            Limits.pushout.associator_inv_naturality_right_condition]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorLeft X₁.left) (obj.{v, v, u, u} (obj (curriedTensor C) X₂.left) X₃.right) ⟶
      ((X₁ □ X₂) □ X₃).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorLeft X₁.left)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₂.left) X₃.left)
          (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left) (map (obj (curriedTensor C) X₂.left) X₃.hom)))
      (map (tensorLeft X₁.left)
        (pushout.inr (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
          (map (obj (curriedTensor C) X₂.left) X₃.hom)))
      (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left ≫
        Arrow.Hom.left (Iso.hom (whiskerLeftIso X₂ X₃)) ≫
          pushout.desc
            (pushout.inl (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                  (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
                X₃.right ≫
              pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
                (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            ⋯))
    (map (tensorLeft X₁.left)
        (pushout.inr (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
          (map (obj (curriedTensor C) X₂.left) X₃.hom)) ≫
      map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom ≫
        Iso.inv (α_ X₁.left X₂.right X₃.right) ≫
          pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
              X₃.right ≫
            pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))

Tactic:
simp [whisker_exchange_assoc, Limits.pushout.condition_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ (X₁ □ X₂ □ X₃).left ⟶ ((X₁ □ X₂) □ X₃).left

Tactic:
exact pushout.desc ((whiskerLeftIso _ _).hom.left ≫
          pushout.desc (pushout.inl _ _) ((pushout.inl _ _ ▷ _) ≫ pushout.inr _ _)
          (by simp [Limits.pushout.associator_inv_naturality_right_condition]))
        ((α_ _ _ _).inv ≫ (pushout.inr _ _) ▷ _ ≫ pushout.inr _ _)
        (((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [whisker_exchange_assoc,
            Limits.pushout.associator_inv_naturality_right_condition])
          (by simp [whisker_exchange_assoc, Limits.pushout.condition_whiskerRight_assoc]))

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.Limits.pushout.desc, CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.Hom.left, CategoryTheory.Limits.pushout.inl, CategoryTheory.IsPushout.hom_ext, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom, CategoryTheory.Functor.map_isPushout, CategoryTheory.Iso.inv, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ pushout.desc
        (Iso.hom (α_ X₁.right X₂.right X₃.left) ≫
          X₁.right ◁
              pushout.inl (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
                (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
            pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
              (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
        (Arrow.Hom.left (Iso.hom (whiskerRightIso X₁ X₂)) ≫
          pushout.desc
            (X₁.right ◁
                pushout.inr (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
                  (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
              pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
                (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
            (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
              (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
            ⋯)
        ⋯ ≫
      pushout.desc
        (Arrow.Hom.left (Iso.hom (whiskerLeftIso X₂ X₃)) ≫
          pushout.desc
            (pushout.inl (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                  (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
                X₃.right ≫
              pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
                (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            ⋯)
        (Iso.inv (α_ X₁.left X₂.right X₃.right) ≫
          pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
              X₃.right ≫
            pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
        ⋯ =
    𝟙 ((X₁ □ X₂) □ X₃).left

Tactic:
apply pushout.hom_ext (by simp)

Premises used: CategoryTheory.Limits.pushout.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
refine_1₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MonoidalCategory.tensorRight, CategoryTheory.IsPushout.hom_ext, CategoryTheory.Functor.map_isPushout