awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
c j : C
rw :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c)))
    (Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j)
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)))
rw₁ rw₂ :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c)))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
          ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c)))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
          ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c)))
⊢ Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c)))
    (Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      ℌ.π c j)
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)))

Tactic:
rw [← Wedge.mk_ι
      (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
      (H.obj c) (ℌ.π c) (ℌ.hπ c),
    Wedge.IsLimit.lift_ι]

Premises used: CategoryTheory.Limits.Wedge.mk_ι, CategoryTheory.Limits.Wedge.IsLimit.lift_ι, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.π, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
w : ∀ (c : C), (η ≫ ℌ'.coev_app).app c = (ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c
⊢ η ≫ ℌ'.coev_app = ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 F) η) ℌ'

Tactic:
ext c
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
c : C
w : η.app c ≫ ℌ'.coev_app.app c = ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c
⊢ (η ≫ ℌ'.coev_app).app c = (ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
c : C
w :
  ∀ (j : (multicospanShapeEnd.{v₁, u₁} C).L),
    Eq (α :=
      G.obj c ⟶
        (multicospanIndexEnd
              (((dayConvolutionInternalHomDiagramFunctor F).obj
                    (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _)).obj
                c)).left
          j)
      ((η.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)
⊢ η.app c ≫ ℌ'.coev_app.app c = ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c

Tactic:
apply Wedge.IsLimit.hom_ext <| ℌ'.isLimitWedge c

Premises used: CategoryTheory.Limits.Wedge.IsLimit.hom_ext, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.isLimitWedge
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
c : C
j : (multicospanShapeEnd.{v₁, u₁} C).L
w :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (unop (F.op.obj (op j))) (G.obj c) ⟶
      (tensorRight c ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _).obj j)
    (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))
⊢ Eq (α :=
    G.obj c ⟶
      (multicospanIndexEnd
            (((dayConvolutionInternalHomDiagramFunctor F).obj
                  (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _)).obj
              c)).left
        j)
    ((η.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

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
c : C
j : (multicospanShapeEnd.{v₁, u₁} C).L
w :
  MonoidalClosed.uncurry ((η.app c ≫ ℌ'.coev_app.app c) ≫ ℌ'.π c j) =
    MonoidalClosed.uncurry ((ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫ ℌ'.π c j)
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (unop (F.op.obj (op j))) (G.obj c) ⟶
      (tensorRight c ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _).obj j)
    (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
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
c : C
j : (multicospanShapeEnd.{v₁, u₁} C).L
w :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c) ⟶
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
    (MonoidalClosed.uncurry (η.app c ≫ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G') (j, c))))
    (F.obj j ◁ η.app c ≫ NatTrans.app (DayConvolution.unit F G') (j, c))
⊢ MonoidalClosed.uncurry ((η.app c ≫ ℌ'.coev_app.app c) ≫ ℌ'.π c j) =
    MonoidalClosed.uncurry ((ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫ ℌ'.π c j)

Tactic:
simp only [Category.assoc, coev_app_π, Functor.comp_obj, tensor_obj,
    map_app_comp_π, coev_app_π_assoc, MonoidalClosed.uncurry_natural_right,
    MonoidalClosed.uncurry_curry, DayConvolution.unit_app_map_app,
    NatTrans.id_app, id_tensorHom]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.uncurry_natural_right, CategoryTheory.MonoidalCategory.tensor_obj, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π, CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.NatTrans.id_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π, CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _) H'
c : C
j : (multicospanShapeEnd.{v₁, u₁} C).L
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c) ⟶
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G' _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
    (MonoidalClosed.uncurry (η.app c ≫ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G') (j, c))))
    (F.obj j ◁ η.app c ≫ NatTrans.app (DayConvolution.unit F G') (j, c))

Tactic:
simp [MonoidalClosed.uncurry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.uncurry_natural_left
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_6 : DayConvolution F H
a :
  Eq (α :=
    (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (op (F ⊠ G))).obj
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _))
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
          (a : F ⊛ G ⟶ F ⊛ G) →
            ((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (op (F ⊠ G))).obj (F ⊛ G))
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
          (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app) :
      (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (op (F ⊠ G))).obj
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _))
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
          (a : F ⊛ G ⟶ F ⊛ G) →
            ((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (op (F ⊠ G))).obj (F ⊛ G))
        (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)) :
      (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (op (F ⊠ G))).obj
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _))
⊢ CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
      (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app =
    𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)

Tactic:
apply DayConvolution.corepresentableBy F G |>.homEquiv.injective

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy, Equiv.injective
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_6 : DayConvolution F H
a :
  ∀ (x y : C),
    Eq.{v₂ + 1} (α :=
      (F ⊠ G).obj (x, y) ⟶ (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (x, y))
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
            (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
          (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
            (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app))
        (x, y))
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
            (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
          (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)))
        (x, y))
⊢ Eq (α := F ⊠ G ⟶ tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
          (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
          (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app) :
      F ⊠ G ⟶ tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
          (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
        (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)) :
      F ⊠ G ⟶ tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_6 : DayConvolution F H
x y : C
a :
  Eq.{v₂ + 1} (α :=
    (F, G).2.obj (x, y).2 ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom ((F, G).1.obj (x, y).1))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (x, y)))
    (MonoidalClosed.curry
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
            (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
          (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
            (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app))
        (x, y)))
    (MonoidalClosed.curry
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
            (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
          (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)))
        (x, y)))
⊢ Eq.{v₂ + 1} (α :=
    (F ⊠ G).obj (x, y) ⟶ (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (x, y))
    (NatTrans.app
      ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
          (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
          (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app))
      (x, y))
    (NatTrans.app
      ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
          (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
        (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)))
      (x, y))

Tactic:
apply MonoidalClosed.curry_injective

Premises used: CategoryTheory.MonoidalClosed.curry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_6 : DayConvolution F H
x y : C
⊢ Eq.{v₂ + 1} (α :=
    (F, G).2.obj (x, y).2 ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom ((F, G).1.obj (x, y).1))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (x, y)))
    (MonoidalClosed.curry
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
            (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
          (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _)
            (DayConvolution.map (𝟙 F) ℌ.coev_app) ℌ.ev_app))
        (x, y)))
    (MonoidalClosed.curry
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F G) :
            (a : F ⊛ G ⟶ F ⊛ G) → F ⊠ G ⟶ tensor C ⋙ F ⊛ G)
          (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)))
        (x, y)))

