-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Ordinary.Basic (goal)
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
⊢ 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)))
have rw : Eq.{v' + 1} (α :=
  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 _ _ (P.ι.obj X) (P.ι.obj Y))
        (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (P.ι.obj Y) (P.ι.obj Z)))
      ((eHomEquiv V : (a : P.ι.obj X ⟶ P.ι.obj Y) → 𝟙_ V ⟶ P.ι.obj X ⟶[V] P.ι.obj Y) (P.ι.map f) ⊗ₘ
        (eHomEquiv V : (a : P.ι.obj Y ⟶ P.ι.obj Z) → 𝟙_ V ⟶ P.ι.obj Y ⟶[V] P.ι.obj Z) (P.ι.map g))
      (eComp V (P.ι.obj X) (P.ι.obj Y) (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)))
Tactic: rw [Functor.map_comp, eHomEquiv_comp]