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 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 : C
dsimp :
  Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j =
    ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
⊢ (ℌ.map f ℌ').app c ≫ ℌ'.π c j = ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))

Tactic:
dsimp [map]

Premises used: CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map
-- 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 : C
rw :
  Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j =
    ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))
rw₁ rw₂ :
  ℌ.π c j ≫ 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))
⊢ Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun (j : C) ↦ ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))) ⋯ ≫
      ℌ'.π c j =
    ℌ.π c j ≫ Functor.map (ihom (F.obj j)) (f.app (tensorObj.{v₁, u₁} (𝒞 := inst) j c))

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

Premises used: CategoryTheory.Limits.Wedge.mk_ι, CategoryTheory.Limits.Wedge.IsLimit.lift_ι, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, 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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
⊢ Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    ((fun
          (t :
            H.obj x.2 ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
        (F.obj x.1 ◁ t :
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
            tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
              (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
      (ℌ.π x.2 x.1 ≫ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2))))
    ((fun
          (t :
            H.obj x.2 ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
        (F.obj x.1 ◁ t :
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
            tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
              (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
      (ℌ.π x.2 y.1 ≫ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))

Tactic:
have := congrArg (fun t ↦ F.obj x.1 ◁ t) <| ℌ.hπ x.2 f.1
-- 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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    ((fun
          (t :
            H.obj x.2 ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
        (F.obj x.1 ◁ t :
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
            tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
              (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
      (ℌ.π x.2 x.1 ≫ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2))))
    ((fun
          (t :
            H.obj x.2 ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))) ↦
        (F.obj x.1 ◁ t :
          tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
            tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
              (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))))
      (ℌ.π x.2 y.1 ≫ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
dsimp :
  (F.map f.1 ▷ H.obj x.2 ≫ F.obj y.1 ◁ H.map f.2) ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫ G.map (f.1 ⊗ₘ f.2)
⊢ (unop (op (F ⊠ H))).map f ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫
      (Functor.obj (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C)) G).map f

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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ (ℌ.π x.2 x.1 ≫ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2))))
    (F.obj x.1 ◁
      (ℌ.π x.2 y.1 ≫ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)))
    (F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))

Tactic:
simp only [whiskerLeft_comp] at this

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)))
    (F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
simp :
  F.map f.1 ▷ H.obj x.2 ≫
      F.obj y.1 ◁ (ℌ.π x.2 y.1 ≫ Functor.map (ihom (F.obj y.1)) (G.map (y.1 ◁ f.2))) ≫
        NatTrans.app (ihom.ev (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 y.2)) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫
      NatTrans.app (ihom.ev (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x.1 x.2)) ≫ G.map (f.1 ⊗ₘ f.2)
⊢ (F.map f.1 ▷ H.obj x.2 ≫ F.obj y.1 ◁ H.map f.2) ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫ G.map (f.1 ⊗ₘ f.2)

Tactic:
simp only [Category.assoc, MonoidalClosed.uncurry_eq, Functor.id_obj,
          ← whiskerLeft_comp_assoc, map_comp_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.uncurry_eq, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Functor.id_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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)))
    (F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
simp :
  F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫
        NatTrans.app (ihom.ev (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫
      F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)) ≫
        NatTrans.app (ihom.ev (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2)
⊢ F.map f.1 ▷ H.obj x.2 ≫
      F.obj y.1 ◁ (ℌ.π x.2 y.1 ≫ Functor.map (ihom (F.obj y.1)) (G.map (y.1 ◁ f.2))) ≫
        NatTrans.app (ihom.ev (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 y.2)) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫
      NatTrans.app (ihom.ev (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x.1 x.2)) ≫ G.map (f.1 ⊗ₘ f.2)

Tactic:
simp only [whiskerLeft_comp, Category.assoc, ihom.ev_naturality,
          Functor.comp_obj, curriedTensor_obj_obj, Functor.id_obj,
          ← whisker_exchange_assoc, tensorHom_def, Functor.map_comp,
          ← ihom.ev_naturality_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.Functor.id_obj, CategoryTheory.ihom.ev_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.ihom.ev_naturality_assoc
-- 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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)))
    (F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
rw :
  F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫
        NatTrans.app (ihom.ev (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
          (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
        (F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
        (NatTrans.app (ihom.ev (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2))
⊢ F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫
        NatTrans.app (ihom.ev (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫
      F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)) ≫
        NatTrans.app (ihom.ev (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2)

Tactic:
rw [reassoc_of% 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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1) (H.obj x.2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
        (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
    (F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ Functor.map (ihom (F.obj x.1)) (G.map (f.1 ▷ x.2)))
    (F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
⊢ F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫
        NatTrans.app (ihom.ev (F.obj y.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x.1)
          (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2))))
        (F.obj x.1 ◁ NatTrans.app (MonoidalClosed.pre (F.map f.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)))
        (NatTrans.app (ihom.ev (F.obj x.1)) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) y.1 x.2)) ≫ G.map (y.1 ◁ f.2))

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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
⊢ ∀ (β : F ⊠ H ⟶ tensor C ⋙ G) (X : C × C),
    NatTrans.app (DayConvolution.unit F H) X ≫
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _).descOfIsLeftKanExtension (DayConvolution.unit F H) G
              β).app
          (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) X) =
      β.app X

Tactic:
have := Functor.descOfIsLeftKanExtension_fac_app (F ⊛ H)
    (DayConvolution.unit F H) G
-- 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
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
this :
  ∀ (β : F ⊠ H ⟶ tensor C ⋙ G) (X : C × C),
    NatTrans.app (DayConvolution.unit F H) X ≫
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _).descOfIsLeftKanExtension (DayConvolution.unit F H) G
              β).app
          (tensorObj.{v₁, u₁} (𝒞 := inst) X.1 X.2) =
      β.app X
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _).obj (x, y))
      (NatTrans.app (DayConvolution.unit F H) (x, y)) (NatTrans.app ℌ.ev_app (tensorObj.{v₁, u₁} (𝒞 := inst) x y)) =
    MonoidalClosed.uncurry (ℌ.π y x)

