∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  {X Y : CategoryTheory.MonoOver A} (k : X ⟶ Y) (g : CategoryTheory.MonoOver A),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.Limits.pullback.fst ((CategoryTheory.MonoOver.forget A).obj g).hom X.arrow)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget A).obj g).hom X.arrow) k.hom.left)
        ⋯)
      (((CategoryTheory.MonoOver.pullback Y.arrow).comp (CategoryTheory.MonoOver.map Y.arrow)).obj g).arrow =
    (((CategoryTheory.MonoOver.pullback X.arrow).comp (CategoryTheory.MonoOver.map X.arrow)).obj g).arrow