awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
fst snd : C
⊢ Eq (α := (F ⊠ H).obj (fst, snd) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _).obj (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))))
      (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))))
      (fst, snd))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_8 : DayConvolution F G
inst_9 : DayConvolution G H
inst_10 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_4 G H _)
inst_11 : DayConvolution (@convolution _ _ _ _ inst_2 inst_4 F G _) H
inst_12 : DayConvolution H F
inst_13 : DayConvolution G (@convolution _ _ _ _ inst_2 inst_4 H F _)
inst_14 : DayConvolution (@convolution _ _ _ _ inst_2 inst_4 G H _) F
inst_15 : DayConvolution G F
inst_16 : DayConvolution (@convolution _ _ _ _ inst_2 inst_4 G F _) H
inst_17 : DayConvolution F H
inst_18 : DayConvolution G (@convolution _ _ _ _ inst_2 inst_4 F H _)
z x y : C
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _).obj (x, z))
        (NatTrans.app (unit F H) (x, z)) (NatTrans.app (Iso.hom (braiding F H)) (tensorObj.{v₁, u₁} (𝒞 := inst) x z)) ≫
      (@convolution _ _ _ _ inst_2 inst_4 H F _).map (Iso.inv (β_ z x)) =
    (Iso.hom (β_ ((H, F).2.obj (z, x).2) ((H, F).1.obj (z, x).1)) ≫
        NatTrans.app (unit H F) (z, x) ≫
          (@convolution _ _ _ _ inst_2 inst_4 H F _).map (Iso.hom (β_ (z, x).1 (z, x).2))) ≫
      (@convolution _ _ _ _ inst_2 inst_4 H F _).map (Iso.inv (β_ z x))

Tactic:
haveI := unit_app_braiding_hom_app F H x z =≫ (H ⊛ F).map (β_ z x).inv
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
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 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_8 : DayConvolution F G
inst_9 : DayConvolution G H
inst_10 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_4 G H _)
inst_11 : DayConvolution (@convolution _ _ _ _ inst_2 inst_4 F G _) H
inst_12 : DayConvolution H (@convolution _ _ _ _ inst_2 inst_4 F G _)
inst_13 : DayConvolution H F
inst_14 : DayConvolution (@convolution _ _ _ _ inst_2 inst_4 H F _) G
inst_15 : DayConvolution H G
inst_16 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_4 H G _)
inst_17 : DayConvolution F H
inst_18 : DayConvolution (@convolution _ _ _ _ inst_2 inst_4 F H _) G
x y z : C
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _).obj (x, z))
        (NatTrans.app (unit F H) (x, z)) (NatTrans.app (Iso.hom (braiding F H)) (tensorObj.{v₁, u₁} (𝒞 := inst) x z)) ≫
      (@convolution _ _ _ _ inst_2 inst_4 H F _).map (Iso.inv (β_ z x)) =
    (Iso.hom (β_ ((H, F).2.obj (z, x).2) ((H, F).1.obj (z, x).1)) ≫
        NatTrans.app (unit H F) (z, x) ≫
          (@convolution _ _ _ _ inst_2 inst_4 H F _).map (Iso.hom (β_ (z, x).1 (z, x).2))) ≫
      (@convolution _ _ _ _ inst_2 inst_4 H F _).map (Iso.inv (β_ z x))

Tactic:
haveI := unit_app_braiding_hom_app F H x z =≫ (H ⊛ F).map (β_ z x).inv
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
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 : SymmetricCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : SymmetricCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
hγ :
  CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
          (Iso.hom (braiding G F)))) =
    unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))
⊢ CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
      (Iso.hom (braiding G F)) =
    𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _)

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.convolution, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolution.unit
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
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 : SymmetricCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : SymmetricCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
hγ :
  ∀ (x y : C),
    Eq (α := (F ⊠ G).obj (x, y) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
      (NatTrans.app
        (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
          (Functor.whiskerLeft (tensor C)
            (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
              (Iso.hom (braiding G F)))))
        (x, y))
      ((unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))).app (x, y))
⊢ CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
          (Iso.hom (braiding G F)))) =
    unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
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 : SymmetricCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : SymmetricCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
⊢ Eq (α := (F ⊠ G).obj (x, y) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _) (unit F G)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G F _) (Iso.hom (braiding F G))
            (Iso.hom (braiding G F)))))
      (x, y))
    ((unit F G ≫ Functor.whiskerLeft (tensor C) (𝟙 (@convolution _ _ _ _ inst_2 inst_4 F G _))).app (x, y))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 G' : Functor.{v₁, v₂, u₁, u₂} C V
