∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Y} {s : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout s f] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [CategoryTheory.HasLiftingProperty s p],
  CategoryTheory.HasLiftingProperty (CategoryTheory.Limits.pushout.inr s f) p