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

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ (ExternalProduct.extensionUnitLeft (F ⊛ G) (unit F G) H ≫
          ((tensor C).prod (𝟭 C)).whiskerLeft
            (unit (F ⊛ G) H ≫
              (tensor C).whiskerLeft ((associator F G H).hom ≫ (braiding F (G ⊛ H)).hom ≫ (associator G H F).hom))).app
      ((x, y), z) =
    (ExternalProduct.extensionUnitLeft (F ⊛ G) (unit F G) H ≫
          ((tensor C).prod (𝟭 C)).whiskerLeft
            (unit (F ⊛ G) H ≫
              (tensor C).whiskerLeft
                (map (braiding F G).hom (𝟙 H) ≫ (associator G F H).hom ≫ map (𝟙 G) (braiding F H).hom))).app
      ((x, y), z)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
z x y : C
⊢ ((unit F G).app (x, y) ▷ H.obj z ≫ (F ⊛ G).obj (x ⊗ y) ◁ 𝟙 (H.obj z)) ≫
      (unit (F ⊛ G) H).app (x ⊗ y, z) ≫
        (associator F G H).hom.app ((x ⊗ y) ⊗ z) ≫
          (braiding F (G ⊛ H)).hom.app ((x ⊗ y) ⊗ z) ≫ (associator G H F).hom.app ((x ⊗ y) ⊗ z) =
    ((unit F G).app (x, y) ▷ H.obj z ≫ (F ⊛ G).obj (x ⊗ y) ◁ 𝟙 (H.obj z)) ≫
      (unit (F ⊛ G) H).app (x ⊗ y, z) ≫
        (map (braiding F G).hom (𝟙 H)).app ((x ⊗ y) ⊗ z) ≫
          (associator G F H).hom.app ((x ⊗ y) ⊗ z) ≫ (map (𝟙 G) (braiding F H).hom).app ((x ⊗ y) ⊗ z)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝ : MonoidalClosed V
