-- 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
rw :
  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'))
          (CategoryStruct.comp (Y :=
            MonoidalCategoryStruct.tensorObj (𝒞 := Cat.category)
              (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category)))
            (Iso.inv (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))))
            (MonoidalCategoryStruct.tensorHom
                ((eHomEquiv Cat : (a_1 : a ⟶ b) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] b) f)
                ((eHomEquiv Cat : (a : b ⟶ c) → MonoidalCategoryStruct.tensorUnit Cat ⟶ b ⟶[Cat] c) g) ≫
              eComp Cat a b c))) :
      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)
    ((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:
rw [eHomEquiv_comp]

Premises used: CategoryTheory.eHomEquiv_comp