awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
erw :
  Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        NatTrans.app
          (Cone.π
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          j)
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
          (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          (limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j))
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))

Tactic:
erw [limit.lift_π]

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
rw :
  Iso.hom (ρ_ (limit F)) ≫ limit.π F j =
    𝟙 (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1))) ≫
      Iso.hom (ρ_ (limit F)) ≫ limit.π F j
rw₁ rw₂ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j) (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        NatTrans.app
          (Cone.π
            { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
              π :=
                { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                  NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                    (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } })
          j)
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))

Tactic:
rw [whiskerLeft_id, Category.id_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
j : J
⊢ CategoryStruct.comp (Y :=
      Functor.obj (C := Functor.{w, v, w, u} J C) lim ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (ε lim)
      (limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) =
    𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1))

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F G : Functor.{w, v, w, u} J C
j : J
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst_1) (Functor.obj lim F) (Functor.obj lim G) ⟶
      (tensorObj (𝒞 := Functor.category) F G).obj j)
    (μ lim F G ≫ limit.π (tensorObj (𝒞 := Functor.category) F G) j) (limit.π F j ⊗ₘ limit.π G j)

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
h₁ :
  Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl
      (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl 0)
h₂ :
  Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inr
      (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inr 0)
⊢ Eq (α :=
    coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl
      (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inl 0)

Tactic:
simp [tensorHom_def, ← comp_whiskerRight_assoc, coprod.inl_desc]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂ ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c₁.pt c₂.pt)
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inr
      (coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂)))
    (CategoryStruct.comp (Y :=
      coprod.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)) coprod.inr 0)

Tactic:
simp [tensorHom_def', ← whiskerLeft_comp_assoc, coprod.inr_desc]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Limits.coprod.inr_desc
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
inst_5 : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst_6 : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst_7 : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
⊢ HasBinaryCoproduct.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
    (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst_2 : Category.{v_2, u_2} J
inst_3 : Category.{v_3, u_3} J₁
inst_4 : Category.{v_4, u_4} J₂
F₁ F₂ : Functor.{v_2, v_1, u_2, u_1} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst_5 : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst_6 : IsSifted.{v_2, u_2} J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
refine_1 : Functor.diag J ⋙ externalProduct F₁ F₂ ≅ tensorObj (𝒞 := Functor.category) F₁ F₂
refine_2 :
  Iso (C := Cocone (tensorObj (𝒞 := Functor.category) F₁ F₂))
    (Functor.obj (C := Cocone (Functor.diag J ⋙ externalProduct F₁ F₂))
      (Cocone.precompose
        (Iso.inv (NatIso.ofComponents (fun (x : J) ↦ Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x)) ⋯)))
      (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)))
    (c₁.tensor c₂)
⊢ IsColimit (F := tensorObj (𝒞 := Functor.category) F₁ F₂) (c₁.tensor c₂)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    ((Functor.Final.isColimitWhiskerEquiv (Functor.diag J) _).2 (hc₁.tensor₂ hc₂))

Premises used: CategoryTheory.Functor.diag, CategoryTheory.Limits.IsColimit.tensor₂, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, Equiv.toFun, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst_2 : Category.{v_2, u_2} J
inst_3 : Category.{v_3, u_3} J₁
inst_4 : Category.{v_4, u_4} J₂
F₁ F₂ : Functor.{v_2, v_1, u_2, u_1} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst_5 : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst_6 : IsSifted.{v_2, u_2} J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
X Y : J
x : X ⟶ Y
⊢ (Functor.diag J ⋙ externalProduct F₁ F₂).map x ≫
      Iso.hom
        ((fun (x : J) ↦
            (Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x) :
              (Functor.diag J ⋙ externalProduct F₁ F₂).obj x ≅ (Functor.diag J ⋙ externalProduct F₁ F₂).obj x))
          Y) =
    Iso.hom
        ((fun (x : J) ↦
            (Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x) :
              (Functor.diag J ⋙ externalProduct F₁ F₂).obj x ≅ (Functor.diag J ⋙ externalProduct F₁ F₂).obj x))
          X) ≫
      (tensorObj (𝒞 := Functor.category) F₁ F₂).map x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst_2 : Category.{v_2, u_2} J
inst_3 : Category.{v_3, u_3} J₁
inst_4 : Category.{v_4, u_4} J₂
F₁ F₂ : Functor.{v_2, v_1, u_2, u_1} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst_5 : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst_6 : IsSifted.{v_2, u_2} J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Functor.diag J ⋙ externalProduct F₁ F₂ ≅ tensorObj (𝒞 := Functor.category) F₁ F₂

Tactic:
exact NatIso.ofComponents (fun _ ↦ Iso.refl _) (fun _ ↦ by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst_2 : Category.{v_2, u_2} J
inst_3 : Category.{v_3, u_3} J₁
inst_4 : Category.{v_4, u_4} J₂
F₁ F₂ : Functor.{v_2, v_1, u_2, u_1} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst_5 : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst_6 : IsSifted.{v_2, u_2} J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Iso (C := Cocone (tensorObj (𝒞 := Functor.category) F₁ F₂))
    (Functor.obj (C := Cocone (Functor.diag J ⋙ externalProduct F₁ F₂))
      (Cocone.precompose
        (Iso.inv (NatIso.ofComponents (fun (x : J) ↦ Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x)) ⋯)))
      (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)))
    (c₁.tensor c₂)

Tactic:
exact Cocone.ext (Iso.refl _)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
J : Type u₁
inst_2 : Category.{v₁, u₁} J
F G : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
inst_4 : HasColimit G
w : F ≅ G
j : J
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q (F.obj j) ⟶ tensorObj.{v, u} (𝒞 := inst) Q (colimit G))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Q (colimit F)) (Q ◁ colimit.ι F j)
      (Q ◁ Iso.hom (HasColimit.isoOfNatIso w)))
    (Q ◁ w.hom.app j ≫ Q ◁ colimit.ι G j)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
J : Type u₁
inst_2 : Category.{v₁, u₁} J
F G : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
inst_4 : HasColimit G
w : F ≅ G
j : J
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (F.obj j) Q ⟶ tensorObj.{v, u} (𝒞 := inst) (colimit G) Q)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (colimit F) Q) (colimit.ι F j ▷ Q)
      (Iso.hom (HasColimit.isoOfNatIso w) ▷ Q))
    (w.hom.app j ▷ Q ≫ colimit.ι G j ▷ Q)

Tactic:
simp [← MonoidalCategory.comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
J : Type u₁
inst_2 : Category.{v₁, u₁} J
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
c : Cocone F
j : J
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q (F.obj j) ⟶ tensorObj.{v, u} (𝒞 := inst) Q c.pt)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Q (colimit F)) (Q ◁ colimit.ι F j) (Q ◁ colimit.desc F c))
    (Q ◁ c.ι.app j)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
J : Type u₁
inst_2 : Category.{v₁, u₁} J
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
c : Cocone F
j : J
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (F.obj j) Q ⟶ tensorObj.{v, u} (𝒞 := inst) c.pt Q)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (colimit F) Q) (colimit.ι F j ▷ Q) (colimit.desc F c ▷ Q))
    (c.ι.app j ▷ Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
inst_2 : Category.{v_2, u_2} J
F : Functor.{v_2, v_1, u_2, u_1} J C
inst_3 : BraidedCategory.{v_1, u_1} C
c : C
inst_4 : PreservesColimit F (tensorLeft c)
⊢ PreservesColimit F (tensorRight c)

Tactic:
preservesColimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c)

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
inst_2 : Category.{v_2, u_2} J
F : Functor.{v_2, v_1, u_2, u_1} J C
inst_3 : BraidedCategory.{v_1, u_1} C
c : C
inst_4 : PreservesColimit F (tensorRight c)
⊢ PreservesColimit F (tensorLeft c)

