∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (f : A ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (h : CategoryTheory.Subobject.mk f ≤ X),
  CategoryTheory.Mono (CategoryTheory.Subobject.ofMkLE f X h)