-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.Arrow C)
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.left)]
  [inst_4 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.right)]
  [inst_5 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.left)]
  [inst_6 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.right)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator X₁ X₂ X₃).hom.left =
    CategoryTheory.Limits.pushout.desc
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.right X₃.left).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right
            (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom)))
          (CategoryTheory.Limits.pushout.inl
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom
              (CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom)))
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left
              (CategoryTheory.Limits.pushout.desc (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.right X₃.hom)
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.right) ⋯)))))
      (CategoryTheory.CategoryStruct.comp ⋯.isoPushout.hom
        (CategoryTheory.Limits.colimit.desc
          (CategoryTheory.Limits.span
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left) X₃.right)
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom) X₃.right))
          ((CategoryTheory.Limits.Cocone.precompose
                (CategoryTheory.Limits.spanExt
                    (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.left X₃.right)
                    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.left X₃.right)
                    (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.right X₃.right) ⋯ ⋯).hom).obj
            (CategoryTheory.Limits.PushoutCocone.mk
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.right
                  (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom)))
                (CategoryTheory.Limits.pushout.inl
                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom
                    (CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom)))
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left
                    (CategoryTheory.Limits.pushout.desc
                      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.right X₃.hom)
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.right) ⋯))))
              (CategoryTheory.Limits.pushout.inr
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom
                  (CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom)))
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left
                  (CategoryTheory.Limits.pushout.desc
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.right X₃.hom)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.right) ⋯)))
              ⋯))))
      ⋯