∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) (g : CategoryTheory.MonoOver Y),
  CategoryTheory.Mono ((CategoryTheory.Over.pullback f).obj ((CategoryTheory.MonoOver.forget Y).obj g)).hom