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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv = (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv) =
    inv ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv = (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) =
    inv ((α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom = (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
inst✝¹¹ : MonoidalCategory D
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
E' : Type u₄
inst✝⁸ : Category.{v₄, u₄} E'
inst✝⁷ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁶ : F₁.LaxMonoidal
inst✝⁵ : F₂.LaxMonoidal
inst✝⁴ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝³ : G₁.LaxMonoidal
inst✝² : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝¹ : IsMonoidal τ
inst✝ : IsMonoidal τ'
⊢ ε (F₁ ⋙ G₁) ≫ (τ ◫ τ').app (𝟙_ C) = ε (F₂ ⋙ G₂)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) =
    inv (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ X (𝟙_ C) Y).inv ≫ (ρ_ X).hom ▷ Y = X ◁ (λ_ Y).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ X).inv ▷ Y ≫ (α_ X (𝟙_ C) Y).hom = X ◁ (λ_ Y).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (λ_ Y).inv ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ▷ Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
inst✝¹¹ : MonoidalCategory D
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
E' : Type u₄
inst✝⁸ : Category.{v₄, u₄} E'
inst✝⁷ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁶ : F₁.LaxMonoidal
inst✝⁵ : F₂.LaxMonoidal
inst✝⁴ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝³ : G₁.LaxMonoidal
inst✝² : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝¹ : IsMonoidal τ
inst✝ : IsMonoidal τ'
X Y : C
⊢ μ (F₁ ⋙ G₁) X Y ≫ (τ ◫ τ').app (X ⊗ Y) = ((τ ◫ τ').app X ⊗ₘ (τ ◫ τ').app Y) ≫ μ (F₂ ⋙ G₂) X Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).hom ▷ Y = (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ inv ((λ_ X).inv ▷ Y) = inv ((λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (α_ Y (𝟙_ C) (𝟙_ C)).inv ≫ (α_ X (Y ⊗ 𝟙_ C) (𝟙_ C)).inv ≫ (X ◁ (ρ_ Y).hom) ▷ 𝟙_ C =
    (α_ X Y (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (X ⊗ Y) ◁ (λ_ (𝟙_ C)).hom

Tactic:
←
      associator_inv_naturality_middle,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (α_ Y (𝟙_ C) (𝟙_ C)).inv ≫ X ◁ (ρ_ Y).hom ▷ 𝟙_ C ≫ (α_ X Y (𝟙_ C)).inv =
    (α_ X Y (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (X ⊗ Y) ◁ (λ_ (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
E' : Type u₄
inst✝⁶ : Category.{v₄, u₄} E'
inst✝⁵ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁴ : F₁.LaxMonoidal
inst✝³ : F₂.LaxMonoidal
inst✝² : F₃.LaxMonoidal
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (Functor.whiskerRight τ G₁)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ inv (X ◁ (ρ_ Y).inv) = inv ((ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ▷ Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = (λ_ X).inv ▷ Y ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' Y' Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ₘ g) ⊗ₘ h = (α_ X Y Z).hom ≫ (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X' Y' Z').inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ₘ g ⊗ₘ h = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X' Y' Z').hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝² : G₁.LaxMonoidal
inst✝¹ : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝ : IsMonoidal τ'
⊢ IsMonoidal (F₁.whiskerLeft τ')

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
h : Z ⟶ Z'
⊢ (𝟙 (X ⊗ Y) ⊗ₘ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ E
H : E ⥤ E'
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : H.LaxMonoidal
⊢ ε ((F ⋙ G) ⋙ H) ≫ (F.associator G H).hom.app (𝟙_ C) = ε (F ⋙ G ⋙ H)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' : C
f : X ⟶ X'
⊢ (f ⊗ₘ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f.hom ⊗ₘ g) ≫ (f.inv ⊗ₘ h) = (𝟙 V ⊗ₘ g) ≫ (𝟙 V ⊗ₘ h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f.inv ⊗ₘ g) ≫ (f.hom ⊗ₘ h) = (𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ E
H : E ⥤ E'
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : H.LaxMonoidal
X Y : C
⊢ μ ((F ⋙ G) ⋙ H) X Y ≫ (F.associator G H).hom.app (X ⊗ Y) =
    ((F.associator G H).hom.app X ⊗ₘ (F.associator G H).hom.app Y) ≫ μ (F ⋙ G ⋙ H) X Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ f.hom) ≫ (h ⊗ₘ f.inv) = (g ⊗ₘ 𝟙 V) ≫ (h ⊗ₘ 𝟙 V)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ f.inv) ≫ (h ⊗ₘ f.hom) = (g ⊗ₘ 𝟙 W) ≫ (h ⊗ₘ 𝟙 W)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ⊗ₘ g) ≫ (inv f ⊗ₘ h) = (𝟙 V ⊗ₘ g) ≫ (𝟙 V ⊗ₘ h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (inv f ⊗ₘ g) ≫ (f ⊗ₘ h) = (𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ f) ≫ (h ⊗ₘ inv f) = (g ⊗ₘ 𝟙 V) ≫ (h ⊗ₘ 𝟙 V)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ₘ inv f) ≫ (h ⊗ₘ f) = (g ⊗ₘ 𝟙 W) ≫ (h ⊗ₘ 𝟙 W)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ f ≫ g ⊗ₘ 𝟙 Z = (f ⊗ₘ 𝟙 Z) ≫ (g ⊗ₘ 𝟙 Z)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ₘ f ≫ g = (𝟙 Z ⊗ₘ f) ≫ (𝟙 Z ⊗ₘ g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (𝟙 Y ⊗ₘ f) ≫ (g ⊗ₘ 𝟙 X) = g ⊗ₘ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (g ⊗ₘ 𝟙 W) ≫ (𝟙 Z ⊗ₘ f) = g ⊗ₘ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 (𝟙_ C) ⊗ₘ f = 𝟙 (𝟙_ C) ⊗ₘ g ↔ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ f ⊗ₘ 𝟙 (𝟙_ C) = g ⊗ₘ 𝟙 (𝟙_ C) ↔ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z✝ X Y Z Z' : C
f : Z ⟶ Z'
⊢ (tensorLeft (X ⊗ Y)).map f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (tensorLeft Y ⋙ tensorLeft X).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorLeftTensor X Y).inv.app Z = (α_ X Y Z).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : (tensoringLeft C).map f = (tensoringLeft C).map g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : (tensoringRight C).map f = (tensoringRight C).map g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z✝ X Y Z Z' : C
f : Z ⟶ Z'
⊢ (tensorRight (X ⊗ Y)).map f ≫ (α_ Z' X Y).symm.hom = (α_ Z X Y).symm.hom ≫ (tensorRight X ⋙ tensorRight Y).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorRightTensor X Y).inv.app Z = (α_ Z X Y).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
W X Y Z : C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (f.1 ⊗ₘ g.1) ×ₘ f.2 ⊗ₘ g.2 = (f.1 ▷ X₂.1 ×ₘ f.2 ▷ X₂.2) ≫ (Y₁.1 ◁ g.1 ×ₘ Y₁.2 ◁ g.2)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C
inst✝¹⁵ : MonoidalCategory C
D : Type u₂
inst✝¹⁴ : Category.{v₂, u₂} D
inst✝¹³ : MonoidalCategory D
E : Type u₃
inst✝¹² : Category.{v₃, u₃} E
inst✝¹¹ : MonoidalCategory E
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ ε (F.prod' H) ≫ (prod' α β).app (𝟙_ C) = ε (G.prod' K)

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y X' Y' : J
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (F.map f ⊗ₘ G.map g) ≫ (α.app Y ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ (F'.map f ⊗ₘ G'.map g)

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ F.map f ▷ G.obj X' ≫ (α.app Y ⊗ₘ β.app X') = (α.app X ⊗ₘ β.app X') ≫ F'.map f ▷ G'.obj X'

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X' Y' : J
f : X' ⟶ Y'
X : J
⊢ F.obj X ◁ G.map f ≫ (α.app X ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ F'.obj X ◁ G'.map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ homMk (x✝¹.hom ⊗ₘ x✝.hom) = homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ F.map (f ⊗ₘ g) = F.map (f ▷ X₂ ≫ Y₁ ◁ g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁ X₂ : D
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C
inst✝¹⁵ : MonoidalCategory C
D : Type u₂
inst✝¹⁴ : Category.{v₂, u₂} D
inst✝¹³ : MonoidalCategory D
E : Type u₃
inst✝¹² : Category.{v₃, u₃} E
inst✝¹¹ : MonoidalCategory E
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y) = ((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
⊢ LaxMonoidal.ε F₂ ≫ e.inv.app (𝟙_ C) = LaxMonoidal.ε F₁

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map (X ◁ 𝟙 Y) = F.map (𝟙 (X ⊗ Y))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map (𝟙 X ▷ Y) = F.map (𝟙 (X ⊗ Y))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁ X₂ X₃ Y₁ Y₂ Y₃ : D
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ F.map (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) = F.map ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
f : X ⟶ Y
⊢ F.map (𝟙_ D ◁ f ≫ (λ_ Y).hom) = F.map ((λ_ X).hom ≫ f)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
f : X ⟶ Y
⊢ F.map (f ▷ 𝟙_ D ≫ (ρ_ Y).hom) = F.map ((ρ_ X).hom ≫ f)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
X Y : C
⊢ LaxMonoidal.μ F₂ X Y ≫ e.inv.app (X ⊗ Y) = (e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).map f ≫ ofHom (limitπRingHom F x✝) =
    ofHom (limitπRingHom F x✝¹) ≫ F.map f

Tactic:
by

Goal state after: