∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  {g : CategoryTheory.Over X}, CategoryTheory.Mono (CategoryTheory.Limits.image.ι g.hom)