∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) {X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}} (f : X ⟶ Y)
  (X' : CategoryTheory.Discrete PUnit.{u_1 + 1}),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).map f)
        ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).obj X'))
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))