∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) (tensorUnit : P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  (tensorObj : ∀ (X Y : C), P X → P Y → P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
  {X Y : P.FullSubcategory} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ObjectProperty.homMk
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom
          { obj := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, property := tensorUnit }.obj))
      (P.fullyFaithfulι.preimageIso (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y.obj)).hom =
    CategoryTheory.CategoryStruct.comp
      (P.fullyFaithfulι.preimageIso (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj)).hom f