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 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
        (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))
        ⋯ ≫
      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))
            ⋯)
        ⋯ =
    𝟙 (X₁ □ X₂ □ X₃).left

Tactic:
refine 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 ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.IsPushout.hom_ext, CategoryTheory.Functor.map_isPushout
-- 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 [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- 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_2 : 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 pushout.hom_ext (by simp [← MonoidalCategory.whiskerLeft_comp])

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_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
refine_2₁ : 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
-- 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 [← MonoidalCategory.whiskerLeft_comp, ← MonoidalCategory.comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [← MonoidalCategory.comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
X : Arrow.{v, u} C
I : C
i : IsInitial.{v, u} I
W : C
this_1 : IsIso (X := tensorObj.{v, u} (𝒞 := inst) X.left I) (X.hom ▷ I)
this :
  IsPushout (X.hom ▷ I) (X.left ◁ i.to W)
    (IsInitial.to (i.ofIso (Iso.symm (zeroMul i))) (tensorObj.{v, u} (𝒞 := inst) X.left W))
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X.left W))
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).right ⟶ tensorObj.{v, u} (𝒞 := inst) X.right W)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.mk (i.to W)).left)
        (map (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.mk (i.to W)).left)
        (map (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).hom))
      (Iso.hom (Iso.symm this.isoPushout) ≫ X.hom ▷ W))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.mk (i.to W)).left)
        (map (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.mk (i.to W)).left)
        (map (obj (curriedTensor C) X.left) (Arrow.mk (i.to W)).hom))
      (ι (ofHasPushout (curriedTensor C) X.hom (Arrow.mk (i.to W)).hom) ≫
        Iso.hom (Iso.refl (obj.{v, v, u, u} (obj (curriedTensor C) X.right) (Arrow.mk (i.to W)).right))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : BraidedCategory.{v, u} C
X : Arrow.{v, u} C
I : C
i : IsInitial.{v, u} I
W : C
this_1 : IsIso (X := tensorObj.{v, u} (𝒞 := inst) I X.left) (I ◁ X.hom)
this :
  IsPushout (i.to W ▷ X.left) (I ◁ X.hom) (𝟙 (tensorObj.{v, u} (𝒞 := inst) W X.left))
    (IsInitial.to (i.ofIso (Iso.symm (mulZero i))) (tensorObj.{v, u} (𝒞 := inst) W X.left))
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.mk (i.to W)).right) X.left ⟶ tensorObj.{v, u} (𝒞 := inst) W X.right)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.mk (i.to W)).left) X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.mk (i.to W)).hom) X.left)
        (map (obj (curriedTensor C) (Arrow.mk (i.to W)).left) X.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) (Arrow.mk (i.to W)).hom) X.left)
        (map (obj (curriedTensor C) (Arrow.mk (i.to W)).left) X.hom))
      (Iso.hom (Iso.symm this.isoPushout) ≫ W ◁ X.hom))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.mk (i.to W)).left) X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.mk (i.to W)).hom) X.left)
        (map (obj (curriedTensor C) (Arrow.mk (i.to W)).left) X.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) (Arrow.mk (i.to W)).hom) X.left)
        (map (obj (curriedTensor C) (Arrow.mk (i.to W)).left) X.hom))
      (ι (ofHasPushout (curriedTensor C) (Arrow.mk (i.to W)).hom X.hom) ≫
        Iso.hom (Iso.refl (obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.mk (i.to W)).right) X.right))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
X : Arrow.{v, u} C
I : C
i : IsInitial.{v, u} I
T : C
t : IsTerminal.{v, u} T
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X.left T ⟶ X.right)
    (Iso.hom (X.left ◁ᵢ t.uniqueUpToIso SemiCartesianMonoidalCategory.isTerminalTensorUnit ≪≫ ρ_ X.left) ≫ X.hom)
    (X.hom ▷ T ≫ Iso.hom (X.right ◁ᵢ t.uniqueUpToIso SemiCartesianMonoidalCategory.isTerminalTensorUnit ≪≫ ρ_ X.right))

Tactic:
simp [← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
refine_1 : (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ≅ X.left
refine_2 :
  Iso.hom
        {
          hom :=
            pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
              (Iso.hom (ρ_ X.left)) ⋯,
          inv :=
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X.left (tensorUnit.{v, u} C (𝒞 := inst)))
              (Iso.inv (ρ_ X.left))
              (pushout.inr
                (NatTrans.app (map (curriedTensor C) X.hom)
                  (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
                (map (obj (curriedTensor C) X.left)
                  (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))),
          hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      X.hom =
    (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).hom ≫ Iso.hom (ρ_ X.right)
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))) ≅ X

Tactic:
refine Arrow.isoMk ?_ (ρ_ X.right) ?_

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 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
refine_1 :
  obj.{v, v, u, u} (obj (curriedTensor C) X.right)
      (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ⟶
    X.left
refine_1₁ :
  Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.left)
        (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ⟶
      X.left)
    (NatTrans.app (map (curriedTensor C) X.hom)
        (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ≫
      IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
    (map (obj (curriedTensor C) X.left)
        (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ≫
      Iso.hom (ρ_ X.left))
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶ X.left

Tactic:
refine pushout.desc ?_ (ρ_ X.left).hom ?_

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.Arrow.left, CategoryTheory.Limits.pushout.desc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
⊢ obj.{v, v, u, u} (obj (curriedTensor C) X.right)
      (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ⟶
    X.left

Tactic:
exact (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to _

Premises used: CategoryTheory.zeroMul, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsInitial.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.left)
        (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ⟶
      X.left)
    (NatTrans.app (map (curriedTensor C) X.hom)
        (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ≫
      IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
    (map (obj (curriedTensor C) X.left)
        (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ≫
      Iso.hom (ρ_ X.left))

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.zeroMul, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsInitial.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
⊢ CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))
      (pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
          (Iso.hom (ρ_ X.left)) ⋯ ≫
        CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X.left (tensorUnit.{v, u} C (𝒞 := inst)))
          (Iso.inv (ρ_ X.left))
          (pushout.inr
            (NatTrans.app (map (curriedTensor C) X.hom)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (map (obj (curriedTensor C) X.left)
              (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))) =
    pushout.inr
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))) ≫
      𝟙 (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
⊢ CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))
      (pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
          (Iso.hom (ρ_ X.left)) ⋯ ≫
        CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X.left (tensorUnit.{v, u} C (𝒞 := inst)))
          (Iso.inv (ρ_ X.left))
          (pushout.inr
            (NatTrans.app (map (curriedTensor C) X.hom)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (map (obj (curriedTensor C) X.left)
              (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))) =
    pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))) ≫
      𝟙 (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.zeroMul, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsInitial.ofIso