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

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ (∑ x, if h : x = j✝ then (𝟙 X ⊗ₘ biproduct.π f x) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (𝟙 X ⊗ₘ biproduct.π f x) ≫ 0 ⊗ₘ 𝟙 Y) =
    ∑ x,
      if h : x = j✝ then (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ eqToHom ⋯) ≫ (α_ X (f j✝) Y).inv
      else (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ 0) ≫ (α_ X (f j✝) Y).inv

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg pfgh : C
η_f : p ⊗ f ≅ pf
η_g : pf ⊗ g ≅ pfg
η_h : pfg ⊗ h ≅ pfgh
⊢ (p ◁ α_ f g h ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h)).hom =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ (p ◁ λ_ f ≪≫ η_f).hom = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ (p ◁ ρ_ f ≪≫ η_f).hom = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ p ◁ Iso.refl f ≪≫ η_f = η_f

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ F.map (f ⊗ₘ g) = δ F X X' ≫ (F.map f ⊗ₘ F.map g) ≫ μ F Y Y'

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
f : Y ⟶ Z
⊢ F.map (X ◁ f) = δ F X Y ≫ F.obj X ◁ F.map f ≫ μ F X Z

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
f : X ⟶ Y
Z : C
⊢ F.map (f ▷ Z) = δ F X Z ≫ F.map f ▷ F.obj Z ≫ μ F Y Z

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : Cᵒᵖ
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
⊢ ((x✝³.unop ⊗ₘ x✝².unop).op ≫ (x✝¹.unop ⊗ₘ x✝.unop).op).unop = ((x✝³ ≫ x✝¹).unop ⊗ₘ (x✝² ≫ x✝).unop).op.unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Cᵒᵖ
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
h : X₃✝ ⟶ Y₃✝
⊢ (((f.unop ⊗ₘ g.unop).op.unop ⊗ₘ h.unop).op ≫ (α_ (unop Y₁✝) (unop Y₂✝) (unop Y₃✝)).symm.op.hom).unop =
    ((α_ (unop X₁✝) (unop X₂✝) (unop X₃✝)).symm.op.hom ≫ (f.unop ⊗ₘ (g.unop ⊗ₘ h.unop).op.unop).op).unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((unop (op (𝟙_ C)) ◁ f.unop).op ≫ (λ_ (unop Y✝)).symm.op.hom).unop = ((λ_ (unop X✝)).symm.op.hom ≫ f).unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((f.unop ▷ unop (op (𝟙_ C))).op ≫ (ρ_ (unop Y✝)).symm.op.hom).unop = ((ρ_ (unop X✝)).symm.op.hom ≫ f).unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : Cᴹᵒᵖ
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
⊢ ((x✝².unmop ⊗ₘ x✝³.unmop).mop ≫ (x✝.unmop ⊗ₘ x✝¹.unmop).mop).unmop = ((x✝² ≫ x✝).unmop ⊗ₘ (x✝³ ≫ x✝¹).unmop).mop.unmop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Cᴹᵒᵖ
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
h : X₃✝ ⟶ Y₃✝
⊢ ((h.unmop ⊗ₘ (g.unmop ⊗ₘ f.unmop).mop.unmop).mop ≫ (α_ Y₃✝.unmop Y₂✝.unmop Y₁✝.unmop).symm.mop.hom).unmop =
    ((α_ X₃✝.unmop X₂✝.unmop X₁✝.unmop).symm.mop.hom ≫ ((h.unmop ⊗ₘ g.unmop).mop.unmop ⊗ₘ f.unmop).mop).unmop

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᴹᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((f.unmop ▷ { unmop := 𝟙_ C }.unmop).mop ≫ (ρ_ Y✝.unmop).mop.hom).unmop = ((ρ_ X✝.unmop).mop.hom ≫ f).unmop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᴹᵒᵖ
f : X✝ ⟶ Y✝
⊢ (({ unmop := 𝟙_ C }.unmop ◁ f.unmop).mop ≫ (λ_ Y✝.unmop).mop.hom).unmop = ((λ_ X✝.unmop).mop.hom ≫ f).unmop

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ (μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z) ≫
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    (μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z) ≫
      F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (λ_ X).hom = δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (λ_ X).inv = (λ_ (F.obj X)).inv ≫ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (ρ_ X).hom = δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom

Tactic:
simp

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

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
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (ρ_ X).inv = (ρ_ (F.obj X)).inv ≫ F.obj X ◁ ε F ≫ μ F X (𝟙_ C)

