∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {a b c : CategoryTheory.EnrichedCat V} {f g h : CategoryTheory.EnrichedFunctor V ↑a ↑b} (α : f ⟶ g) (β : g ⟶ h)
  (I : CategoryTheory.EnrichedFunctor V ↑b ↑c),
  CategoryTheory.EnrichedCat.whiskerRight { out := CategoryTheory.CategoryStruct.comp α.out β.out } I =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α I)
      (CategoryTheory.EnrichedCat.whiskerRight β I)