Composition with injective function is an injective operatio

Stream: Is there code for X?

[Heather Macbeth]

Is there a little collection of lemmas about injective functions somewhere? Where can this go?

lemma function.injective.comp_left {α β γ : Type*} {f₁ f₂ : α → β} {g : β → γ}
  (hg : function.injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ :=
begin
  refine funext (λ i, hg _),
  exact congr_fun hgf i,
end

[Yakov Pechersky]

Maybe have congr somewhere in the name?

[Anne Baanen]

Isn't there already something like docs#function.injective.of_comp? Sorry, mis-parsed the statement.

[Anne Baanen]

But the logic.function.basic file seems appropriate

[Eric Wieser]

Another version of that statement would be:

lemma function.injective.comp_left {α β γ : Type*} {g : β → γ}
  (hg : function.injective g) : function.injective ((∘) g : (α → β) → (α → γ)) :=
λ f₁ f₂ hgf, funext $ λ i, hg (congr_fun hgf i : _)