Injection_iff_Left_Cancellable

import Mathlib.Logic.Function.Basic

theorem Injection_iff_Left_Cancellable {α β : Type _} (f : α → β) : Function.Injective f ↔ ∀ {γ : Type _} (g₁ g₂ : γ → α), f ∘ g₁ = f ∘ g₂ → g₁ = g₂ := by sorry