∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y Z : CategoryTheory.Subobject X} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlying.map f) Z.arrow = Y.arrow