-- 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)
    ((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)
have 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)
Tactic: rw [eHomEquiv_comp]