-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_inv_app_hom_apply_app : ∀ {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 H X : CategoryTheory.Functor C V)
  (a :
    (((CategoryTheory.Functor.whiskeringLeft (C × C × C) C V).obj
              (((CategoryTheory.Functor.id C).prod (CategoryTheory.MonoidalCategory.tensor C)).comp
                (CategoryTheory.MonoidalCategory.tensor C))).comp
          (CategoryTheory.coyoneda.obj
            (Opposite.op
              (CategoryTheory.MonoidalCategory.externalProduct F
                (CategoryTheory.MonoidalCategory.externalProduct G H))))).obj
      X)
  (X_1 : (C × C) × C),
  ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso F G H).inv.app X))
          a).app
      X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (F.map ((CategoryTheory.prod.associativity C C C).unit.app X_1).1.1) (G.obj X_1.1.2))
        (H.obj X_1.2))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X_1.1.1) (G.obj X_1.1.2) (H.obj X_1.2)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X_1.1.1)
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (G.map ((CategoryTheory.prod.associativity C C C).unit.app X_1).1.2) (H.obj X_1.2)))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X_1.1.1)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (G.obj X_1.1.2)
                (H.map ((CategoryTheory.prod.associativity C C C).unit.app X_1).2)))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X_1.1.1) (G.obj X_1.1.2) (H.obj X_1.2)).inv
              (CategoryTheory.CategoryStruct.comp
                (((CategoryTheory.CategoryStruct.id
                          ((CategoryTheory.prod.inverseAssociator C C C).comp
                              (CategoryTheory.MonoidalCategory.externalProduct
                                (CategoryTheory.MonoidalCategory.externalProduct F G) H) ⟶
                            (CategoryTheory.prod.inverseAssociator C C C).comp
                              (((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)).comp
                                ((CategoryTheory.MonoidalCategory.tensor C).comp X)))).hom'
                      ((TypeCat.ofHom fun g =>
                            CategoryTheory.CategoryStruct.comp g
                              (((CategoryTheory.Functor.whiskeringLeft (C × C × C) C V).map
                                    (CategoryTheory.NatIso.ofComponents
                                        (fun x => CategoryTheory.MonoidalCategoryStruct.associator x.1 x.2.1 x.2.2)
                                        ⋯).inv).app
                                X)).hom'
                        ((TypeCat.ofHom fun g =>
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.NatIso.ofComponents
                                    (fun x =>
                                      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj x.1) (G.obj x.2.1)
                                          (H.obj x.2.2)).symm)
                                    ⋯).inv
                                g).hom'
                          a))).app
                  (X_1.1.1, X_1.1.2, X_1.2))
                (CategoryTheory.CategoryStruct.comp
                  (X.map (CategoryTheory.MonoidalCategoryStruct.associator X_1.1.1 X_1.1.2 X_1.2).hom)
                  (CategoryTheory.CategoryStruct.comp
                    (X.map
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom
                        ((CategoryTheory.prod.associativity C C C).unitInv.app X_1).1.1
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom
                          ((CategoryTheory.prod.associativity C C C).unitInv.app X_1).1.2
                          ((CategoryTheory.prod.associativity C C C).unitInv.app X_1).2)))
                    (X.map (CategoryTheory.MonoidalCategoryStruct.associator X_1.1.1 X_1.1.2 X_1.2).inv))))))))