∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g}
  (hc : CategoryTheory.Limits.IsColimit c),
  Function.Injective f → ∀ (x₁ : X₁) (x₂ : X₂), c.inl x₁ = c.inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