awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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 : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution G H
inst_6 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_3 G H _)
inst_7 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_8 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_9 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
⊢ (F ⊠ @convolution _ _ _ _ inst_2 inst_3 G H _).IsLeftKanExtension
    (extensionUnitRight (@convolution _ _ _ _ inst_2 inst_3 G H _) (unit G H) F)

Tactic:
(isPointwiseLeftKanExtensionExtensionUnitRight _ _ _ <|
    isPointwiseLeftKanExtensionUnit G H).isLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolution.isPointwiseLeftKanExtensionUnit, CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitRight
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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 : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution G H
inst_6 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_3 G H _)
inst_7 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_8 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_9 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
⊢ (@convolution _ _ _ _ inst_2 inst_3 F G _ ⊠ H).IsLeftKanExtension
    (extensionUnitLeft (@convolution _ _ _ _ inst_2 inst_3 F G _) (unit F G) H)

Tactic:
(isPointwiseLeftKanExtensionExtensionUnitLeft _ _ _ <|
    isPointwiseLeftKanExtensionUnit F G).isLeftKanExtension

Premises used: CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitLeft, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolution.isPointwiseLeftKanExtensionUnit
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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 : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_6 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_7 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
H K : Functor.{v₁, v₂, u₁, u₂} C V
inst_8 : DayConvolution G H
inst_9 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 F G _) H
inst_10 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_3 G H _)
inst_11 : DayConvolution H K
inst_12 : DayConvolution G (@convolution _ _ _ _ inst_2 inst_3 H K _)
inst_13 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 G H _) K
inst_14 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 (@convolution _ _ _ _ inst_2 inst_3 F G _) H _) K
inst_15 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 F G _) (@convolution _ _ _ _ inst_2 inst_3 H K _)
inst_16 : DayConvolution (@convolution _ _ _ _ inst_2 inst_3 F (@convolution _ _ _ _ inst_2 inst_3 G H _) _) K
inst_17 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_3 G (@convolution _ _ _ _ inst_2 inst_3 H K _) _)
inst_18 : DayConvolution F (@convolution _ _ _ _ inst_2 inst_3 (@convolution _ _ _ _ inst_2 inst_3 G H _) K _)
⊢ ((@convolution _ _ _ _ inst_2 inst_3 F G _ ⊠ H) ⊠ K).IsLeftKanExtension
    (extensionUnitLeft (@convolution _ _ _ _ inst_2 inst_3 F G _ ⊠ H)
      (extensionUnitLeft (@convolution _ _ _ _ inst_2 inst_3 F G _) (unit F G) H) K)

Tactic:
have : (((F ⊛ G) ⊠ H) ⊠ K).IsLeftKanExtension
    (α := extensionUnitLeft ((F ⊛ G) ⊠ H)
      (extensionUnitLeft _ (unit F G) H) K) :=
    isPointwiseLeftKanExtensionExtensionUnitLeft _ _ _
      (isPointwiseLeftKanExtensionExtensionUnitLeft _ _ _
        (isPointwiseLeftKanExtensionUnit F G)) |>.isLeftKanExtension
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e :
  ∀ (f : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ c),
    Eq (α := tensorUnit.{v₂, u₂} V (𝒞 := inst_1) ⟶ v) (can ≫ U.map f ≫ g) (can ≫ U.map f ≫ h)
apply :
  ∀ (j : CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) c),
    Eq (α :=
      obj.{0, v₂, v₁, u₂}
          (CostructuredArrow.proj (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) c ⋙
            fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
          j ⟶
        v)
      (NatTrans.app
          (Limits.Cocone.ι
            (LeftExtension.coconeAt (LeftExtension.mk U { app := fun (x : Discrete PUnit.{1}) ↦ can, naturality := ⋯ })
              c))
          j ≫
        g)
      (NatTrans.app
          (Limits.Cocone.ι
            (LeftExtension.coconeAt (LeftExtension.mk U { app := fun (x : Discrete PUnit.{1}) ↦ can, naturality := ⋯ })
              c))
          j ≫
        h)
⊢ g = h

Tactic:
apply (isPointwiseLeftKanExtensionCan c).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.MonoidalCategory.DayConvolutionUnit.isPointwiseLeftKanExtensionCan
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e :
  ∀ (f : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ c),
    Eq (α := tensorUnit.{v₂, u₂} V (𝒞 := inst_1) ⟶ v) (can ≫ U.map f ≫ g) (can ≫ U.map f ≫ h)
j : CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) c
⊢ Eq (α :=
    obj.{0, v₂, v₁, u₂}
        (CostructuredArrow.proj (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) c ⋙
          fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
        j ⟶
      v)
    (NatTrans.app
        (Limits.Cocone.ι
          (LeftExtension.coconeAt (LeftExtension.mk U { app := fun (x : Discrete PUnit.{1}) ↦ can, naturality := ⋯ })
            c))
        j ≫
      g)
    (NatTrans.app
        (Limits.Cocone.ι
          (LeftExtension.coconeAt (LeftExtension.mk U { app := fun (x : Discrete PUnit.{1}) ↦ can, naturality := ⋯ })
            c))
        j ≫
      h)

Tactic:
simpa using e j.hom

Premises used: CategoryTheory.CostructuredArrow.hom
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
⊢ (F ⊠ U).IsLeftKanExtension (L := Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (F :=
    F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1))) (extensionUnitRight U (φ U) F)

