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
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)
⊢ Functor.IsLeftKanExtension.{0, 0, v₂, u₂, v₁, u₁}
    (functor ((𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory))) (νNatTrans C V)

Tactic:
isPointwiseLeftKanExtensionUnitUnit C V (C ⊛⥤ V) |>.isLeftKanExtension

Premises used: CategoryTheory.MonoidalCategory.DayFunctor.ν, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans, CategoryTheory.MonoidalCategory.DayFunctor, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.isPointwiseLeftKanExtensionUnitUnit
-- 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 : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : (𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory) ⟶ F
h :
  ν C V ≫ α.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    ν C V ≫ β.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))
h₁ : α.natTrans = β.natTrans
⊢ α = β

Tactic:
ext1
-- 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 : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : (𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory) ⟶ F
h :
  ν C V ≫ α.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    ν C V ≫ β.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))
h₁ :
  νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) α.natTrans =
    νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) β.natTrans
⊢ α.natTrans = β.natTrans

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension
    (𝟙_ (C ⊛⥤ V)).functor (νNatTrans C V)

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans, CategoryTheory.MonoidalCategory.DayFunctor, CategoryTheory.MonoidalCategoryStruct.tensorUnit, 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 : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : (𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory) ⟶ F
h :
  ν C V ≫ α.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    ν C V ≫ β.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))
h₁ :
  ∀ (x : Discrete PUnit.{1}),
    (νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) α.natTrans).app x =
      (νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) β.natTrans).app x
⊢ νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) α.natTrans =
    νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) β.natTrans

Tactic:
ext
-- 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 : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : (𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory) ⟶ F
h :
  ν C V ≫ α.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    ν C V ≫ β.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))
x : Discrete PUnit.{1}
⊢ (νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) α.natTrans).app x =
    (νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) β.natTrans).app x

Tactic:
h

Premises used: CategoryTheory.MonoidalCategory.DayFunctor.ν
-- 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 : DayFunctor.{v₁, v₂, u₁, u₂} C V
α β : (𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory) ⟶ F
h :
  ν C V ≫ α.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    ν C V ≫ β.natTrans.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))
x : Discrete PUnit.{1}
⊢ (νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) α.natTrans).app x =
    (νNatTrans C V ≫ Functor.whiskerLeft (Functor.fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) β.natTrans).app x

Tactic:
exact h
-- 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 : DayFunctor.{v₁, v₂, u₁, u₂} C V
φ : tensorUnit.{v₂, u₂} V (𝒞 := inst_1) ⟶ F.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₂, u₁, u₂} (functor ((𝟙_ (DayFunctor.{v₁, v₂, u₁, u₂} C V)) (𝒞 := instCategory)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (ν C V) (NatTrans.app (Hom.natTrans (unitDesc φ)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    φ

Tactic:
Functor.descOfIsLeftKanExtension_fac_app (𝟙_ (C ⊛⥤ V)).functor (νNatTrans C V)
    F.functor { app _ := φ } default

Premises used: CategoryTheory.MonoidalCategory.DayFunctor.ν, Inhabited.default, CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans, CategoryTheory.MonoidalCategory.DayFunctor, CategoryTheory.NatTrans.mk, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app, CategoryTheory.MonoidalCategory.DayFunctor.functor
-- 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
⊢ (@convolution _ _ _ _ inst_2 inst_3 F G _).IsLeftKanExtension (unit F G)

Tactic:
isPointwiseLeftKanExtensionUnit F G |>.isLeftKanExtension

Premises used: 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
h h' : DayConvolution F G
⊢ unit F G ≫ Functor.whiskerLeft (tensor C) (h.uniqueUpToIso h').hom = unit F G

Tactic:
simp [uniqueUpToIso]

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.uniqueUpToIso
-- 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
h h' : DayConvolution F G
⊢ unit F G ≫ Functor.whiskerLeft (tensor C) (h.uniqueUpToIso h').inv = unit F G

Tactic:
simp [uniqueUpToIso]

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.uniqueUpToIso
-- 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
x x' y y' : C
f : x ⟶ x'
g : y ⟶ y'
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x) (G.obj y) ⟶
      (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_3 F G _).obj (x', y'))
    ((F.map f ⊗ₘ G.map g) ≫ NatTrans.app (unit F G) (x', y'))
    (NatTrans.app (unit F G) (x, y) ≫ (@convolution _ _ _ _ inst_2 inst_3 F G _).map (f ⊗ₘ g))

Tactic:
simpa [tensorHom_def] using (unit F G).naturality (f ×ₘ g)

Premises used: CategoryTheory.Prod.mkHom, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.NatTrans.naturality, 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
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
x x' y : C
f : x ⟶ x'
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x) (G.obj y) ⟶
      (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_3 F G _).obj (x', y))
    (F.map f ▷ G.obj y ≫ NatTrans.app (unit F G) (x', y))
    (NatTrans.app (unit F G) (x, y) ≫ (@convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ y))

Tactic:
simpa [tensorHom_def] using (unit F G).naturality (f ×ₘ 𝟙 _)

Premises used: CategoryTheory.Prod.mkHom, CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.NatTrans.naturality, 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
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
x y y' : C
g : y ⟶ y'
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x) (G.obj y) ⟶
      (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_3 F G _).obj (x, y'))
    (F.obj x ◁ G.map g ≫ NatTrans.app (unit F G) (x, y'))
    (NatTrans.app (unit F G) (x, y) ≫ (@convolution _ _ _ _ inst_2 inst_3 F G _).map (x ◁ g))

Tactic:
simpa [tensorHom_def] using (unit F G).naturality (𝟙 _ ×ₘ g)

Premises used: CategoryTheory.Prod.mkHom, CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.NatTrans.naturality, 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
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
F' G' : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F' G'
f : F ⟶ F'
g : G ⟶ G'
x y : C
⊢ Eq (α := (F ⊠ G).obj (x, y) ⟶ (@convolution _ _ _ _ inst_2 inst_3 F' G' _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x y))
    (CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_3 F G _).obj (x, y))
      (NatTrans.app (unit F G) (x, y)) (NatTrans.app (map f g) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)))
    ((f.app x ⊗ₘ g.app y) ≫ NatTrans.app (unit F' G') (x, y))

Tactic:
simpa [tensorHom_def] using
    (Functor.descOfIsLeftKanExtension_fac_app (F ⊛ G) (unit F G) (F' ⊛ G') <|
      (externalProductBifunctor C C V).map (f ×ₘ g) ≫ unit F' G') (x, y)

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.convolution, CategoryTheory.Prod.mkHom, CategoryTheory.MonoidalCategory.externalProductBifunctor, Prod.mk, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app, 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
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolution F G
⊢ ∀ {Y Y' : Functor.{v₁, v₂, u₁, u₂} C V} (g : Y ⟶ Y') (f : @convolution _ _ _ _ inst_2 inst_3 F G _ ⟶ Y),
    Eq (α :=
      (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (Opposite.op (F ⊠ G))).obj Y')
      (((@convolution _ _ _ _ inst_2 inst_3 F G _).homEquivOfIsLeftKanExtension (unit F G) Y' :
            (a : F ⊛ G ⟶ Y') →
              ((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).obj Y')
          (f ≫ g) :
        (Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙ Functor.obj coyoneda (Opposite.op (F ⊠ G))).obj
          Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙
                    Functor.obj coyoneda (Opposite.op (F ⊠ G))).map
                g) :
            (a :
                (fun (X : Type (max u₁ v₂)) ↦ X)
                  (((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).obj Y)) →
              (fun (X : Type (max u₁ v₂)) ↦ X)
                (((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).obj Y'))
          (((@convolution _ _ _ _ inst_2 inst_3 F G _).homEquivOfIsLeftKanExtension (unit F G) Y :
              (a : F ⊛ G ⟶ Y) →
                ((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).obj Y)
            f) :
        (fun (X : Type (max u₁ v₂)) ↦ X)
          ((Functor.obj (Functor.whiskeringLeft (C × C) C V) (tensor C) ⋙
                Functor.obj coyoneda (Opposite.op (F ⊠ G))).obj
            Y'))

Tactic:
aesop
-- 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
c : C
v : V
f g : (@convolution _ _ _ _ inst_2 inst_3 F G _).obj c ⟶ v
h :
  ∀ {x y : C} (u : tensorObj.{v₁, u₁} (𝒞 := inst) x y ⟶ c),
    NatTrans.app (unit F G) (x, y) ≫ (@convolution _ _ _ _ inst_2 inst_3 F G _).map u ≫ f =
      NatTrans.app (unit F G) (x, y) ≫ (@convolution _ _ _ _ inst_2 inst_3 F G _).map u ≫ g
j : CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) c
⊢ ((Functor.LeftExtension.mk (@convolution _ _ _ _ inst_2 inst_3 F G _) (unit F G)).coconeAt c).ι.app j ≫ f =
    ((Functor.LeftExtension.mk (@convolution _ _ _ _ inst_2 inst_3 F G _) (unit F G)).coconeAt c).ι.app j ≫ g

Tactic:
simpa using h j.hom

Premises used: CategoryTheory.CostructuredArrow.hom