awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
F G : DayFunctor.{v₁, v₂, u₁, u₂} C V
β : F ⟶ G
natTrans : F.functor ⟶ G.functor
h : { natTrans := natTrans : F.Hom G }.natTrans = β.natTrans
mk :
  ∀ (natTrans_1 : F.functor ⟶ G.functor)
    (h : { natTrans := natTrans : F.Hom G }.natTrans = { natTrans := natTrans_1 }.natTrans),
    { natTrans := natTrans : F.Hom G } = { natTrans := natTrans_1 }
⊢ { natTrans := natTrans : F.Hom G } = β

Tactic:
cases β
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
F G : DayFunctor.{v₁, v₂, u₁, u₂} C V
natTrans natTrans_1 : F.functor ⟶ G.functor
h : { natTrans := natTrans : F.Hom G }.natTrans = { natTrans := natTrans_1 }.natTrans
⊢ { natTrans := natTrans : F.Hom G } = { natTrans := natTrans_1 }

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G : DayFunctor.{v₁, v₂, u₁, u₂} C V
⊢ (tensorObj (𝒞 := instCategory) F G).functor.IsLeftKanExtension (F.η G)

Tactic:
(isPointwiseLeftKanExtensionConvolutionExtensionUnit F G).isLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.MonoidalCategory.DayFunctor.η, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.isPointwiseLeftKanExtensionConvolutionExtensionUnit
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : tensorObj (𝒞 := instCategory) F G ⟶ H
h :
  ∀ (x y : C),
    Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ H.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ α.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ β.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
h₁ : α.natTrans = β.natTrans
⊢ α = β

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : tensorObj (𝒞 := instCategory) F G ⟶ H
h :
  ∀ (x y : C),
    Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ H.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ α.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ β.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
h₁ : F.η G ≫ Functor.whiskerLeft (tensor C) α.natTrans = F.η G ≫ Functor.whiskerLeft (tensor C) β.natTrans
⊢ α.natTrans = β.natTrans

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension
    (F ⊗ G).functor (η F G) _

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.MonoidalCategory.DayFunctor.η, CategoryTheory.MonoidalCategory.DayFunctor.functor
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : tensorObj (𝒞 := instCategory) F G ⟶ H
h :
  ∀ (x y : C),
    Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ H.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ α.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ β.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
h₁ :
  ∀ (x y : C),
    Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ (tensor C ⋙ H.functor).obj (x, y))
      ((F.η G ≫ Functor.whiskerLeft (tensor C) α.natTrans).app (x, y))
      ((F.η G ≫ Functor.whiskerLeft (tensor C) β.natTrans).app (x, y))
⊢ F.η G ≫ Functor.whiskerLeft (tensor C) α.natTrans = F.η G ≫ Functor.whiskerLeft (tensor C) β.natTrans

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : tensorObj (𝒞 := instCategory) F G ⟶ H
h :
  ∀ (x y : C),
    Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ H.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ α.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ β.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
x y : C
⊢ Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ (tensor C ⋙ H.functor).obj (x, y))
    ((F.η G ≫ Functor.whiskerLeft (tensor C) α.natTrans).app (x, y))
    ((F.η G ≫ Functor.whiskerLeft (tensor C) β.natTrans).app (x, y))

