-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.pentagon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (H K : CategoryTheory.Functor C V) [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_9 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_10 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_11 : CategoryTheory.MonoidalCategory.DayConvolution H K]
  [inst_12 :
    CategoryTheory.MonoidalCategory.DayConvolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K)]
  [inst_13 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) K]
  [inst_14 :
    CategoryTheory.MonoidalCategory.DayConvolution
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution
        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
      K]
  [inst_15 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K)]
  [inst_16 :
    CategoryTheory.MonoidalCategory.DayConvolution
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F
        (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H))
      K]
  [inst_17 :
    CategoryTheory.MonoidalCategory.DayConvolution F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution G
        (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K))]
  [inst_18 :
    CategoryTheory.MonoidalCategory.DayConvolution F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution
        (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) K)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map
        (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom (CategoryTheory.CategoryStruct.id K))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.associator F
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) K).hom
        (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F)
          (CategoryTheory.MonoidalCategory.DayConvolution.associator G H K).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.associator
          (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H K).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.associator F G
          (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K)).hom