Tactic:
isPointwiseLeftKanExtensionExtensionUnitRight
    U (φ U) F isPointwiseLeftKanExtensionCan |>.isLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ, CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitRight, CategoryTheory.MonoidalCategory.DayConvolutionUnit.isPointwiseLeftKanExtensionCan
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
⊢ (U ⊠ F).IsLeftKanExtension (L := Functor.prod (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟭 C)) (F :=
    fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)) ⊠ F) (extensionUnitLeft U (φ U) F)

Tactic:
isPointwiseLeftKanExtensionExtensionUnitLeft
    U (φ U) F isPointwiseLeftKanExtensionCan |>.isLeftKanExtension

Premises used: CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitLeft, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ, CategoryTheory.MonoidalCategory.DayConvolutionUnit.isPointwiseLeftKanExtensionCan
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
⊢ obj (whiskeringLeft (C × C) C V) (tensor C) ⋙
      obj (whiskeringLeft (Discrete PUnit.{1} × C) (C × C) V)
          (Functor.prod (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟭 C)) ⋙
        obj coyoneda (Opposite.op (fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)) ⊠ F)) ≅
    obj coyoneda (Opposite.op F)

Tactic:
calc
    _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙
          (whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙
          (whiskeringLeft _ _ _).obj (prod.leftUnitorEquivalence C).inverse ⋙
          coyoneda.obj (.op <|
           (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) :=
      isoWhiskerLeft _ (isoWhiskerLeft _
        (NatIso.ofComponents fun _ ↦ Equiv.toIso <|
          (prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv))
    _ ≅ (whiskeringLeft _ _ _).obj
            ((prod.leftUnitorEquivalence C).inverse ⋙ (Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C) ⋙
              tensor C) ⋙
          coyoneda.obj (.op <|
            (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) :=
      .refl _
    _ ≅ (whiskeringLeft _ _ _).obj (𝟭 _) ⋙ coyoneda.obj (.op <|
          (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) :=
      isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents fun _ ↦ λ_ _) _
    _ ≅ _ := coyoneda.mapIso <| Iso.op <| NatIso.ofComponents fun _ ↦ (λ_ _).symm

Premises used: CategoryTheory.coyoneda, CategoryTheory.Iso.op, CategoryTheory.MonoidalCategory.tensor, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.prod, Equiv.toIso, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.prod.leftUnitorEquivalence, Opposite.op, CategoryTheory.Functor.whiskeringLeft, CategoryTheory.MonoidalCategory.externalProduct, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Functor.fromPUnit, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
⊢ obj (whiskeringLeft (C × C) C V) (tensor C) ⋙
      obj (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V)
          (Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ⋙
        obj coyoneda (Opposite.op (F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))) ≅
    obj coyoneda (Opposite.op F)

Tactic:
calc
    _ ≅ (whiskeringLeft _ _ _).obj (tensor C) ⋙
          (whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙
          (whiskeringLeft _ _ _).obj (prod.rightUnitorEquivalence C).inverse ⋙
          coyoneda.obj (.op <|
           (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) :=
      isoWhiskerLeft _ (isoWhiskerLeft _
        (NatIso.ofComponents fun _ ↦ Equiv.toIso <|
          (prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv))
    _ ≅ (whiskeringLeft _ _ _).obj
            ((prod.rightUnitorEquivalence C).inverse ⋙
              ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙ tensor C) ⋙
          coyoneda.obj (.op <|
            (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) :=
      .refl _
    _ ≅ (whiskeringLeft _ _ _).obj (𝟭 _) ⋙ coyoneda.obj (.op <|
          (prod.rightUnitorEquivalence C).inverse ⋙ F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) :=
      isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents fun _ ↦ ρ_ _) _
    _ ≅ _ := coyoneda.mapIso <| Iso.op <| NatIso.ofComponents fun _ ↦ (ρ_ _).symm

Premises used: CategoryTheory.coyoneda, CategoryTheory.Iso.op, CategoryTheory.MonoidalCategory.tensor, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.prod, Equiv.toIso, CategoryTheory.Functor.isoWhiskerLeft, Opposite.op, CategoryTheory.Functor.whiskeringLeft, CategoryTheory.MonoidalCategory.externalProduct, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.prod.rightUnitorEquivalence, CategoryTheory.Functor.fromPUnit, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_6 : DayConvolution U F
x : C
⊢ Eq.{v₂ + 1} (α := F.obj x ⟶ (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _).obj x)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)) (F.obj x))
      (Iso.inv (λ_ (F.obj x)))
      (CategoryStruct.comp (Y :=
        (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _).obj
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x))
        (NatTrans.app
          (Functor.whiskerLeft (prod.leftInverseUnitor C)
            (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F)
                  (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _) :
                (a : U ⊠ F ⟶ tensor C ⋙ U ⊛ F) →
                  fromPUnit (𝟙_ V) ⊠ F ⟶ (fromPUnit (𝟙_ C)).prod (𝟭 C) ⋙ tensor C ⋙ U ⊛ F)
              (((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _).homEquivOfIsLeftKanExtension
                    (DayConvolution.unit U F) (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _) :
                  (a : U ⊛ F ⟶ U ⊛ F) → U ⊠ F ⟶ tensor C ⋙ U ⊛ F)
                (𝟙 (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)))))
          x)
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _).map (Iso.hom (λ_ x)))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)) (F.obj x))
      (Iso.inv (λ_ (F.obj x)))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (U.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj x))
        (can ▷ F.obj x)
        (CategoryStruct.comp (Y :=
          (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _).obj
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x))
          (NatTrans.app (DayConvolution.unit U F) (tensorUnit.{v₁, u₁} C (𝒞 := inst), x))
          ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _).map (Iso.hom (λ_ x))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_6 : DayConvolution U F