Tactic:
h x y
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : tensorObj (𝒞 := instCategory) F G ⟶ H
h :
  ∀ (x y : C),
    Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ H.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ α.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
      (NatTrans.app (F.η G) (x, y) ≫ β.natTrans.app (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
x y : C
⊢ Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ (tensor C ⋙ H.functor).obj (x, y))
    ((F.η G ≫ Functor.whiskerLeft (tensor C) α.natTrans).app (x, y))
    ((F.η G ≫ Functor.whiskerLeft (tensor C) β.natTrans).app (x, y))

Tactic:
exact h x y
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α : F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor
⊢ CategoryStruct.comp (Y := tensor C ⋙ (tensorObj (𝒞 := instCategory) F G).functor) (F.η G)
      (Functor.whiskerLeft (tensor C) (Hom.natTrans (tensorDesc α))) =
    α

Tactic:
Functor.descOfIsLeftKanExtension_fac _ _ _ _

Premises used: CategoryTheory.Functor.descOfIsLeftKanExtension, CategoryTheory.StructuredArrow.IsUniversal.desc, CategoryTheory.Functor.descOfIsLeftKanExtension_fac
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G H : DayFunctor.{v₁, v₂, u₁, u₂} C V
α : F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor
x y : C
⊢ Eq (α := (F.functor ⊠ G.functor).obj (x, y) ⟶ H.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
    (CategoryStruct.comp (Y := (tensor C ⋙ (tensorObj (𝒞 := instCategory) F G).functor).obj (x, y))
      (NatTrans.app (F.η G) (x, y)) (NatTrans.app (Hom.natTrans (tensorDesc α)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)))
    (α.app (x, y))

Tactic:
Functor.descOfIsLeftKanExtension_fac_app _ _ _ _ _

Premises used: CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G : DayFunctor.{v₁, v₂, u₁, u₂} C V
x y : C
⊢ Eq (α :=
    (F.functor ⊠ G.functor).obj (x, y) ⟶
      (Functor.pointwiseLeftKanExtension (tensor C) (F.functor ⊠ G.functor)).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
    (CategoryStruct.comp (Y := (tensor C ⋙ (tensorObj (𝒞 := instCategory) F G).functor).obj (x, y))
      (NatTrans.app (F.η G) (x, y))
      (NatTrans.app (Iso.hom (F.isoPointwiseLeftKanExtension G)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)))
    (Limits.colimit.ι (CostructuredArrow.proj (tensor C) (tensorObj.{v₁, u₁} (𝒞 := inst) x y) ⋙ F.functor ⊠ G.functor)
      (CostructuredArrow.mk (Y := (x, y)) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) x y))))

Tactic:
simpa [η, isoPointwiseLeftKanExtension] using
    Functor.descOfIsLeftKanExtension_fac_app
      (F ⊗ G).functor (η F G) _
      ((tensor C).pointwiseLeftKanExtensionUnit (F.functor ⊠ G.functor)) (x, y)

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtensionUnit, CategoryTheory.MonoidalCategory.tensor, Prod.mk, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.MonoidalCategory.externalProduct, CategoryTheory.MonoidalCategory.DayFunctor.isoPointwiseLeftKanExtension, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app, CategoryTheory.MonoidalCategory.DayFunctor.η, CategoryTheory.MonoidalCategory.DayFunctor.functor
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
hasDayConvolution : ∀ (F G : Functor.{v₁, v₂, u₁, u₂} C V), Functor.HasPointwiseLeftKanExtension (tensor C) (F ⊠ G)
hasDayConvolutionUnit :
  Functor.HasPointwiseLeftKanExtension.{0, 0, v₁, u₁, v₂, u₂} (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Functor.fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)))
inst_4 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_5 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_6 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape
      (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (𝟭 C) (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.prod (tensor C) (𝟭 C)) d)
      (tensorRight v)
F G : DayFunctor.{v₁, v₂, u₁, u₂} C V
x y : C
⊢ Eq (α :=
    Functor.obj (C := CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
        (CostructuredArrow.proj (tensor C) (tensorObj.{v₁, u₁} (𝒞 := inst) x y) ⋙ F.functor ⊠ G.functor)
        (CostructuredArrow.mk (Y := (x, y)) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) x y))) ⟶
      (tensorObj (𝒞 := instCategory) F G).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
    (Limits.colimit.ι (CostructuredArrow.proj (tensor C) (tensorObj.{v₁, u₁} (𝒞 := inst) x y) ⋙ F.functor ⊠ G.functor)
        (CostructuredArrow.mk (Y := (x, y)) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) x y))) ≫
      NatTrans.app (Iso.inv (F.isoPointwiseLeftKanExtension G)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
    (NatTrans.app (F.η G) (x, y))

Tactic:
simp [η, isoPointwiseLeftKanExtension]

Premises used: CategoryTheory.MonoidalCategory.DayFunctor.isoPointwiseLeftKanExtension, CategoryTheory.MonoidalCategory.DayFunctor.η