-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
H :
  HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
          ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g ≫ h)) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
          ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g' ≫ h')) :
        a.toBase ⟶ d.toBase))
    (eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
        (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯))
⊢ HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
          ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g ≫ h)) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
          ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g' ≫ h')) :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp
        (𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) ≫
          Hom.base η ≫ 𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
        (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯) :
      Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
        (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
            ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g ≫ h)) :
          a.toBase ⟶ d.toBase)
        (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
            ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g' ≫ h')) :
          a.toBase ⟶ d.toBase))

Tactic:
rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

Premises used: CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom, CategoryTheory.CatEnriched.eqToHom_hComp_eqToHom, CategoryTheory.CatEnriched.hComp_comp