-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
    ((Equiv.trans (eHomEquiv Cat)
            (Equiv.trans
              (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a c))
              Cat.fromChosenTerminalEquiv) :
          (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase)
        (f ≫ g) :
      a.toBase ⟶ c.toBase)
    (CategoryStruct.comp (Y := b.toBase)
        ((Equiv.trans (eHomEquiv Cat)
              (Equiv.trans
                (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                  (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a b))
                Cat.fromChosenTerminalEquiv) :
            (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase)
          f)
        ((Equiv.trans (eHomEquiv Cat)
              (Equiv.trans
                (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                  (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ b c))
                Cat.fromChosenTerminalEquiv) :
            (a : b ⟶ c) → b.toBase ⟶ c.toBase)
          g) :
      a.toBase ⟶ c.toBase)
have simp : Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
  ((Cat.fromChosenTerminalEquiv :
        (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] c) : Type u')) → a.toBase ⟶ c.toBase)
      ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
            (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a c) :
          (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] c) →
            (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] c) : Type u'))
        ((eHomEquiv Cat : (a_1 : a ⟶ c) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] c) (f ≫ g))) :
    a.toBase ⟶ c.toBase)
  (CategoryStruct.comp (Y := b.toBase)
      ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] b) : Type u')) →
            a.toBase ⟶ b.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a b) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] b) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] b) : Type u'))
          ((eHomEquiv Cat : (a_1 : a ⟶ b) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] b) f)))
      ((Cat.fromChosenTerminalEquiv :
          (a : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(b ⟶[Cat] c) : Type u')) → b.toBase ⟶ c.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ b c) :
            (a : MonoidalCategoryStruct.tensorUnit Cat ⟶ b ⟶[Cat] c) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(b ⟶[Cat] c) : Type u'))
          ((eHomEquiv Cat : (a : b ⟶ c) → MonoidalCategoryStruct.tensorUnit Cat ⟶ b ⟶[Cat] c) g))) :
    a.toBase ⟶ c.toBase)
Tactic: simp only [Equiv.trans_apply]