awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine Arrow.isoMk ?_ (α_ _ _ _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
have refine_1 : ((X₁ □ X₂) □ X₃).left ⟶ (X₁ □ X₂ □ X₃).left
Tactic: refine Iso.mk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ ((X₁ □ X₂) □ X₃).left ≅ (X₁ □ X₂ □ X₃).left
have refine_1₁ : (X₁ □ X₂ □ X₃).left ⟶ ((X₁ □ X₂) □ X₃).left
Tactic: refine Iso.mk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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_1₁ : (X₁ □ X₂ □ X₃).left ⟶ ((X₁ □ X₂) □ X₃).left
⊢ ((X₁ □ X₂) □ X₃).left ≅ (X₁ □ X₂ □ X₃).left
have refine_1₂ : 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))
          sorry)
      sorry ≫
    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))
          sorry)
      (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))
      sorry =
  𝟙 ((X₁ □ X₂) □ X₃).left
Tactic: refine Iso.mk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
⊢ 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
have refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply pushout.hom_ext (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
have refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine_1₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
⊢ 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
have refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine pushout.hom_ext ?_ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
have refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine_1₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply pushout.hom_ext (by simp [← MonoidalCategory.whiskerLeft_comp])
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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)
have refine_2₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))) ≅ X
have refine_1 : (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ≅ X.left
Tactic: refine Arrow.isoMk ?_ (ρ_ X.right) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))) ≅ X
have refine_2 : Iso.hom
      {
        hom :=
          pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
            (Iso.hom (ρ_ X.left)) sorry,
        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 := sorry, inv_hom_id := sorry } ≫
    X.hom =
  (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).hom ≫ Iso.hom (ρ_ X.right)
Tactic: refine Arrow.isoMk ?_ (ρ_ X.right) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ≅ X.left
have refine_1 : (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶ X.left
Tactic: refine Iso.mk ?_ ((ρ_ X.left).inv ≫ pushout.inr _ _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ≅ X.left
have refine_1₁ : Eq (α :=
  (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶
    (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
  (pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
        (Iso.hom (ρ_ X.left)) sorry ≫
      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))))))) :
    (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
  (𝟙 (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left :
    (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
Tactic: refine Iso.mk ?_ ((ρ_ X.left).inv ≫ pushout.inr _ _) ?_ ?_