∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) [inst_1 : CategoryTheory.Mono f]
  (g : Z ⟶ X), (CategoryTheory.Subobject.mk f).Factors g ↔ (CategoryTheory.MonoOver.mk f).Factors g