∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} (f : Z ⟶ X) (g : Z ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.IsPushout f g (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g)