-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
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
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)
⊢ 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)

Tactic:
simp only [Equiv.trans_apply]

Premises used: Equiv.trans_apply