mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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.map (α_ X Y Z).hom =
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic

Goal state before:
pp: α : Type u_1
a b a' b' : α
ha : a = a'
hb : b = b'
h : a' = b'
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
f₁ f₂ f₃ f₄ : C
α α' : f₁ ⟶ f₂
η η' : f₂ ⟶ f₃
ηs ηs' : f₃ ⟶ f₄
e_α : α = α'
e_η : η = η'
e_ηs : ηs = ηs'
⊢ α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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

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

Tactic:
by

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ᵒᵖ
⊢ ((α_ (unop X) (unop (op (𝟙_ C))) (unop Y)).symm.op.hom ≫ (unop X ◁ (λ_ (unop Y)).symm.op.hom.unop).op).unop =
    ((ρ_ (unop X)).symm.op.hom.unop ▷ unop Y).op.unop

Tactic:
by

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.map (α_ X Y Z).inv =
    δ 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

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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:
by

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

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

Tactic:
by

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ᴹᵒᵖ
⊢ ((α_ Y.unmop { unmop := 𝟙_ C }.unmop X.unmop).symm.mop.hom ≫ ((ρ_ Y.unmop).mop.hom.unmop ▷ X.unmop).mop).unmop =
    (Y.unmop ◁ (λ_ X.unmop).mop.hom.unmop).mop.unmop

Tactic:
by

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)).inv =
    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:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ε (mopMopEquivalence C).inverse =
    (mopMopEquivalence C).toAdjunction.unit.app (𝟙_ Cᴹᵒᵖᴹᵒᵖ) ≫
      (mopMopEquivalence C).inverse.map (η (mopMopEquivalence C).functor)

Tactic:
by

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:
by

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:
by

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
⊢ μ (mopMopEquivalence C).inverse X Y =
    (mopMopEquivalence C).toAdjunction.unit.app
        ((mopMopEquivalence C).inverse.obj X ⊗ (mopMopEquivalence C).inverse.obj Y) ≫
      (mopMopEquivalence C).inverse.map
        (δ (mopMopEquivalence C).functor ((mopMopEquivalence C).inverse.obj X) ((mopMopEquivalence C).inverse.obj Y) ≫
          ((mopMopEquivalence C).toAdjunction.counit.app X ⊗ₘ (mopMopEquivalence C).toAdjunction.counit.app Y))

Tactic:
by

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:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ε (opOpEquivalence C).inverse =
    (opOpEquivalence C).toAdjunction.unit.app (𝟙_ Cᵒᵖᵒᵖ) ≫
      (opOpEquivalence C).inverse.map (η (opOpEquivalence C).functor)

Tactic:
by

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:
by

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),
    μ (opOpEquivalence C).inverse X Y =
      (opOpEquivalence C).toAdjunction.unit.app
          ((opOpEquivalence C).inverse.obj X ⊗ (opOpEquivalence C).inverse.obj Y) ≫
        (opOpEquivalence C).inverse.map
          (δ (opOpEquivalence C).functor ((opOpEquivalence C).inverse.obj X) ((opOpEquivalence C).inverse.obj Y) ≫
            ((opOpEquivalence C).toAdjunction.counit.app X ⊗ₘ (opOpEquivalence C).toAdjunction.counit.app Y))

Tactic:
by

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
⊢ CategoryTheory.inv (η F) = ε F

Tactic:
by

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
⊢ CategoryTheory.inv (ε F) = η F

Tactic:
by

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
⊢ CategoryTheory.inv (μ F X Y) = δ F X Y

Tactic:
by

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
⊢ CategoryTheory.inv (δ F X Y) = μ F X Y

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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

Goal state before:
pp: case δ
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝ = (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝

Tactic:
μIso_hom,

Goal state after:
case δ
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ δ F x✝¹ x✝ = μ F x✝¹ x✝ ≫ δ F x✝¹ x✝
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
⊢ Function.Injective (@toLaxMonoidal C inst✝³ inst✝² D inst✝¹ inst✝ F)

Tactic:
by

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
⊢ Function.Injective (@toOplaxMonoidal C inst✝³ inst✝² D inst✝¹ inst✝ F)

Tactic:
by

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 : C
f : X ⟶ Y
X' : C
⊢ F.map f ▷ F.obj X' ≫ (μIso Y X').hom = (μIso X X').hom ≫ F.map (f ▷ X')

Tactic:
by

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 X' : C
g : X ⟶ Y
⊢ F.obj X' ◁ F.map g ≫ (μIso X' Y).hom = (μIso X' X).hom ≫ F.map (X' ◁ g)

Tactic:
by

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).hom ▷ F.obj Z ≫ (μIso (X ⊗ Y) Z).hom ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ (μIso Y Z).hom ≫ (μIso X (Y ⊗ Z)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ (α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom

Tactic:
ext : 1
  apply TensorProduct.ext_threefold
  intro x y z
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ (α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ (x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
by

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)).hom = εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
⊢ { toFun := ⇑(ConcreteCategory.hom f), map_add' := ⋯ }.toFun (n • x) =
    (RingHom.id ℤ) n • { toFun := ⇑(ConcreteCategory.hom f), map_add' := ⋯ }.toFun x

Tactic:
by

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:
by

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:
by

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
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
by

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
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
by

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:
by

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 : C
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
by

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:
by

Goal state after: