Inverse_of_Many_to_One_Relation_is_One_to_Many

import Mathlib.Data.Set.Function
import Mathlib.Logic.Function.Basic

theorem Inverse_of_Many_to_One_Relation_is_One_to_Many {α β : Type _} (f : α → β) : Function.Injective (fun p : α × α => (f p.1, f p.2)) → ∀ y : β, ∀ x₁ x₂ : α, f x₁ = y → f x₂ = y → x₁ = x₂ := by sorry