∀ {J : Type u_1} [inst : LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) (x x_1 : SimplexCategoryᵒᵖ)
  (x_2 : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j)
            (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom j k)).map
        x_2)
      ((fun x x_3 => (CategoryTheory.Functor.prod' x_3.1 x_3.2).comp (i.compFunctor j k)) x_1) =
    CategoryTheory.CategoryStruct.comp
      ((fun x x_3 => (CategoryTheory.Functor.prod' x_3.1 x_3.2).comp (i.compFunctor j k)) x)
      ((CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i k).map x_2)