-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X Y Z : P.FullSubcategory
f : X ⟶ Y
g : Y ⟶ Z
change :
  Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (P.ι.obj X) (P.ι.obj Z))
    ((eHomEquiv V : (a : P.ι.obj X ⟶ P.ι.obj Z) → 𝟙_ V ⟶ P.ι.obj X ⟶[V] P.ι.obj Z) (P.ι.map (f ≫ g)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (P.ι.obj X) (P.ι.obj Z))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst_4) (tensorUnit.{v', u'} V (𝒞 := inst_4)) (tensorUnit.{v', u'} V (𝒞 := inst_4)))
        (Iso.inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst_4))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst_4)
            (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Y.obj (P := P)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (Y.obj (P := P)) (Z.obj (P := P))))
          ((eHomEquiv V : (a : X.obj ⟶ Y.obj) → 𝟙_ V ⟶ X.obj ⟶[V] Y.obj)
              ((P.fullyFaithfulι.homEquiv : (a : X ⟶ Y) → X.obj ⟶ Y.obj) f) ⊗ₘ
            (eHomEquiv V : (a : Y.obj ⟶ Z.obj) → 𝟙_ V ⟶ Y.obj ⟶[V] Z.obj)
              ((P.fullyFaithfulι.homEquiv : (a : Y ⟶ Z) → Y.obj ⟶ Z.obj) g))
          (eComp V X Y Z)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Z.obj (P := P)))
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Z.obj (P := P)))
    ((eHomEquiv V : (a : X.obj ⟶ Z.obj) → 𝟙_ V ⟶ X.obj ⟶[V] Z.obj)
        ((P.fullyFaithfulι.homEquiv : (a : X ⟶ Z) → X.obj ⟶ Z.obj) (f ≫ g)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Z.obj (P := P)))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst_4) (tensorUnit.{v', u'} V (𝒞 := inst_4)) (tensorUnit.{v', u'} V (𝒞 := inst_4)))
        (Iso.inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst_4))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst_4)
            (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Y.obj (P := P)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (Y.obj (P := P)) (Z.obj (P := P))))
          ((eHomEquiv V : (a : X.obj ⟶ Y.obj) → 𝟙_ V ⟶ X.obj ⟶[V] Y.obj)
              ((P.fullyFaithfulι.homEquiv : (a : X ⟶ Y) → X.obj ⟶ Y.obj) f) ⊗ₘ
            (eHomEquiv V : (a : Y.obj ⟶ Z.obj) → 𝟙_ V ⟶ Y.obj ⟶[V] Z.obj)
              ((P.fullyFaithfulι.homEquiv : (a : Y ⟶ Z) → Y.obj ⟶ Z.obj) g))
          (eComp V X Y Z)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Z.obj (P := P)))

Tactic:
change (eHomEquiv V) (P.ι.map (f ≫ g)) = _

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.eHomEquiv