G : Functor.{v₁, v₂, u₁, u₂} C V
inst_7 : DayConvolution U G
f : F ⟶ G
hγ :
  Eq (α := U ⊠ F ⟶ tensor C ⋙ G)
    (CategoryStruct.comp (Y := tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)
      (DayConvolution.unit U F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U G _) (DayConvolution.map (𝟙 U) f)
          (Iso.hom (leftUnitor U G)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)
      (DayConvolution.unit U F) (Functor.whiskerLeft (tensor C) (Iso.hom (leftUnitor U F) ≫ f)))
⊢ Eq (α := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _ ⟶ G)
    (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U G _) (DayConvolution.map (𝟙 U) f)
      (Iso.hom (leftUnitor U G)))
    (Iso.hom (leftUnitor U F) ≫ f)

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolution.unit
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_6 : DayConvolution U F
G : Functor.{v₁, v₂, u₁, u₂} C V
inst_7 : DayConvolution U G
f : F ⟶ G
hγ :
  Eq (α :=
    fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)) ⊠ F ⟶
      Functor.prod (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟭 C) ⋙ tensor C ⋙ G)
    (extensionUnitLeft U (φ U) F ≫
      Functor.whiskerLeft (Functor.prod (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟭 C))
        (CategoryStruct.comp (Y := tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)
          (DayConvolution.unit U F)
          (Functor.whiskerLeft (tensor C)
            (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U G _)
              (DayConvolution.map (𝟙 U) f) (Iso.hom (leftUnitor U G))))))
    (extensionUnitLeft U (φ U) F ≫
      Functor.whiskerLeft (Functor.prod (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟭 C))
        (CategoryStruct.comp (Y := tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)
          (DayConvolution.unit U F) (Functor.whiskerLeft (tensor C) (Iso.hom (leftUnitor U F) ≫ f))))
⊢ Eq (α := U ⊠ F ⟶ tensor C ⋙ G)
    (CategoryStruct.comp (Y := tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)
      (DayConvolution.unit U F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U G _) (DayConvolution.map (𝟙 U) f)
          (Iso.hom (leftUnitor U G)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 U F _)
      (DayConvolution.unit U F) (Functor.whiskerLeft (tensor C) (Iso.hom (leftUnitor U F) ≫ f)))

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitLeft U (φ U) F) _

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ, CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft