∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C] {d d' : C}
  (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor d).hom f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor d').hom