-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
V_1 : Type u₂
inst_1 : Category.{v₂, u₂} V_1
inst_2 : MonoidalCategory.{v₁, u₁} C_1
inst_3 : MonoidalCategory.{v₂, u₂} V_1
C : Type u₁
inst_4 : Category.{v₁, u₁} C
V : Type u₂
inst_5 : Category.{v₂, u₂} V
inst_6 : MonoidalCategory.{v₁, u₁} C
inst_7 : MonoidalCategory.{v₂, u₂} V
D : Type u₃
inst_8 : Category.{v₃, u₃} D
inst_9 : InducedLawfulDayConvolutionMonoidalCategoryStructCore.{v₁, v₂, v₃, u₁, u₂, u₃} C V D
d d' : D
X Y : C × C
f : X ⟶ Y
simp :
  Eq.{v₂ + 1} (α :=
    Functor.obj.{v₁, v₂, u₁, u₂}
        (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d ⊠ Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') X ⟶
      Functor.obj.{v₁, v₂, u₁, u₂}
        (tensor C ⋙
          Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
            (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
        Y)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₂, u₁, u₂}
        (tensor C ⋙
          @DayConvolution.convolution _ _ _ _ inst_6 inst_7 (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
            (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') _)
        X)
      (NatTrans.app
        (DayConvolution.unit (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
          (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d'))
        X)
      (Functor.map
          (tensor C ⋙
            @DayConvolution.convolution _ _ _ _ inst_6 inst_7 (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
              (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') _)
          f ≫
        NatTrans.app (Iso.inv (tensorObjIsoConvolution C V d d'))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst_4) Y.1 Y.2)))
    (NatTrans.app
        (DayConvolution.unit (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
          (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d'))
        (X.1, X.2) ≫
      NatTrans.app (Iso.inv (tensorObjIsoConvolution C V d d'))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst_4) X.1 X.2) ≫
        Functor.map
          (tensor C ⋙
            Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
              (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
          f)
⊢ Eq.{v₂ + 1} (α :=
    Functor.obj.{v₁, v₂, u₁, u₂}
        (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d ⊠ Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') X ⟶
      Functor.obj.{v₁, v₂, u₁, u₂}
        (tensor C ⋙
          Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
            (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
        Y)
    (Functor.map (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d ⊠ Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') f ≫
      convolutionUnitApp V d d' Y.1 Y.2)
    (convolutionUnitApp V d d' X.1 X.2 ≫
      Functor.map
        (tensor C ⋙
          Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
            (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
        f)

Tactic:
simp only [convolutionUnitApp_eq, Category.assoc, NatTrans.naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq, CategoryTheory.NatTrans.naturality_assoc