η : G ⟶ G'
c c' : C
f : c ⟶ c'
j : Cᵒᵖ
k : C
⊢ Eq (α :=
    Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj (unop j))) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) k c)) ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj (unop j))) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) k c')))
    (Functor.map (ihom (F.obj (unop j))) (G.map (k ◁ f)) ≫
      Functor.map (ihom (F.obj (unop j))) (η.app (tensorObj.{v₁, u₁} (𝒞 := inst) k c')))
    (Functor.map (ihom (F.obj (unop j))) (η.app (tensorObj.{v₁, u₁} (𝒞 := inst) k c)) ≫
      Functor.map (ihom (F.obj (unop j))) (G'.map (k ◁ f)))

Tactic:
simpa [-NatTrans.naturality] using
          congr_arg (ihom <| F.obj <| unop j).map (η.naturality <| k ◁ f)

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.Functor.map, congr_arg, CategoryTheory.NatTrans.naturality, CategoryTheory.ihom, Opposite.unop, 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
⊢ Eq.{v₂ + 1} (α :=
    ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j')).obj j' ⟶
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
    ((fun
          (t :
            (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
              (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
        t.app j')
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map φ.op ≫
        (((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)))
    ((fun
          (t :
            (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
              (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
        t.app j')
      ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j') ≫
        (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op))

Tactic:
have := congrArg (fun t ↦ t.app j') <|
        dayConvolutionInternalHomDiagramFunctor
          F |>.map f |>.app c |>.naturality φ.op
-- 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  Eq.{v₂ + 1} (α :=
    ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j')).obj j' ⟶
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
    ((fun
          (t :
            (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
              (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
        t.app j')
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map φ.op ≫
        (((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)))
    ((fun
          (t :
            (((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj (op j') ⟶
              (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)) ↦
        t.app j')
      ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j') ≫
        (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op))
dsimp :
  (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
      Functor.map (ihom (F.obj j)) (G'.map (φ ▷ c)) =
    (ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))
⊢ Eq (α := H.obj c ⟶ ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).obj j')
    ((fun (j : C) ↦ ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)) j)
        j ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).map φ)
    ((fun (j : C) ↦ ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)) j)
        j' ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op).app j')

Tactic:
dsimp at 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  Eq (α :=
    Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j')) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (NatTrans.app (MonoidalClosed.pre (F.map φ)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
rw :
  Eq (α := H.obj c ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (ℌ.π c j' ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
        Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    ((ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
⊢ (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
      Functor.map (ihom (F.obj j)) (G'.map (φ ▷ c)) =
    (ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))

Tactic:
rw [Category.assoc, ← (ihom (F.obj j)).map_comp, ← f.naturality,
        Functor.map_comp, reassoc_of% ℌ.hπ]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, CategoryTheory.NatTrans.naturality, CategoryTheory.ihom, CategoryTheory.Functor.map_comp, 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  Eq (α :=
    Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j')) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (NatTrans.app (MonoidalClosed.pre (F.map φ)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
⊢ Eq (α := H.obj c ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj j)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    (ℌ.π c j' ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)) ≫
        Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))
    ((ℌ.π c j' ≫ Functor.map (ihom (F.obj j')) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j' c))) ≫
      NatTrans.app (MonoidalClosed.pre (F.map φ)) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) j' c)))

Tactic:
simp
-- 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
apply :
  ∀ (j : (multicospanShapeEnd.{v₁, u₁} C).L),
    (H.map f ≫
          Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
            (fun (j : C) ↦
              ℌ.π c' j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c').app (op j)) j)
            ⋯) ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
      (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
            (fun (j : C) ↦
              ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c).app (op j)) j)
            ⋯ ≫
          H'.map f) ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun (j : C) ↦
          ℌ.π c' j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c').app (op j)) j)
        ⋯ =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦
          ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c).app (op j)) j)
        ⋯ ≫
      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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
dsimp :
  (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) ⋯) ≫
      ℌ'.π c' j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
        H'.map f) ≫
      ℌ'.π c' j
⊢ (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦
            ℌ.π c' j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c').app (op j)) j)
          ⋯) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun (j : C) ↦
            ℌ.π c j ≫ NatTrans.app ((((dayConvolutionInternalHomDiagramFunctor F).map f_1).app c).app (op j)) j)
          ⋯ ≫
        H'.map f) ≫
      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 G H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
simp :
  H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) ⋯ ≫
        ℌ'.π c' j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j ≫ Functor.map (ihom (F.obj j)) (G'.map (j ◁ f))
⊢ (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) ⋯) ≫
      ℌ'.π c' j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
        H'.map f) ≫
      ℌ'.π c' j

Tactic:
simp only [Category.assoc, map_comp_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π
-- 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
rw :
  H.map f ≫ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c')) =
    (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
      Functor.map (ihom (F.obj j)) (G'.map (j ◁ f))
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun (j : C) ↦ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c'))) ⋯ ≫
        ℌ'.π c' j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j ≫ Functor.map (ihom (F.obj j)) (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_ι (ℌ'.isLimitWedge c'),
      Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)]

Premises used: CategoryTheory.Limits.Wedge.mk_ι, CategoryTheory.Limits.Wedge.IsLimit.lift_ι, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, CategoryTheory.Limits.Wedge.IsLimit.lift_ι_assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.isLimitWedge, 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 H : Functor.{v₁, v₂, u₁, u₂} C V
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
f_1 : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd.{v₁, u₁} C).L
⊢ H.map f ≫ ℌ.π c' j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c')) =
    (ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f_1.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ≫
      Functor.map (ihom (F.obj j)) (G'.map (j ◁ f))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp