awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.OplaxMonoidal
X Y Z : Comon.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α :=
    Comon.X.{v₂, u₂} { X := F.obj X.X, comon := obj.instComonObj X.X F : Comon.{v₂, u₂} D } ⟶
      Comon.X.{v₂, u₂} { X := F.obj Z.X, comon := obj.instComonObj Z.X F })
    (Comon.Hom.hom { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ })
    (Comon.Hom.hom
      (CategoryStruct.comp (Y := { X := F.obj Y.X, comon := obj.instComonObj Y.X F })
        { hom := F.map f.hom, isComonHom_hom := ⋯ } { hom := F.map g.hom, isComonHom_hom := ⋯ }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
⊢ Eq.{v₁ + 1} (α := Conv M N) 1 (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g : Conv M N
⊢ f * g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (f ▷ M ≫ N ◁ g ≫ μ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
simp :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (f ▷ M ≫ N ◁ g ≫ μ) ▷ M ≫ N ◁ h ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫ N ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (g ▷ M ≫ N ◁ h ≫ μ) ≫ μ)
⊢ f * g * h = f * (g * h)

Tactic:
simp only [mul_eq]

Premises used: CategoryTheory.Conv.mul_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
simp :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (Δ ▷ M ≫ f ▷ M ▷ M ≫ Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ μ ▷ M ≫ N ◁ h ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
          (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (f ▷ M ≫ N ◁ g ≫ μ) ▷ M ≫ N ◁ h ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫ N ◁ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ (g ▷ M ≫ N ◁ h ≫ μ) ≫ μ)

Tactic:
simp only [comp_whiskerRight, whisker_assoc, Category.assoc,
      MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.whisker_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
a : tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N
| μ ▷ M ≫ N ◁ h

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
slice_lhs :
  Δ ≫
      Δ ▷ M ≫
        f ▷ M ▷ M ≫
          Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
          (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (Δ ▷ M ≫ f ▷ M ▷ M ≫ Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ μ ▷ M ≫ N ◁ h ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
          (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))

Tactic:
slice_lhs 7 8 =>
      rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
a : M ◁ Δ ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M
| f ▷ M ≫ N ◁ Δ

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
slice_rhs :
  Δ ≫
      Δ ▷ M ≫
        f ▷ M ▷ M ≫
          Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) N N))
          (((M ◁ Δ ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ N ◁ g ▷ M) ≫ N ◁ N ◁ h) (N ◁ μ) ≫
        μ)
⊢ Δ ≫
      Δ ▷ M ≫
        f ▷ M ▷ M ≫
          Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (f ▷ M ≫
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (N ◁ Δ)
          (N ◁ g ▷ M ≫ N ◁ N ◁ h ≫ N ◁ μ ≫ μ))

Tactic:
slice_rhs 2 3 =>
      rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f g h : Conv M N
⊢ Δ ≫
      Δ ▷ M ≫
        f ▷ M ▷ M ≫
          Iso.hom (α_ N M M) ≫ N ◁ g ▷ M ≫ Iso.inv (α_ N N M) ≫ (tensorObj.{v₁, u₁} (𝒞 := inst) N N ◁ h ≫ μ ▷ N) ≫ μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M M) Δ
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) N (tensorObj.{v₁, u₁} (𝒞 := inst) N N))
          (((M ◁ Δ ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ N ◁ g ▷ M) ≫ N ◁ N ◁ h) (N ◁ μ) ≫
        μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f : Conv M N
⊢ 1 * f = f

Tactic:
simp [one_eq, mul_eq, ← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Conv.one_eq, CategoryTheory.Conv.mul_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Conv
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : C
inst_2 : ComonObj M
inst_3 : MonObj N
f : Conv M N
⊢ f * 1 = f

Tactic:
simp [one_eq, mul_eq, ← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Conv.one_eq, CategoryTheory.Conv.mul_eq
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C × C
f : x ⟶ y
⊢ (F ⊠ G).map f ≫
      Iso.hom (β_ ((F, G).1.obj y.1) ((F, G).2.obj y.2)) ≫
        NatTrans.app (unit G F) (y.2, y.1) ≫
          (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (y.2, y.1).1 (y.2, y.1).2)) =
    (Iso.hom (β_ ((F, G).1.obj x.1) ((F, G).2.obj x.2)) ≫
        NatTrans.app (unit G F) (x.2, x.1) ≫
          (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (x.2, x.1).1 (x.2, x.1).2))) ≫
      (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G F _).map f

Tactic:
simp [tensorHom_def, ← Functor.map_comp]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C × C
f : x ⟶ y
⊢ (G ⊠ F).map f ≫
      Iso.inv (β_ ((G, F).2.obj y.2) ((G, F).1.obj y.1)) ≫
        NatTrans.app (unit F G) (y.2, y.1) ≫
          (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (y.2, y.1).2 (y.2, y.1).1)) =
    (Iso.inv (β_ ((G, F).2.obj x.2) ((G, F).1.obj x.1)) ≫
        NatTrans.app (unit F G) (x.2, x.1) ≫
          (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (x.2, x.1).2 (x.2, x.1).1))) ≫
      (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).map f

Tactic:
simp [tensorHom_def, ← Functor.map_comp]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
F₁ :
  CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
      (NatTrans.app (unit F G) (x, y))
      (NatTrans.app (Iso.hom (braiding F G)) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (x, y))) =
    Iso.hom (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)) ≫
      NatTrans.app (unit G F) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (y, x).1 (y, x).2))
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
      (NatTrans.app (unit F G) (x, y)) (NatTrans.app (Iso.hom (braiding F G)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)) =
    Iso.hom (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)) ≫
      NatTrans.app (unit G F) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (y, x).1 (y, x).2))

Tactic:
change
    (unit F G).app (x, y) ≫ (braiding F G).hom.app ((tensor C).obj (x, y)) = _

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.braiding, CategoryTheory.MonoidalCategory.tensor, Prod.mk, CategoryTheory.Iso.hom, CategoryTheory.MonoidalCategory.DayConvolution.unit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F G _).obj (x, y))
      (NatTrans.app (unit F G) (x, y))
      (NatTrans.app (Iso.hom (braiding F G)) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (x, y))) =
    Iso.hom (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)) ≫
      NatTrans.app (unit G F) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 G F _).map (Iso.hom (β_ (y, x).1 (y, x).2))

Tactic:
simp [braiding, braidingHomCorepresenting, -tensor_obj]

Premises used: CategoryTheory.MonoidalCategory.tensor_obj, CategoryTheory.MonoidalCategory.DayConvolution.braiding, CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
G₁ :
  CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G F _).obj (x, y))
      (NatTrans.app (unit G F) (x, y))
      (NatTrans.app (Iso.inv (braiding F G)) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (x, y))) =
    Iso.inv (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)) ≫
      NatTrans.app (unit F G) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (y, x).2 (y, x).1))
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G F _).obj (x, y))
      (NatTrans.app (unit G F) (x, y)) (NatTrans.app (Iso.inv (braiding F G)) (tensorObj.{v₁, u₁} (𝒞 := inst) x y)) =
    Iso.inv (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)) ≫
      NatTrans.app (unit F G) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (y, x).2 (y, x).1))

Tactic:
change
    (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) = _

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.braiding, CategoryTheory.MonoidalCategory.tensor, Prod.mk, CategoryTheory.Iso.inv, CategoryTheory.MonoidalCategory.DayConvolution.unit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F G
inst_7 : DayConvolution G F
x y : C
⊢ CategoryStruct.comp (Y := (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G F _).obj (x, y))
      (NatTrans.app (unit G F) (x, y))
      (NatTrans.app (Iso.inv (braiding F G)) (Functor.obj.{v₁, v₁, u₁, u₁} (tensor C) (x, y))) =
    Iso.inv (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)) ≫
      NatTrans.app (unit F G) (y, x) ≫ (@convolution _ _ _ _ inst_2 inst_4 F G _).map (Iso.inv (β_ (y, x).2 (y, x).1))

Tactic:
simp [braiding, braidingHomCorepresenting, -tensor_obj]

Premises used: CategoryTheory.MonoidalCategory.tensor_obj, CategoryTheory.MonoidalCategory.DayConvolution.braiding, CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
hγ :
  Eq (α := H ⊠ F ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _)
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))))
⊢ Eq (α := @convolution _ _ _ _ inst_2 inst_4 H F _ ⟶ @convolution _ _ _ _ inst_2 inst_4 G H _)
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))

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

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.convolution, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolution.unit
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
hγ :
  ∀ (fst snd : C),
    Eq (α := (H ⊠ F).obj (fst, snd) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _).obj (fst, snd))
      (NatTrans.app
        (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
          (Functor.whiskerLeft (tensor C)
            (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η)
              (Iso.hom (braiding H G)))))
        (fst, snd))
      (NatTrans.app
        (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
          (Functor.whiskerLeft (tensor C)
            (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F))
              (map η (𝟙 H)))))
        (fst, snd))
⊢ Eq (α := H ⊠ F ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _)
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))))

Tactic:
ext ⟨_, _⟩
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G H : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
fst snd : C
⊢ Eq (α := (H ⊠ F).obj (fst, snd) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 G H _).obj (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H G _) (map (𝟙 H) η) (Iso.hom (braiding H G)))))
      (fst, snd))
    (NatTrans.app
      (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H F _) (unit H F)
        (Functor.whiskerLeft (tensor C)
          (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 F H _) (Iso.hom (braiding H F)) (map η (𝟙 H)))))
      (fst, snd))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
hγ :
  Eq (α := F ⊠ H ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _)
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))))
⊢ Eq (α := @convolution _ _ _ _ inst_2 inst_4 F H _ ⟶ @convolution _ _ _ _ inst_2 inst_4 H G _)
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))
    (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))

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

Premises used: CategoryTheory.MonoidalCategory.DayConvolution.convolution, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayConvolution.unit
-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : MonoidalCategory.{v₂, u₂} V
inst_5 : BraidedCategory.{v₂, u₂} V
F G : Functor.{v₁, v₂, u₁, u₂} C V
η : F ⟶ G
H : Functor.{v₁, v₂, u₁, u₂} C V
inst_6 : DayConvolution F H
inst_7 : DayConvolution H F
inst_8 : DayConvolution G H
inst_9 : DayConvolution H G
hγ :
  ∀ (fst snd : C),
    Eq (α := (F ⊠ H).obj (fst, snd) ⟶ (tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _).obj (fst, snd))
      (NatTrans.app
        (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
          (Functor.whiskerLeft (tensor C)
            (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H))
              (Iso.hom (braiding G H)))))
        (fst, snd))
      (NatTrans.app
        (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
          (Functor.whiskerLeft (tensor C)
            (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H))
              (map (𝟙 H) η))))
        (fst, snd))
⊢ Eq (α := F ⊠ H ⟶ tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 H G _)
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 G H _) (map η (𝟙 H)) (Iso.hom (braiding G H)))))
    (CategoryStruct.comp (Y := tensor C ⋙ @convolution _ _ _ _ inst_2 inst_4 F H _) (unit F H)
      (Functor.whiskerLeft (tensor C)
        (CategoryStruct.comp (Y := @convolution _ _ _ _ inst_2 inst_4 H F _) (Iso.hom (braiding F H)) (map (𝟙 H) η))))

Tactic:
ext ⟨_, _⟩