feat(Data/Set/Restrict): extend is injective on the range (leanprover-community#39856)

These lemmas are placed here since that puts them close to the other `extend` lemmas, but they can't be in Logic/Function/Basic since InjOn and Set.range aren't defined there yet

Author: b-mehta

Mathlib/Data/Set/Restrict.lean

@@ -129,6 +129,21 @@ theorem range_extend {f : α → β} (hf : Injective f) (g : α → γ) (g' : β
   rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
   exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
 
+/-- If `g` factors through `f` and `g` is injective, then `extend f g j` is injective on the
+range of `f`. -/
+lemma _root_.Function.FactorsThrough.extend_injOn {f : α → β} {g : α → γ} {j : β → γ}
+    (hf : g.FactorsThrough f) (hg : g.Injective) :
+    (range f).InjOn (extend f g j) := by
+  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ heq
+  rw [hf.extend_apply, hf.extend_apply] at heq
+  rw [hg heq]
+
+/-- If `f` and `g` are injective, then `extend f g j` is injective on the range of `f`. -/
+lemma _root_.Function.Injective.extend_injOn {f : α → β} {g : α → γ} {j : β → γ}
+    (hf : f.Injective) (hg : g.Injective) :
+    (range f).InjOn (extend f g j) :=
+  (hf.factorsThrough g).extend_injOn hg
+
 /-- Restrict codomain of a function `f` to a set `s`. Same as `Subtype.coind` but this version
 has codomain `↥s` instead of `Subtype s`. -/
 def codRestrict (f : ι → α) (s : Set α) (h : ∀ x, f x ∈ s) : ι → s := fun x => ⟨f x, h x⟩