mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C) ≫ 𝟙 (G.obj (F.obj (𝟙_ C)))

Tactic:
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
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 ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C)
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 ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ adj.unit.app (X ⊗ Y) = adj.unit.app (X ⊗ Y) ≫ 𝟙 (G.obj (F.obj (X ⊗ Y)))

Tactic:
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
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 ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ adj.unit.app (X ⊗ Y) = adj.unit.app (X ⊗ Y)
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
this : MonoidalCategory D := induced F fData
x✝ : D
⊢ (λ_ (F.obj x✝)).hom = fData.εIso.hom ▷ F.obj x✝ ≫ (fData.μIso (𝟙_ D) x✝).hom ≫ F.map (λ_ x✝).hom

Tactic:
by simp [fData.leftUnitor_eq]

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 ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ adj.counit.app X ⊗ₘ adj.counit.app Y = (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (X ⊗ Y)

Tactic:
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
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 ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ adj.counit.app X ⊗ₘ adj.counit.app Y = adj.counit.app X ⊗ₘ adj.counit.app Y
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, (X ◁ biproduct.π f x ⊗ₘ 𝟙 Y) ≫ (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝ ▷ Y =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ biproduct.π f x ▷ Y ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          X ◁ biproduct.π (fun j ↦ f j ⊗ Y) j✝ ≫ (α_ X (f j✝) Y).inv

Tactic:
simp_rw [← tensorHom_id, ← id_tensorHom]

Goal state after:
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,
      ((𝟙 X ⊗ₘ biproduct.π f x) ⊗ₘ 𝟙 Y) ≫
        (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ (biproduct.π (fun j ↦ X ⊗ f j) j✝ ⊗ₘ 𝟙 Y) =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          (𝟙 X ⊗ₘ biproduct.π (fun j ↦ f j ⊗ Y) j✝) ≫ (α_ X (f j✝) Y).inv
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.LaxMonoidal
X : C
⊢ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = ε F ▷ F.obj X ≫ μ F (𝟙_ C) X ≫ 𝟙 (F.obj (𝟙_ C ⊗ X))

Tactic:
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = ε F ▷ F.obj X ≫ μ F (𝟙_ C) 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
inst✝ : F.LaxMonoidal
X : C
⊢ F.obj X ◁ ε F ≫ μ F X (𝟙_ C) = F.obj X ◁ ε F ≫ μ F X (𝟙_ C) ≫ 𝟙 (F.obj (X ⊗ 𝟙_ C))

Tactic:
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ F.obj X ◁ ε F ≫ μ F X (𝟙_ C) = F.obj X ◁ ε F ≫ μ F X (𝟙_ C)
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.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) = μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z = μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z
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.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (F.obj x✝¹ ◁ F.map x✝ ≫ μ F x✝¹ Y✝) =
    μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝ ≫ F.map (x✝¹ ◁ x✝))

Tactic:
μ_natural_right

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
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ F.map x✝¹ ▷ F.obj x✝ = F.map x✝¹ ▷ F.obj x✝ ≫ 𝟙 (F.obj Y✝ ⊗ F.obj x✝)

Tactic:
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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ F.map x✝¹ ▷ F.obj x✝ = F.map x✝¹ ▷ F.obj 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ F.obj x✝¹ ◁ F.map x✝ = F.obj x✝¹ ◁ F.map x✝ ≫ 𝟙 (F.obj x✝¹ ⊗ F.obj Y✝)

Tactic:
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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ F.obj x✝¹ ◁ F.map x✝ = F.obj x✝¹ ◁ F.map 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ 𝟙 (F.obj X ⊗ F.obj Y ⊗ F.obj Z)

Tactic:
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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁
            (F.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
              F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
                adj.counit.app (F.obj (G.obj Y) ⊗ F.obj (G.obj Z)) ≫ (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          adj.counit.app X ▷ (Y ⊗ Z)

Tactic:
counit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁
            (F.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
              adj.counit.app (F.obj (G.obj Y ⊗ G.obj Z)) ≫
                δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          adj.counit.app X ▷ (Y ⊗ Z)
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      F.map (G.map (η F) ▷ G.obj X) ≫
        F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
          F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X))) ≫
            F.map (G.map (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)) ≫ adj.counit.app (𝟙_ D ⊗ X) ≫ (λ_ X).hom

Tactic:
counit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      F.map (G.map (η F) ▷ G.obj X) ≫
        F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
          F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X))) ≫
            adj.counit.app (F.obj (G.obj (𝟙_ D)) ⊗ F.obj (G.obj X)) ≫
              (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      F.map (G.map (η F) ▷ G.obj X) ≫
        F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
          F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X))) ≫
            adj.counit.app (F.obj (G.obj (𝟙_ D)) ⊗ F.obj (G.obj X)) ≫
              (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom

Tactic:
counit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      F.map (G.map (η F) ▷ G.obj X) ≫
        F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
          adj.counit.app (F.obj (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
            δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
x✝ : C
g : x✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (𝟙 x✝ ≫ g)

Tactic:
rwa [Category.id_comp]

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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫
      F.map (G.obj X ◁ G.map (η F)) ≫
        F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
          F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D)))) ≫
            F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫ adj.counit.app (X ⊗ 𝟙_ D) ≫ (ρ_ X).hom

Tactic:
counit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫
      F.map (G.obj X ◁ G.map (η F)) ≫
        F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
          F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D)))) ≫
            adj.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj (𝟙_ D))) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)) ≫ (ρ_ X).hom
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫
      F.map (G.obj X ◁ G.map (η F)) ≫
        F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
          F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D)))) ≫
            adj.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj (𝟙_ D))) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)) ≫ (ρ_ X).hom

Tactic:
counit_naturality_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫
      F.map (G.obj X ◁ G.map (η F)) ≫
        F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
          adj.counit.app (F.obj (G.obj X ⊗ G.obj (𝟙_ D))) ≫
            δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)) ≫ (ρ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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 C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Z✝ ◁ F.map f✝ ≫ μ F Z✝ Y✝ =
    (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝ ≫ F.map (Z✝ ◁ f✝)

Tactic:
μ_natural_right

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝ ≫ F.map (Z✝ ◁ f✝) =
    (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝ ≫ F.map (Z✝ ◁ 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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      (G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
          G.obj (F.obj X) ◁
            (μ G (F.obj Y) (F.obj Z) ≫
              adj.unit.app (G.obj (F.obj Y ⊗ F.obj Z)) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z)))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
right_triangle_components,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      (G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
          G.obj (F.obj X) ◁ (μ G (F.obj Y) (F.obj Z) ≫ 𝟙 (G.obj (F.obj Y ⊗ F.obj Z)))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

Tactic:
comp_id

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
⊢ adj.IsMonoidal

Tactic:
refine ⟨?_, fun X Y ↦ ?_⟩

Goal state after:
case refine_1
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
⊢ ε G = adj.unit.app (𝟙_ C) ≫ G.map (η F)

case refine_2
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
X Y : D
⊢ μ G X Y = adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

Tactic:
comp_id

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X