∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_4} [inst_2 : CategoryTheory.Category.{u_3, u_4} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddMonObj (F.obj X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
        (hF.preimage
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
            CategoryTheory.AddMonObj.zero)))
      (hF.preimage
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X)
          CategoryTheory.AddMonObj.add)) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom