-- 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 d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : 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))
    (CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
        Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
    (β :=
    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))
have 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 sorry ≫
    CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom sorry)
      (Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
  (β :=
  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 sorry ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom sorry) :
    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]