Tactic:
simp

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

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ ε (F ⋙ G) ≫ η (F ⋙ G) = 𝟙 (𝟙_ E)

Tactic:
simp

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

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ η (F ⋙ G) ≫ ε (F ⋙ G) = 𝟙 ((F ⋙ G).obj (𝟙_ C))

Tactic:
simp

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

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ μ (F ⋙ G) x✝¹ x✝ ≫ δ (F ⋙ G) x✝¹ x✝ = 𝟙 ((F ⋙ G).obj x✝¹ ⊗ (F ⋙ G).obj x✝)

Tactic:
simp

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

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ δ (F ⋙ G) x✝¹ x✝ ≫ μ (F ⋙ G) x✝¹ x✝ = 𝟙 ((F ⋙ G).obj (x✝¹ ⊗ x✝))

Tactic:
simp

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X Y Z : C
⊢ (μIso (X ⊗ Y) Z).inv ≫
      (μIso X Y).inv ▷ F.obj Z ≫ (μIso X Y).hom ▷ F.obj Z ≫ (μIso (X ⊗ Y) Z).hom ≫ F.map (α_ X Y Z).hom =
    F.map (α_ X Y Z).hom ≫
      (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv ≫ F.obj X ◁ (μIso Y Z).hom ≫ (μIso X (Y ⊗ Z)).hom

Tactic:
simp

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj X) =
    (εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom) ≫
      F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h : C
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h i j : C
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g : C
η : f ⟶ g
⊢ η = (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
α : g ≅ h
⊢ (f ◁ᵢ α).hom = (f ◁ᵢ α).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
α : f ≅ g
h : C
⊢ (α ▷ᵢ h).hom = (α ▷ᵢ h).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
h : C
⊢ η ▷ h = (Iso.refl (f ⊗ h)).hom ≫ η ▷ h ≫ (Iso.refl (g ⊗ h)).hom

Tactic:
simp

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

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (F.obj X ⊗ 𝟙_ D) =
    (F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom) ≫
      F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : f ⟶ g
θ : h ⟶ i
⊢ η ⊗ₘ θ = (Iso.refl (f ⊗ h)).hom ≫ (η ⊗ₘ θ) ≫ (Iso.refl (g ⊗ i)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
α : f ≅ g
β : h ≅ i
⊢ (α ⊗ᵢ β).hom = (α ⊗ᵢ β).hom

Tactic:
simp

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 ≫ F.map (𝟙 (𝟙_ (C × C)).1) = ε F

Tactic:
rw [Functor.map_id, Category.comp_id]

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 = ε F
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 ≫ G.map (𝟙 (𝟙_ (C × C)).2) = ε G

Tactic:
rw [Functor.map_id, Category.comp_id]

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 = ε G
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 ≫ F.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).1) = μ F X Y

Tactic:
rw [Functor.map_id, Category.comp_id]

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = μ F X Y
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
j : Jᵒᵖ
⊢ ((coconeLeftOpOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeLeftOp s)).unop).op = (s.ι.app j).op

Tactic:
simp only [coconeLeftOpOfCone_ι_app, op_comp, Quiver.Hom.op_unop, IsLimit.fac,
        coneOfCoconeLeftOp_π_app, op_unop]

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 ≫ G.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).2) = μ G X Y

Tactic:
rw [Functor.map_id, Category.comp_id]

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = μ G X Y
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
j : J
⊢ ((hc.desc (coconeOfConeRightOp s)).op ≫ (coneRightOpOfCocone c).π.app j).unop = (s.π.app j).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
j : J
⊢ ((coconeRightOpOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeRightOp s)).op).unop = (s.ι.app j).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
j : J
⊢ ((hc.desc (coconeOfConeUnop s)).unop ≫ (coneUnopOfCocone c).π.app j).op = (s.π.app j).op

Tactic:
simp

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).1 = η F

Tactic:
change F.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).1 = η F

Tactic:
by
  change F.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
j : J
⊢ ((coconeUnopOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeUnop s)).unop).op = (s.ι.app j).op

Tactic:
simp

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).1 = δ F X Y

Tactic:
change F.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

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

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).1 = δ F X Y

Tactic:
by
  change F.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
j : Jᵒᵖ
⊢ ((hc.desc (coconeRightOpOfCone s)).unop ≫ (coneOfCoconeRightOp c).π.app j).op = (s.π.app j).op

Tactic:
simp

Goal state after: