∀ {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)
  (create :
    (s : CategoryTheory.Limits.PushoutCocone f g) →
      { l //
        CategoryTheory.CategoryStruct.comp t.inl l = s.inl ∧
          CategoryTheory.CategoryStruct.comp t.inr l = s.inr ∧
            ∀ {m : t.pt ⟶ s.pt},
              CategoryTheory.CategoryStruct.comp t.inl m = s.inl →
                CategoryTheory.CategoryStruct.comp t.inr m = s.inr → m = l })
  (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp t.inl ↑(create s) = s.inl