Tactic:
simp [this, ev_app]

Premises used: CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_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 G H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F G' H'
inst_6 : DayConvolution F H'
η : G ⟶ G'
a :
  Eq (α := (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (op (F ⊠ H))).obj G')
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
          (a : F ⊛ H ⟶ G') → ((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (op (F ⊠ H))).obj G')
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H' _)
          (DayConvolution.map (𝟙 F) (ℌ.map η ℌ')) ℌ'.ev_app) :
      (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (op (F ⊠ H))).obj G')
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
          (a : F ⊛ H ⟶ G') → ((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (op (F ⊠ H))).obj G')
        (ℌ.ev_app ≫ η) :
      (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (op (F ⊠ H))).obj G')
⊢ Eq (α := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H _ ⟶ G')
    (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H' _)
      (DayConvolution.map (𝟙 F) (ℌ.map η ℌ')) ℌ'.ev_app)
    (ℌ.ev_app ≫ η)

Tactic:
apply DayConvolution.corepresentableBy F H |>.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 G H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F G' H'
inst_6 : DayConvolution F H'
η : G ⟶ G'
a :
  ∀ (x y : C),
    Eq.{v₂ + 1} (α := (F ⊠ H).obj (x, y) ⟶ (tensor C ⋙ G').obj (x, y))
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
            (a : F ⊛ H ⟶ G') → F ⊠ H ⟶ tensor C ⋙ G')
          (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H' _)
            (DayConvolution.map (𝟙 F) (ℌ.map η ℌ')) ℌ'.ev_app))
        (x, y))
      (NatTrans.app
        ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
            (a : F ⊛ H ⟶ G') → F ⊠ H ⟶ tensor C ⋙ G')
          (ℌ.ev_app ≫ η))
        (x, y))
⊢ Eq (α := F ⊠ H ⟶ tensor C ⋙ G')
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
          (a : F ⊛ H ⟶ G') → F ⊠ H ⟶ tensor C ⋙ G')
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H' _)
          (DayConvolution.map (𝟙 F) (ℌ.map η ℌ')) ℌ'.ev_app) :
      F ⊠ H ⟶ tensor C ⋙ G')
    ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
          (a : F ⊛ H ⟶ G') → F ⊠ H ⟶ tensor C ⋙ G')
        (ℌ.ev_app ≫ η) :
      F ⊠ H ⟶ tensor C ⋙ 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 G H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : Functor.{v₁, v₂, u₁, u₂} C V
ℌ' : DayConvolutionInternalHom F G' H'
inst_6 : DayConvolution F H'
η : G ⟶ G'
x y : C
⊢ Eq.{v₂ + 1} (α := (F ⊠ H).obj (x, y) ⟶ (tensor C ⋙ G').obj (x, y))
    (NatTrans.app
      ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
          (a : F ⊛ H ⟶ G') → F ⊠ H ⟶ tensor C ⋙ G')
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F H' _)
          (DayConvolution.map (𝟙 F) (ℌ.map η ℌ')) ℌ'.ev_app))
      (x, y))
    (NatTrans.app
      ((Functor.CorepresentableBy.homEquiv (DayConvolution.corepresentableBy F H) :
          (a : F ⊛ H ⟶ G') → F ⊠ H ⟶ tensor C ⋙ G')
        (ℌ.ev_app ≫ η))
      (x, y))

Tactic:
simp [MonoidalClosed.uncurry_eq, ← whiskerLeft_comp_assoc]

Premises used: CategoryTheory.MonoidalClosed.uncurry_eq, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc
-- 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''
⊢ 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.map (𝟙 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))

Tactic:
have := DayConvolution.unit_naturality F G f (𝟙 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 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.map (𝟙 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 (α :=
    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))

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

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.MonoidalCategory.tensorHom_id