∀ (V : Type u_4) [inst : CategoryTheory.Category.{u_3, u_4} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D]
  {X Y : D} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.ForgetEnrichment.equivInverse V D).comp (CategoryTheory.ForgetEnrichment.equivFunctor V D)).map
        f)
      ((fun X =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.ForgetEnrichment.equivInverse V D).comp
                    (CategoryTheory.ForgetEnrichment.equivFunctor V D)).obj
                X))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.ForgetEnrichment.equivInverse V D).comp
                    (CategoryTheory.ForgetEnrichment.equivFunctor V D)).obj
                X))
          X).hom
      ((CategoryTheory.Functor.id D).map f)