Tactic:
preservesColimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c).symm

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
inst_2 : Category.{v_2, u_2} J
F : Functor.{v_2, v_1, u_2, u_1} J C
h : ∀ (c : C), PreservesColimit F (tensorRight c)
⊢ PreservesColimit F (curriedTensor C)

Tactic:
preservesColimit_of_evaluation _ _
    (fun c ↦ inferInstanceAs (PreservesColimit F (tensorRight c)))

Premises used: CategoryTheory.Limits.preservesColimit_of_evaluation, _private.0.CategoryTheory.MonoidalCategory.Limits.preservesCoLimit_curriedTensor._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
inst_2 : Category.{v_2, u_2} J
F : Functor.{v_2, v_1, u_2, u_1} J C
inst_3 : BraidedCategory.{v_1, u_1} C
c : C
inst_4 : PreservesLimit F (tensorLeft c)
⊢ PreservesLimit F (tensorRight c)

Tactic:
preservesLimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c)

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso, CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
inst_2 : Category.{v_2, u_2} J
F : Functor.{v_2, v_1, u_2, u_1} J C
inst_3 : BraidedCategory.{v_1, u_1} C
c : C
inst_4 : PreservesLimit F (tensorRight c)
⊢ PreservesLimit F (tensorLeft c)

Tactic:
preservesLimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c).symm

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso, CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
inst_2 : Category.{v_2, u_2} J
F : Functor.{v_2, v_1, u_2, u_1} J C
h : ∀ (c : C), PreservesLimit F (tensorRight c)
⊢ PreservesLimit F (curriedTensor C)

Tactic:
preservesLimit_of_evaluation _ _ <| fun c ↦ inferInstanceAs (PreservesLimit F (tensorRight c))

Premises used: _private.0.CategoryTheory.MonoidalCategory.Limits.preservesLimit_curriedTensor._proof_1, CategoryTheory.Limits.preservesLimit_of_evaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ (inl ≫ hP.desc h k w)) (Q ◁ h)
rw₁ rw₂ : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ h) (Q ◁ h)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ inl ≫ Q ◁ hP.desc h k w) (Q ◁ h)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inl_desc]

Premises used: CategoryTheory.IsPushout.inl_desc, CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ (inr ≫ hP.desc h k w)) (Q ◁ k)
rw₁ rw₂ : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ k) (Q ◁ k)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ inr ≫ Q ◁ hP.desc h k w) (Q ◁ k)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inr_desc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.IsPushout.inr_desc
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) ((inl ≫ hP.desc h k w) ▷ Q) (h ▷ Q)
rw₁ rw₂ : Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (h ▷ Q) (h ▷ Q)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (inl ▷ Q ≫ hP.desc h k w ▷ Q) (h ▷ Q)

Tactic:
rw [← comp_whiskerRight, IsPushout.inl_desc]

Premises used: CategoryTheory.IsPushout.inl_desc, CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) ((inr ≫ hP.desc h k w) ▷ Q) (k ▷ Q)
rw₁ rw₂ : Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (k ▷ Q) (k ▷ Q)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (inr ▷ Q ≫ hP.desc h k w ▷ Q) (k ▷ Q)

Tactic:
rw [← comp_whiskerRight, IsPushout.inr_desc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.IsPushout.inr_desc
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Z ⟶ tensorObj.{v, u} (𝒞 := inst) Q P) (Q ◁ f ≫ Q ◁ inl) (Q ◁ g ≫ Q ◁ inr)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp, hP.w]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Z Q ⟶ tensorObj.{v, u} (𝒞 := inst) P Q) (f ▷ Q ≫ inl ▷ Q) (g ▷ Q ≫ inr ▷ Q)

Tactic:
simp [← MonoidalCategory.comp_whiskerRight, hP.w]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w