∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C}
  [inst_3 : P'.IsMonoidal] (h : P ≤ P') (X : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((CategoryTheory.ObjectProperty.ιOfLE h).obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit P'.FullSubcategory)).hom
        ((CategoryTheory.ObjectProperty.ιOfLE h).obj X))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              ((CategoryTheory.ObjectProperty.ιOfLE h).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory))
              ((CategoryTheory.ObjectProperty.ιOfLE h).obj X))).hom
        ((CategoryTheory.ObjectProperty.ιOfLE h).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))