-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
X Y Z : (↑h.smallCategoryOfSet.obj : Type w)
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
    (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom X Z) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))) :
          (a : (↑(h.hom X Z) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) X ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Z)
        (x ≫ x_1) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
    (CategoryStruct.comp (Y := (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y)
        (((h.homEquiv :
              Equiv.{w + 1, v + 1} (↑(h.hom X Y) : Type w)
                (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
                  ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Y : C))) :
            (a : (↑(h.hom X Y) : Type w)) →
              (h.objEquiv : (a : (↑h.obj : Type w)) → C) X ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y)
          x)
        (((h.homEquiv :
              Equiv.{w + 1, v + 1} (↑(h.hom Y Z) : Type w)
                (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Y : C)
                  ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))) :
            (a : (↑(h.hom Y Z) : Type w)) →
              (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Z)
          x_1) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
have rw : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
    ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
  (((h.homEquiv :
          Equiv.{w + 1, v + 1} (↑(h.hom X Z) : Type w)
            (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
              ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))) :
        (a : (↑(h.hom X Z) : Type w)) →
          (h.objEquiv : (a : (↑h.obj : Type w)) → C) X ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Z)
      (h.smallCategoryOfSet.comp x x_1) :
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
  (CategoryStruct.comp (Y := (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y)
      (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom X Y) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Y : C))) :
          (a : (↑(h.hom X Y) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) X ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y)
        x)
      (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom Y Z) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Y : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))) :
          (a : (↑(h.hom Y Z) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) Y ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) Z)
        x_1) :
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) Z : C))
Tactic: rw [SmallCategoryOfSet.comp_def]