∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] {g : X ⟶ Y} (h : f = g),
  P.HasPullbacksAlong g →
    ∀ (X_1 : P.Over Q Y),
      CategoryTheory.Limits.HasPullback X_1.hom g →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.congrHom ⋯ h).hom
            ((CategoryTheory.MorphismProperty.Over.pullback P Q g).obj X_1).hom =
          ((CategoryTheory.MorphismProperty.Over.pullback P Q f).obj X_1).hom