∀ {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.HasPushoutsAlong f] (A : P.Under Q X),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (P.Under Q X)).obj A).hom
      (CategoryTheory.Limits.pushout.inl ((CategoryTheory.Functor.id (P.Under Q X)).obj A).hom f) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.Limits.pushout.inr ((CategoryTheory.Functor.id (P.Under Q X)).obj A).hom f)