feat: characterise when Set.rangeFactorization is injective (#30126)

Author: YaelDillies

Mathlib/Data/Set/Image.lean

@@ -880,9 +880,6 @@ theorem rangeFactorization_coe (f : ι → β) (a : ι) : (rangeFactorization f
 @[simp]
 theorem coe_comp_rangeFactorization (f : ι → β) : (↑) ∘ rangeFactorization f = f := rfl
 
-theorem rangeFactorization_surjective : Surjective (rangeFactorization f) :=
-  fun ⟨_, ⟨i, rfl⟩⟩ => ⟨i, rfl⟩
-
 @[deprecated (since := "2025-08-18")] alias surjective_onto_range := rangeFactorization_surjective
 
 theorem image_eq_range (f : α → β) (s : Set α) : f '' s = range fun x : s => f x := by

Mathlib/Data/Set/Operations.lean

@@ -156,6 +156,16 @@ def range (f : ι → α) : Set α := {x | ∃ y, f y = x}
 /-- Any map `f : ι → α` factors through a map `rangeFactorization f : ι → range f`. -/
 def rangeFactorization (f : ι → α) : ι → range f := fun i => ⟨f i, mem_range_self i⟩
 
+@[simp] lemma rangeFactorization_injective :
+    (Set.rangeFactorization f).Injective ↔ f.Injective := by
+  simp [Function.Injective, rangeFactorization]
+
+@[simp] lemma rangeFactorization_surjective : (rangeFactorization f).Surjective :=
+  fun ⟨_, i, rfl⟩ ↦ ⟨i, rfl⟩
+
+@[simp] lemma rangeFactorization_bijective :
+    (Set.rangeFactorization f).Bijective ↔ f.Injective := by simp [Function.Bijective]
+
 end Range
 
 /-- We can use the axiom of choice to pick a preimage for every element of `range f`. -/