∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C × C} (Z : C × C) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Z.1 Z.2)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f.1 f.2))
      (CategoryTheory.MonoidalCategory.tensorμ Z.1 Z.2 Y.1 Y.2) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ Z.1 Z.2 X.1 X.2)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z.1 f.1)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z.2 f.2))