Tactic:
simp [MonoidalClosed.curry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.curry_natural_left
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _) H'
w : ∀ (c : C), (ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c = NatTrans.app (𝟙 H) c
⊢ ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ = 𝟙 H

Tactic:
ext c
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _) H'
c : C
w :
  ∀ (j : (multicospanShapeEnd.{v₁, u₁} C).L),
    Eq (α := H.obj c ⟶ (multicospanIndexEnd (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c)).left j)
      ((ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j)
      (NatTrans.app (𝟙 H) c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j)
⊢ (ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c = NatTrans.app (𝟙 H) c

Tactic:
apply Wedge.IsLimit.hom_ext <| ℌ.isLimitWedge c

Premises used: CategoryTheory.Limits.Wedge.IsLimit.hom_ext, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.isLimitWedge
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _) H'
c : C
j : (multicospanShapeEnd.{v₁, u₁} C).L
w :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (unop (F.op.obj (op j))) (H.obj c) ⟶ (tensorRight c ⋙ G).obj j)
    (MonoidalClosed.uncurry ((ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j))
    (MonoidalClosed.uncurry (NatTrans.app (𝟙 H) c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j))
⊢ Eq (α := H.obj c ⟶ (multicospanIndexEnd (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c)).left j)
    ((ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j)
    (NatTrans.app (𝟙 H) c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j)

Tactic:
apply MonoidalClosed.uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _) H'
c : C
j : (multicospanShapeEnd.{v₁, u₁} C).L
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (unop (F.op.obj (op j))) (H.obj c) ⟶ (tensorRight c ⋙ G).obj j)
    (MonoidalClosed.uncurry ((ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j))
    (MonoidalClosed.uncurry (NatTrans.app (𝟙 H) c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j))

Tactic:
simp [MonoidalClosed.uncurry_natural_right]

Premises used: CategoryTheory.MonoidalClosed.uncurry_natural_right
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
F : Functor.{v₁, v₂, u₁, u₂} C V
⊢ functor { functor := F : DayFunctor.{v₁, v₂, u₁, u₂} C V } = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
F : DayFunctor.{v₁, v₂, u₁, u₂} C V
⊢ { functor := F.functor } = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
F G : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : F ⟶ G
h : α.natTrans = β.natTrans
mk :
  ∀ (natTrans : F.functor ⟶ G.functor) (h : { natTrans := natTrans : F.Hom G }.natTrans = β.natTrans),
    { natTrans := natTrans : F.Hom G } = β
⊢ α = β

Tactic:
cases α