F G G' : C ⥤ V
η : G ⟶ G'
c c' : C
f : c ⟶ c'
j : Cᵒᵖ
k : C
⊢ (({ obj := fun c ↦ (((Functor.whiskeringLeft₂ V).obj F.op).obj (tensorRight c ⋙ G)).obj MonoidalClosed.internalHom,
                    map := fun {c c'} f ↦
                      (((Functor.whiskeringLeft₂ V).obj F.op).map
                            (Functor.whiskerRight ((curriedTensor C).flip.map f) G)).app
                        MonoidalClosed.internalHom,
                    map_id := ⋯, map_comp := ⋯ }.map
                f ≫
              (((Functor.whiskeringLeft₂ V).obj F.op).map ((tensorRight c').whiskerLeft η)).app
                MonoidalClosed.internalHom).app
          j).app
      k =
    (((((Functor.whiskeringLeft₂ V).obj F.op).map ((tensorRight c).whiskerLeft η)).app MonoidalClosed.internalHom ≫
              {
                    obj := fun c ↦
                      (((Functor.whiskeringLeft₂ V).obj F.op).obj (tensorRight c ⋙ G')).obj MonoidalClosed.internalHom,
                    map := fun {c c'} f ↦
                      (((Functor.whiskeringLeft₂ V).obj F.op).map
                            (Functor.whiskerRight ((curriedTensor C).flip.map f) G')).app
                        MonoidalClosed.internalHom,
                    map_id := ⋯, map_comp := ⋯ }.map
                f).app
          j).app
      k

Tactic:
dsimp

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
inst✝ : MonoidalClosed V
F G G' : C ⥤ V
η : G ⟶ G'
c c' : C
f : c ⟶ c'
j : Cᵒᵖ
k : C
⊢ (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (G.map (k ◁ f)) ≫
      (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (η.app (k ⊗ c')) =
    (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (η.app (k ⊗ c)) ≫
      (MonoidalClosed.internalHom.obj (op (F.obj (unop j)))).map (G'.map (k ◁ f))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun j ↦ ℌ.π c' j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
        H'.map f) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j

Tactic:
dsimp

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ (H.map f ≫ Wedge.IsLimit.lift (ℌ'.isLimitWedge c') (fun j ↦ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c'))) ⋯) ≫
      ℌ'.π c' j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫ H'.map f) ≫
      ℌ'.π c' j
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ (ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F ≫
          ((𝟭 C).prod (tensor C)).whiskerLeft
            (unit F (G ⊛ H) ≫
              (tensor C).whiskerLeft ((associator F G H).inv ≫ (braiding (F ⊛ G) H).hom ≫ (associator H F G).inv))).app
      (x, y, z) =
    (ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F ≫
          ((𝟭 C).prod (tensor C)).whiskerLeft
            (unit F (G ⊛ H) ≫
              (tensor C).whiskerLeft
                (map (𝟙 F) (braiding G H).hom ≫ (associator F H G).inv ≫ map (braiding F H).hom (𝟙 G)))).app
      (x, y, z)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ (𝟙 (F.obj x) ▷ (G.obj y ⊗ H.obj z) ≫ F.obj x ◁ (unit G H).app (y, z)) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        (associator F G H).inv.app (x ⊗ y ⊗ z) ≫
          (braiding (F ⊛ G) H).hom.app (x ⊗ y ⊗ z) ≫ (associator H F G).inv.app (x ⊗ y ⊗ z) =
    (𝟙 (F.obj x) ▷ (G.obj y ⊗ H.obj z) ≫ F.obj x ◁ (unit G H).app (y, z)) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        (map (𝟙 F) (braiding G H).hom).app (x ⊗ y ⊗ z) ≫
          (associator F H G).inv.app (x ⊗ y ⊗ z) ≫ (map (braiding F H).hom (𝟙 G)).app (x ⊗ y ⊗ z)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝² : MonoidalClosed V
F G H : C ⥤ V
inst✝¹ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F G' H'
inst✝ : DayConvolution F H'
η : G ⟶ G'
⊢ (DayConvolution.corepresentableBy F H).homEquiv (DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app) =
    (DayConvolution.corepresentableBy F H).homEquiv (ℌ.ev_app ≫ η)

Tactic:
dsimp

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
inst✝² : MonoidalClosed V
F G H : C ⥤ V
inst✝¹ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F G' H'
inst✝ : DayConvolution F H'
η : G ⟶ G'
⊢ (DayConvolution.corepresentableBy F H).homEquiv (DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app) =
    (DayConvolution.corepresentableBy F H).homEquiv (ℌ.ev_app ≫ η)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''

Tactic:
dsimp

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
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      (MonoidalClosed.pre (F.map f)).app ((F ⊛ G).obj (c'' ⊗ c))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      H.map f

Tactic:
dsimp

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
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      H.map f
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
⊢ (η ≫ ℌ'.coev_app).app c = (ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c

Tactic:
dsimp

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
⊢ η.app c ≫ ℌ'.coev_app.app c = ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
j : (multicospanShapeEnd C).L
⊢ (η.app c ≫ ℌ'.coev_app.app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j =
    (ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j

Tactic:
apply MonoidalClosed.uncurry_injective

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
j : (multicospanShapeEnd C).L
⊢ MonoidalClosed.uncurry ((η.app c ≫ ℌ'.coev_app.app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j) =
    MonoidalClosed.uncurry
      ((ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫
        Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
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 S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ ((P.tensorBimod Q).tensorBimod L).actLeft ≫ hom P Q L = R.X ◁ hom P Q L ≫ (P.tensorBimod (Q.tensorBimod L)).actLeft

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
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 S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ TensorBimod.actLeft (P.tensorBimod Q) L ≫ hom P Q L = R.X ◁ hom P Q L ≫ TensorBimod.actLeft P (Q.tensorBimod L)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
j : (multicospanShapeEnd C).L
⊢ MonoidalClosed.uncurry ((η.app c ≫ ℌ'.coev_app.app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j) =
    MonoidalClosed.uncurry
      ((ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫
        Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j)

Tactic:
dsimp

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
j : (multicospanShapeEnd C).L
⊢ MonoidalClosed.uncurry ((η.app c ≫ ℌ'.coev_app.app c) ≫ ℌ'.π c j) =
    MonoidalClosed.uncurry ((ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫ ℌ'.π c j)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
inst✝ : DayConvolution F H
⊢ (DayConvolution.corepresentableBy F G).homEquiv (DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app) =
    (DayConvolution.corepresentableBy F G).homEquiv (𝟙 (F ⊛ G))

Tactic:
dsimp

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
inst✝² : MonoidalClosed V
F H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
inst✝ : DayConvolution F H
⊢ (DayConvolution.corepresentableBy F G).homEquiv (DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app) =
    (DayConvolution.corepresentableBy F G).homEquiv (𝟙 (F ⊛ G))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝¹ : MonoidalClosed V
F H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
c : C
j : (multicospanShapeEnd C).L
⊢ (ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j =
    (𝟙 H).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j

Tactic:
apply MonoidalClosed.uncurry_injective

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
inst✝¹ : MonoidalClosed V
F H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
c : C
j : (multicospanShapeEnd C).L
⊢ MonoidalClosed.uncurry ((ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j) =
    MonoidalClosed.uncurry ((𝟙 H).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((X.tensor Y).tensor Z).normalizeObj' ⟶ (X.tensor (Y.tensor Z)).normalizeObj'

Tactic:
dsimp

Goal state after:
C : Type u
X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((X ⊗ Y) ⊗ Z).normalizeObj' ⟶ (X ⊗ Y ⊗ Z).normalizeObj'
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (X✝.tensor (Y✝.tensor Z✝)).normalizeObj' ⟶ ((X✝.tensor Y✝).tensor Z✝).normalizeObj'

Tactic:
dsimp

Goal state after:
C : Type u
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (X✝ ⊗ Y✝ ⊗ Z✝).normalizeObj' ⟶ ((X✝ ⊗ Y✝) ⊗ Z✝).normalizeObj'
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (unit.tensor a✝).normalizeObj' ⟶ a✝.normalizeObj'

Tactic:
dsimp

Goal state after:
C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ a✝.normalizeObj' ⟶ (unit.tensor a✝).normalizeObj'

Tactic:
dsimp

Goal state after:
C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (a✝.tensor unit).normalizeObj' ⟶ a✝.normalizeObj'

Tactic:
dsimp

Goal state after:
C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ a✝.normalizeObj' ⟶ (a✝.tensor unit).normalizeObj'

Tactic:
dsimp

Goal state after:
C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X : NormalMonoidalObject C
⊢ ((tensorFunc C).obj X✝).map { down := { down := ⋯ } } ≫ (normalizeIsoApp C X✝ { as := X }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ ((normalize' C).obj X✝).map { down := { down := ⋯ } }

Tactic:
dsimp

Goal state after:
C : Type u
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X : NormalMonoidalObject C
⊢ (Discrete.functor fun n ↦ inclusionObj n ⊗ X✝).map (𝟙 { as := X }) ≫ (normalizeIsoApp C X✝ { as := X }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ 𝟙 (inclusionObj (X✝.normalizeObj X))