-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
simp :
  Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))))
    (𝟙 (ForgetEnrichment.of W X))
⊢ Eq (α := Functor.obj (forgetEnrichmentEquivFunctor F D e h) X ⟶ Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)
    (CategoryStruct.comp (Y :=
        Functor.obj (forgetEnrichmentEquivFunctor F D e h)
          (Functor.obj (forgetEnrichmentEquivInverse F D e h) (Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)))
        (Functor.map (forgetEnrichmentEquivFunctor F D e h)
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)) ↦
                  Iso.refl
                    (Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x))
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (x : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) ↦
                Iso.refl (Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x))
              ⋯))
          (Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)) :
      Functor.obj (forgetEnrichmentEquivFunctor F D e h) X ⟶ Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)
    (𝟙 (Functor.obj (forgetEnrichmentEquivFunctor F D e h) X) :
      Functor.obj (forgetEnrichmentEquivFunctor F D e h) X ⟶ Functor.obj (forgetEnrichmentEquivFunctor F D e h) X)

Tactic:
simp only [Functor.id_obj, forgetEnrichmentEquivFunctor_obj, Functor.comp_obj,
      forgetEnrichmentEquivInverse_obj, ForgetEnrichment.to_of, NatIso.ofComponents_hom_app,
      Iso.refl_hom, forgetEnrichmentEquivFunctor_map, h, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_obj, CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_obj, CategoryTheory.ForgetEnrichment.to_of, CategoryTheory.Iso.refl_hom, CategoryTheory.NatIso.ofComponents_hom_app, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map