∀ {C : Type u_4} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{u_1, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (c : C) (d : D),
  (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom).unmop.app d =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.Monoidal.μIso F c (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).unmop.app
            d).symm.hom
      ((F.obj c).unmop.map ((CategoryTheory.Functor.Monoidal.εIso F).unmop.app d).symm.hom)