-- 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 _ _ (X.obj (P := P)) (Z.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ Z) → 𝟙_ V ⟶ X.obj ⟶[V] 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))))
          ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ Y) → 𝟙_ V ⟶ X.obj ⟶[V] Y.obj) f ⊗ₘ
            (Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y.obj ⟶[V] 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 simp : 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: simp only [ObjectProperty.ι_obj, Equiv.trans_apply]