∀ {I : Type u_2} {C : I → Type u_3} [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)]
  (X : (i : I) → C i) {Y Z : (i : I) → C i} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.Pi.isoMk fun i => β_ (X i) (Z i)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pi.isoMk fun i => β_ (X i) (Y i)).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)