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 G_1 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 c' c'' : C
f : c' ⟶ c''
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj c') (G.obj c) ⟶
      (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c))
    (F.map f ▷ G.obj c ≫ NatTrans.app (DayConvolution.unit F G) (c'', c))
    (NatTrans.app (DayConvolution.unit F G) (c', c) ≫
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c))
⊢ Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (MonoidalClosed.curry (F.map f ▷ G.obj c ≫ NatTrans.app (DayConvolution.unit F G) (c'', c)))
    (MonoidalClosed.curry
      (NatTrans.app (DayConvolution.unit F G) (c', c) ≫
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c)))

Tactic:
replace this := congrArg MonoidalClosed.curry this
-- 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 G_1 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 c' c'' : C
f : c' ⟶ c''
this :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (MonoidalClosed.curry (F.map f ▷ G.obj c ≫ NatTrans.app (DayConvolution.unit F G) (c'', c)))
    (MonoidalClosed.curry
      (NatTrans.app (DayConvolution.unit F G) (c', c) ≫
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c)))
⊢ Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c')) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj c'') (G.obj c)))
        (MonoidalClosed.curry (F.map f ▷ G.obj c))
        (Functor.map (ihom (F.obj c')) (NatTrans.app (DayConvolution.unit F G) (c'', c))) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c)) ≫
        Functor.map (ihom (F.obj c')) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c)) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))

Tactic:
simp only [MonoidalClosed.curry_natural_right] at this

Premises used: CategoryTheory.MonoidalClosed.curry_natural_right
-- 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 G_1 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 c' c'' : C
f : c' ⟶ c''
this :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c')) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj c'') (G.obj c)))
        (MonoidalClosed.curry (F.map f ▷ G.obj c))
        (Functor.map (ihom (F.obj c')) (NatTrans.app (DayConvolution.unit F G) (c'', c))) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c)) ≫
        Functor.map (ihom (F.obj c')) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c)) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
⊢ Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c')) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj c'') (G.obj c)))
        (MonoidalClosed.curry (F.map f ▷ G.obj c))
        (Functor.map (ihom (F.obj c')) (NatTrans.app (DayConvolution.unit F G) (c'', c))) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c''))
          ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))
        (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'', c)))
        (NatTrans.app (MonoidalClosed.pre (F.map f))
          ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c))) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))

Tactic:
simp [MonoidalClosed.curry_eq]

Premises used: CategoryTheory.MonoidalClosed.curry_eq
-- 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 G_1 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 c' : C
f : c ⟶ c'
dsimp :
  G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯ =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      H.map f
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯ =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      H.map f

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 G_1 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 c' : C
f : c ⟶ c'
apply :
  ∀ (j : (multicospanShapeEnd.{v₁, u₁} C).L),
    (G.map f ≫
          Wedge.IsLimit.lift (ℌ.isLimitWedge c')
            (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯) ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
      (Wedge.IsLimit.lift (ℌ.isLimitWedge c)
            (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
          H.map f) ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
        (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯ =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      H.map f

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 G_1 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 c' : C
f : c ⟶ c'
j : C
simp :
  G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯ ≫
        ℌ.π c' j =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      ℌ.π c j ≫ Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f))
⊢ (G.map f ≫
        Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯) ≫
      Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
    (Wedge.IsLimit.lift (ℌ.isLimitWedge c)
          (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
        H.map f) ≫
      Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j

Tactic:
simp only [multicospanIndexEnd_left,
      dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj, Multifork.ofι_pt,
      Wedge.mk_ι, Category.assoc, map_comp_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Wedge.mk_ι, CategoryTheory.Limits.Multifork.ofι_pt, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π, CategoryTheory.Limits.multicospanIndexEnd_left, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_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 G_1 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 c' : C
f : c ⟶ 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')))
    (G.map f ≫ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c')))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) ≫
      Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun (c'_1 : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'_1, c'))) ⋯ ≫
        ℌ.π c' j =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c)
        (fun (c' : C) ↦ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c))) ⋯ ≫
      ℌ.π c j ≫ Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f))

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

Premises used: CategoryTheory.Limits.Wedge.mk_ι, CategoryTheory.Limits.Wedge.IsLimit.lift_ι, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, CategoryTheory.Limits.Wedge.IsLimit.lift_ι_assoc, 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 G_1 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 c' : C
f : c ⟶ c'
j : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c) ⟶
      (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c'))
    ((F.map (𝟙 j) ⊗ₘ G.map f) ≫ NatTrans.app (DayConvolution.unit F G) (j, c'))
    (NatTrans.app (DayConvolution.unit F G) (j, c) ≫
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (𝟙 j ⊗ₘ f))

Tactic:
have := DayConvolution.unit_naturality F G (𝟙 j) f
-- 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 G_1 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 c' : C
f : c ⟶ c'
j : C
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c) ⟶
      (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c'))
    ((F.map (𝟙 j) ⊗ₘ G.map f) ≫ NatTrans.app (DayConvolution.unit F G) (j, c'))
    (NatTrans.app (DayConvolution.unit F G) (j, c) ≫
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (𝟙 j ⊗ₘ f))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c) ⟶
      (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c'))
    (F.obj j ◁ G.map f ≫ NatTrans.app (DayConvolution.unit F G) (j, c'))
    (NatTrans.app (DayConvolution.unit F G) (j, c) ≫
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f))

Tactic:
simp only [Functor.map_id, id_tensorHom] at this

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Functor.map_id
-- 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 G_1 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 c' : C
f : c ⟶ c'
j : C
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c) ⟶
      (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c'))
    (F.obj j ◁ G.map f ≫ NatTrans.app (DayConvolution.unit F G) (j, c'))
    (NatTrans.app (DayConvolution.unit F G) (j, c) ≫
      (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f))
⊢ Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c')))
    (MonoidalClosed.curry (F.obj j ◁ G.map f ≫ NatTrans.app (DayConvolution.unit F G) (j, c')))
    (MonoidalClosed.curry
      (NatTrans.app (DayConvolution.unit F G) (j, c) ≫
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))

Tactic:
replace this := congrArg MonoidalClosed.curry this
-- 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 G_1 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 c' : C
f : c ⟶ c'
j : C
this :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c')))
    (MonoidalClosed.curry (F.obj j ◁ G.map f ≫ NatTrans.app (DayConvolution.unit F G) (j, c')))
    (MonoidalClosed.curry
      (NatTrans.app (DayConvolution.unit F G) (j, c) ≫
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))
⊢ Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c')))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c')))
      (MonoidalClosed.curry (F.obj j ◁ G.map f))
      (Functor.map (ihom (F.obj j)) (NatTrans.app (DayConvolution.unit F G) (j, c'))))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) ≫
      Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))

Tactic:
simp only [MonoidalClosed.curry_natural_right] at this

Premises used: CategoryTheory.MonoidalClosed.curry_natural_right
-- 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 G_1 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 c' : C
f : c ⟶ c'
j : C
this :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c')))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c')))
      (MonoidalClosed.curry (F.obj j ◁ G.map f))
      (Functor.map (ihom (F.obj j)) (NatTrans.app (DayConvolution.unit F G) (j, c'))))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) ≫
      Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))
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')))
    (G.map f ≫ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c')))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c')))
      (MonoidalClosed.curry (F.obj j ◁ G.map f))
      (Functor.map (ihom (F.obj j)) (NatTrans.app (DayConvolution.unit F G) (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')))
    (G.map f ≫ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c')))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) ≫
      Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))

Tactic:
rw [← this]
-- 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 G_1 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 c' : C
f : c ⟶ c'
j : C
this :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (j, c')))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c')))
      (MonoidalClosed.curry (F.obj j ◁ G.map f))
      (Functor.map (ihom (F.obj j)) (NatTrans.app (DayConvolution.unit F G) (j, c'))))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c)) ≫
      Functor.map (ihom (F.obj j)) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (j ◁ f)))
⊢ 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')))
    (G.map f ≫ MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c')))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj j) (G.obj c')))
      (MonoidalClosed.curry (F.obj j ◁ G.map f))
      (Functor.map (ihom (F.obj j)) (NatTrans.app (DayConvolution.unit F G) (j, c'))))

Tactic:
simp [MonoidalClosed.curry_eq]

Premises used: CategoryTheory.MonoidalClosed.curry_eq
-- 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
dsimp :
  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)))
⊢ ℌ.coev_app.app c ≫ ℌ.π c j = MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (j, c))

Tactic:
dsimp [coev_app]

Premises used: CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app