-- Module: Mathlib.CategoryTheory.SmallRepresentatives
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
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))
⊢ 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))

Tactic:
rw [SmallCategoryOfSet.comp_def]

Premises used: CategoryTheory.SmallCategoryOfSet.comp_def