-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (goal)
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 : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)
e_f :
  Eq.{v'' + 1} (α :=
    tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
      F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
    ((e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)) :
          (a : 𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X) →
            𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
        ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))) :
            (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) →
              𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)
          (eId W (ForgetEnrichment.to W X))) :
      tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
        F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
    ((e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)) :
          (a : 𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X) →
            𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
        (eId V (ForgetEnrichment.to W X)) :
      tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
        F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
e_f₁ :
  Eq.{v'' + 1} (α :=
    tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
      F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
    (eId W (ForgetEnrichment.to W X) :
      tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
        @Hom.{v'', u'', u} _ inst_7 inst_8 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))
    ((e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)) :
        (a : 𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X) →
          𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
      (eId V (ForgetEnrichment.to W X)))
⊢ Eq.{v'' + 1} (α :=
    tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
      F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
    ((e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)) :
          (a : 𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X) →
            𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
        ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))) :
            (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) →
              𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)
          (ForgetEnrichment.homTo W (𝟙 X))) :
      tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
        F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
    ((e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)) :
          (a : 𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X) →
            𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
        (eId V (ForgetEnrichment.to W X)) :
      tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
        F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
have e_f₂ : Eq.{v'' + 1} (α :=
  tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
    F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X)))
  (eId W (ForgetEnrichment.to W X) :
    tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶
      @Hom.{v'', u'', u} _ inst_7 inst_8 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W X))
  (Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to W X)))
Tactic: rw [ForgetEnrichment.homTo_id, Equiv.apply_symm_apply, h, TransportEnrichment.eId_eq]