∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g) (desc : (s : CategoryTheory.Limits.PushoutCocone f g) → t.pt ⟶ s.pt),
  (∀ (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp t.inl (desc s) = s.inl) →
    (∀ (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp t.inr (desc s) = s.inr) →
      ∀ (s : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.span f g)) (j : CategoryTheory.Limits.WalkingSpan),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j