∀ {V : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {W : Type u_4} [inst_2 : CategoryTheory.Category.{u_2, u_4} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u_5)
  [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f))
  {X Y : CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D)} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))).map f)
      ((fun x =>
            CategoryTheory.Iso.refl
              ((CategoryTheory.Functor.id
                    (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))).obj
                x))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Iso.refl
              ((CategoryTheory.Functor.id
                    (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))).obj
                x))
          X).hom
      (((CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h).comp
            (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h)).map
        f)