Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
a b c d : D
this✝² : DayConvolution (((ι C V D).obj a ⊛ (ι C V D).obj b) ⊛ (ι C V D).obj c) ((ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D ((a ⊗ b) ⊗ c) d
this✝¹ : DayConvolution ((ι C V D).obj a ⊛ (ι C V D).obj b) ((ι C V D).obj c ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D (a ⊗ b) (c ⊗ d)
this✝ : DayConvolution ((ι C V D).obj a ⊛ (ι C V D).obj b ⊛ (ι C V D).obj c) ((ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D (a ⊗ b ⊗ c) d
this : DayConvolution ((ι C V D).obj a) ((ι C V D).obj b ⊛ (ι C V D).obj c ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D a (b ⊗ c ⊗ d)
⊢ map (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj b) ((ι C V D).obj c)).hom (𝟙 ((ι C V D).obj d)) ≫
      (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj (b ⊗ c)) ((ι C V D).obj d)).hom ≫
        map (𝟙 ((ι C V D).obj a))
          (DayConvolution.associator ((ι C V D).obj b) ((ι C V D).obj c) ((ι C V D).obj d)).hom =
    (DayConvolution.associator ((ι C V D).obj (a ⊗ b)) ((ι C V D).obj c) ((ι C V D).obj d)).hom ≫
      (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj b) ((ι C V D).obj (c ⊗ d))).hom

Tactic:
let : DayConvolution
          (ι C V D |>.obj a)
          (((ι C V D |>.obj b) ⊛ (ι C V D |>.obj c)) ⊛ (ι C V D |>.obj d)) :=
        convolution C V D _ _

Goal state after:
C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
a b c d : D
this✝³ : DayConvolution (((ι C V D).obj a ⊛ (ι C V D).obj b) ⊛ (ι C V D).obj c) ((ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D ((a ⊗ b) ⊗ c) d
this✝² : DayConvolution ((ι C V D).obj a ⊛ (ι C V D).obj b) ((ι C V D).obj c ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D (a ⊗ b) (c ⊗ d)
this✝¹ : DayConvolution ((ι C V D).obj a ⊛ (ι C V D).obj b ⊛ (ι C V D).obj c) ((ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D (a ⊗ b ⊗ c) d
this✝ : DayConvolution ((ι C V D).obj a) ((ι C V D).obj b ⊛ (ι C V D).obj c ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D a (b ⊗ c ⊗ d)
this : DayConvolution ((ι C V D).obj a) (((ι C V D).obj b ⊛ (ι C V D).obj c) ⊛ (ι C V D).obj d) :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolution C V D a ((b ⊗ c) ⊗ d)
⊢ map (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj b) ((ι C V D).obj c)).hom (𝟙 ((ι C V D).obj d)) ≫
      (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj (b ⊗ c)) ((ι C V D).obj d)).hom ≫
        map (𝟙 ((ι C V D).obj a))
          (DayConvolution.associator ((ι C V D).obj b) ((ι C V D).obj c) ((ι C V D).obj d)).hom =
    (DayConvolution.associator ((ι C V D).obj (a ⊗ b)) ((ι C V D).obj c) ((ι C V D).obj d)).hom ≫
      (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj b) ((ι C V D).obj (c ⊗ d))).hom