∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [inst : CategoryTheory.MonoidalCategory C] {X Y Z : C} (f : X ≅ Y)
  (g : Y ≅ Z) (W : C),
  CategoryTheory.MonoidalCategory.whiskerRightIso (f ≪≫ g) W =
    CategoryTheory.MonoidalCategory.whiskerRightIso f W ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso g W