∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z ≪≫
      β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ≪≫
        CategoryTheory.MonoidalCategoryStruct.associator Y Z X =
    CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫
      CategoryTheory.MonoidalCategoryStruct.associator Y X Z ≪≫
        CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z)