∀ {C : Type u_3} {D : Type u_4} {E : Type u_6} [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] [inst_2 : CategoryTheory.Category.{u_5, u_6} E]
  [inst_3 : CategoryTheory.MonoidalCategory D] [inst_4 : CategoryTheory.MonoidalCategory E]
  (L : CategoryTheory.Functor D E) [inst_5 : L.OplaxMonoidal] {X Y : CategoryTheory.Functor C D} (f : X ⟶ Y)
  (X' : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp
      { app := fun X_1 => CategoryTheory.Functor.OplaxMonoidal.δ L (X.obj X_1) (X'.obj X_1), naturality := ⋯ }
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (((CategoryTheory.Functor.whiskeringRight C D E).obj L).map f)
        (((CategoryTheory.Functor.whiskeringRight C D E).obj L).obj X')) =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.whiskeringRight C D E).obj L).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
      { app := fun X => CategoryTheory.Functor.OplaxMonoidal.δ L (Y.obj X) (X'.obj X), naturality := ⋯ }