∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} (u : X ⟶ P)
  (v : Y ⟶ Q)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v)
      CategoryTheory.Arrow.homMk'._auto_1),
  (CategoryTheory.Arrow.homMk' u v w).left = u