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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * LinearMap.id (x ⊗ₜ[R] y, z).2 =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * LinearMap.id (x ⊗ₜ[R] y, z).2 =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * z = ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 * ((x, y).2 * (x ⊗ₜ[R] y, z).2)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * z = ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 * ((x, y).2 * (x ⊗ₜ[R] y, z).2)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ▷ limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j

Tactic:
]

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ▷ limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j = (λ_ (limit F)).hom ≫ limit.π F j

Tactic:
]

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

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (lim.obj F)).hom ≫ limit.π F j =
    ((limit.lift ((Functor.const J).obj (𝟙_ C))
            { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (((Functor.const J).obj (𝟙_ C)).obj x), naturality := ⋯ } } ⊗ₘ
          𝟙 (lim.obj F)) ≫
        limit.lift (𝟙_ (J ⥤ C) ⊗ F)
            { pt := limit (𝟙_ (J ⥤ C)) ⊗ limit F,
              π := { app := fun j ↦ limit.π (𝟙_ (J ⥤ C)) j ⊗ₘ limit.π F j, naturality := ⋯ } } ≫
          lim.map (λ_ F).hom) ≫
      limit.π F j

Tactic:
dsimp
      simp only [tensorHom_id, limit.lift_map, Category.assoc, limit.lift_π]
      dsimp
      simp only [tensorHom_def, id_whiskerLeft, Category.assoc,
        Iso.inv_hom_id, Category.comp_id, ← comp_whiskerRight_assoc]
      erw [limit.lift_π]
      rw [id_whiskerRight, Category.id_comp]

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

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁ { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ≫
      (ρ_ (limit F)).hom ≫ limit.π F j

Tactic:
]

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁ { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ≫
      (ρ_ (limit F)).hom ≫ limit.π F j
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j = (ρ_ (limit F)).hom ≫ limit.π F j

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ 𝟙 P.X = 𝟙 P.X

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ R.X ◁ P.actLeft ≫ P.actLeft = R.X ◁ P.actLeft ≫ P.actLeft

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      ((map f g).app (x✝.1.1 ⊗ x✝.1.2) ⊗ₘ h.app x✝.2) ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        (unit F (G ⊛ H)).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
          (F ⊛ G ⊛ H).map (α_ x✝.1.1 x✝.1.2 x✝.2).inv ≫ (map f (map g h)).app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      ((map f g).app (x✝.1.1 ⊗ x✝.1.2) ⊗ₘ h.app x✝.2) ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        (unit F (G ⊛ H)).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
          (F ⊛ G ⊛ H).map (α_ x✝.1.1 x✝.1.2 x✝.2).inv ≫ (map f (map g h)).app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ ((f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ≫ (unit F' G').app (x✝.1.1, x✝.1.2)) ▷ H.obj x✝.2 ≫
      (F' ⊛ G').obj (x✝.1.1 ⊗ x✝.1.2) ◁ h.app x✝.2 ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        f.app x✝.1.1 ▷ (G ⊛ H).obj (x✝.1.2 ⊗ x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ ((f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ≫ (unit F' G').app (x✝.1.1, x✝.1.2)) ▷ H.obj x✝.2 ≫
      (F' ⊛ G').obj (x✝.1.1 ⊗ x✝.1.2) ◁ h.app x✝.2 ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        f.app x✝.1.1 ▷ (G ⊛ H).obj (x✝.1.2 ⊗ x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (ρ_ X).inv ≫ (X ◁ (η_ X Y ≫ (β_ Y X).inv) ≫ (α_ X Y X).inv ≫ ((β_ X Y).hom ≫ ε_ X Y) ▷ X) ≫ (λ_ X).hom = 𝟙 X

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (ρ_ X).inv ≫ (X ◁ (η_ X Y ≫ (β_ Y X).inv) ≫ (α_ X Y X).inv ≫ ((β_ X Y).hom ≫ ε_ X Y) ▷ X) ≫ (λ_ X).hom = 𝟙 X
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    inv (X ◁ (β_ Y X).inv) ≫
      (α_ X X Y).inv ≫
        (β_ X X).hom ▷ Y ≫
          (α_ X X Y).hom ≫
            X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    inv (X ◁ (β_ Y X).inv) ≫
      (α_ X X Y).inv ≫
        (β_ X X).hom ▷ Y ≫
          (α_ X X Y).hom ≫
            X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫
      (β_ X X).hom ▷ Y ≫
        (α_ X X Y).hom ≫
          X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫
      (β_ X X).hom ▷ Y ≫
        (α_ X X Y).hom ≫
          X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫
      (α_ X X Y).hom ≫
        X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫
      (α_ X X Y).hom ≫
        X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ S.X ≫ P.actRight = P.actRight ▷ S.X ≫ P.actRight

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ ((g.app x✝.1.2 ⊗ₘ h.app x✝.2) ≫ (unit G' H').app (x✝.1.2, x✝.2)) ≫
          (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹² : Category.{v₂, u₂} V
inst✝¹¹ : MonoidalCategory C
inst✝¹⁰ : MonoidalCategory V
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ ((g.app x✝.1.2 ⊗ₘ h.app x✝.2) ≫ (unit G' H').app (x✝.1.2, x✝.2)) ≫
          (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫
      X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫
      X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
      (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
      (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
        (α_ X Y X).inv) ≫
      (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
        (α_ X Y X).inv) ≫
      (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
          (α_ X Y X).inv) ≫
        (β_ Y X).inv ▷ X) ≫
      (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
          (α_ X Y X).inv) ≫
        (β_ Y X).inv ▷ X) ≫
      (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ ((α_ X Y X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv

Tactic:
]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ ((α_ X Y X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv