∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
      CategoryTheory.CommSq.w._autoParam),
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr w)) →
    CategoryTheory.IsPushout f g inl inr