mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ pushout.inl (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left) (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
      Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    pushout.inl (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
        (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
      Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.op).unop ≫
      (αᵣ (op x✝) (op x✝³) (op (x✝² ⊗ x✝¹))).symm.unop.hom ≫
        (αᵣ (op (unop (op x✝ ⊙ᵣ op x✝³))) (op x✝²) (op x✝¹)).symm.unop.hom =
    (αᵣ (op x✝) (op (x✝³ ⊗ x✝²)) (op x✝¹)).symm.unop.hom ≫
      ((αᵣ (op x✝) (op x✝³) (op x✝²)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Arrow.Hom.right (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) = Arrow.Hom.right ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (λ_ x✝¹).hom.op).unop =
    (αᵣ (op x✝) (op (𝟙_ C)) (op x✝¹)).symm.unop.hom ≫ ((ρᵣ (op x✝)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (ρ_ x✝¹).hom.op).unop =
    (αᵣ (op x✝) (op x✝¹) (op (𝟙_ C))).symm.unop.hom ≫ (ρᵣ (op (unop (op x✝ ⊙ᵣ op x✝¹)))).symm.unop.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
this : d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetractionAux adj c d = (ihom.ev d).app (R.obj c)
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ μ ≫ Δ = Δ ≫ (μ ⊗ₘ μ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ ε.hom ▷ M.X.X = (λ_ M.X.X).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
this :
  X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    X₁.right ◁ Arrow.Hom.left f₂ ▷ X₃.right ≫
      X₁.right ◁ Y₂.left ◁ Arrow.Hom.right f₃ ≫
        X₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) ≫
          Arrow.Hom.right f₁ ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)
⊢ (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ M.X.X ◁ ε.hom = (ρ_ M.X.X).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ M.X.X ◁ Δ.hom = Δ.hom ≫ Δ.hom ▷ M.X.X ≫ (α_ M.X.X M.X.X M.X.X).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : BimonObj M
⊢ η ≫ Δ = (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : BimonObj M
⊢ μ ≫ ε = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : BimonObj M
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ M M (M ⊗ M)).hom ≫
        M ◁ (α_ M M M).inv ≫ M ◁ (β_ M M).hom ▷ M ≫ M ◁ (α_ M M M).hom ≫ (α_ M M (M ⊗ M)).inv ≫ (μ ⊗ₘ μ) =
    μ ≫ Δ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
x✝¹ x✝ : Transported e
⊢ μ e.inverse x✝¹ x✝ ≫ e.inverse.map (e.functor.mapIso (β_ (e.inverse.obj x✝¹) (e.inverse.obj x✝))).hom =
    (β_ (e.inverse.obj x✝¹) (e.inverse.obj x✝)).hom ≫ μ e.inverse x✝ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Transported e
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
⊢ ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Mon C
X : Cᵒᵖ
⊢ Small.{w, v} ↑((yonedaMon.obj M).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
X : Cᵒᵖ
⊢ Small.{w, v} ↑((yonedaGrp.obj M).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Mon C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.obj M).map g)) (shrinkYonedaMonObjObjEquiv.symm f) =
    shrinkYonedaMonObjObjEquiv.symm (g.unop ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M M' : Mon C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.map g).app Y)) (shrinkYonedaMonObjObjEquiv.symm f) =
    shrinkYonedaMonObjObjEquiv.symm (f ≫ g.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.obj M).map g)) (shrinkYonedaGrpObjObjEquiv.symm f) =
    shrinkYonedaGrpObjObjEquiv.symm (g.unop ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M M' : Grp C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.map g).app Y)) (shrinkYonedaGrpObjObjEquiv.symm f) =
    shrinkYonedaGrpObjObjEquiv.symm (f ≫ g.hom.hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
⊢ adj.unit.app d ⊗ₘ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
⊢ ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝¹ : C
x✝ : D
⊢ IsIso (adj.unit.app ((ihom x✝).obj (R.obj x✝¹)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
⊢ ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
i j : J
f : i ⟶ j
⊢ ((Functor.const J).obj (c.1 ⊗ c.1)).map f ≫ (c.π.app j ⊗ₘ c.π.app j) ≫ μ =
    ((c.π.app i ⊗ₘ c.π.app i) ≫ μ) ≫ (F ⋙ forget C).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
this :
  (α_ X₁.left X₂.right X₃.right).hom ≫
      X₁.left ◁ X₂.right ◁ Arrow.Hom.right f₃ ≫
        (α_ X₁.left X₂.right Y₃.right).inv ≫
          Arrow.Hom.left f₁ ▷ X₂.right ▷ Y₃.right ≫
            (α_ Y₁.left X₂.right Y₃.right).hom ≫ Y₁.left ◁ Arrow.Hom.right f₂ ▷ Y₃.right =
    Arrow.Hom.left f₁ ▷ X₂.right ▷ X₃.right ≫
      (α_ Y₁.left X₂.right X₃.right).hom ≫
        Y₁.left ◁ Arrow.Hom.right f₂ ▷ X₃.right ≫ Y₁.left ◁ Y₂.right ◁ Arrow.Hom.right f₃
⊢ (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) =
    (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ ⊗ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ ⊗ X₂).left).map X₃.hom) ≫
        Arrow.Hom.left ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    (hc.lift { pt := 𝟙_ C, π := { app := fun X ↦ η, naturality := ⋯ } } ▷ c.pt ≫
          hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }) ≫
        c.π.app j =
      (λ_ c.pt).hom ≫ c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    (c.pt ◁ hc.lift { pt := 𝟙_ C, π := { app := fun X ↦ η, naturality := ⋯ } } ≫
          hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }) ≫
        c.π.app j =
      (ρ_ c.pt).hom ≫ c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ▷ c.pt ≫
      hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } =
    (α_ c.pt c.pt c.pt).hom ≫
      c.pt ◁ hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ≫
        hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    ((forget C).mapCone (limitCone F c hc)).π.app j =
      (Iso.refl ((forget C).mapCone (limitCone F c hc)).pt).hom ≫ c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
⊢ ∀ (j : J), (η ≫ hc.lift ((forget C).mapCone s)) ≫ c.π.app j = η ≫ c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
⊢ ∀ (j : J),
    (μ ≫ hc.lift ((forget C).mapCone s)) ≫ c.π.app j =
      ((hc.lift ((forget C).mapCone s) ⊗ₘ hc.lift ((forget C).mapCone s)) ≫ μ) ≫ c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
h : J
⊢ { hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h = s.π.app h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (limitCone F c hc).pt
w : ∀ (j : J), m ≫ (limitCone F c hc).π.app j = s.π.app j
j : J
⊢ m.hom ≫ c.π.app j = { hom := hc.lift ((forget C).mapCone s), isMonHom_hom := ⋯ }.hom ≫ c.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
this : IsIso ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c))
⊢ IsIso
    (((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ pushout.inl (((curriedTensor C).map (𝟙_ (Arrow C)).hom).app X.left)
        (((curriedTensor C).obj (𝟙_ (Arrow C)).left).map X.hom) ≫
      Arrow.Hom.left (𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom) =
    pushout.inl (((curriedTensor C).map (𝟙_ (Arrow C)).hom).app X.left)
        (((curriedTensor C).obj (𝟙_ (Arrow C)).left).map X.hom) ≫
      Arrow.Hom.left ((λ_ X).hom ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ Arrow.Hom.right (𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom) = Arrow.Hom.right ((λ_ X).hom ≫ f)

Tactic:
by

Goal state after: