chore: rename Set.surjective_onto_image (leanprover-community#28627)

Rename `Set.surjective_onto_image` to `Set.imageFactorization_surjective`. This matches better with other theorems like `Set.restrictPreimage_surjective`. Also rename `Set.surjective_onto_range` similarly.

I was looking on loogle today and noticed this one again, which doesn't fit any of the naming conventions. I decided to fix it this time.

Author: plp127

Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

@@ -25,7 +25,7 @@ namespace Subgroup
 theorem range_zpowersHom (g : G) : (zpowersHom G g).range = zpowers g := rfl
 
 @[to_additive]
-instance (a : G) : Countable (zpowers a) := Set.surjective_onto_range.countable
+instance (a : G) : Countable (zpowers a) := Set.rangeFactorization_surjective.countable
 
 end Subgroup
 

Mathlib/Data/Finite/Card.lean

@@ -146,10 +146,10 @@ theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α +
   simp only [Nat.card_eq_fintype_card, Fintype.card_sum]
 
 theorem card_image_le {s : Set α} [Finite s] (f : α → β) : Nat.card (f '' s) ≤ Nat.card s :=
-  card_le_of_surjective _ Set.surjective_onto_image
+  card_le_of_surjective _ Set.imageFactorization_surjective
 
 theorem card_range_le [Finite α] (f : α → β) : Nat.card (Set.range f) ≤ Nat.card α :=
-  card_le_of_surjective _ Set.surjective_onto_range
+  card_le_of_surjective _ Set.rangeFactorization_surjective
 
 theorem card_subtype_le [Finite α] (p : α → Prop) : Nat.card { x // p x } ≤ Nat.card α := by
   classical

Mathlib/Data/Set/Countable.lean

@@ -111,7 +111,7 @@ theorem Countable.mono {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (hs : s₂.Count
   have := hs.to_subtype; (inclusion_injective h).countable
 
 theorem countable_range [Countable ι] (f : ι → β) : (range f).Countable :=
-  surjective_onto_range.countable.to_set
+  rangeFactorization_surjective.countable.to_set
 
 theorem countable_iff_exists_subset_range [Nonempty α] {s : Set α} :
     s.Countable ↔ ∃ f : ℕ → α, s ⊆ range f :=

Mathlib/Data/Set/Image.lean

@@ -514,9 +514,12 @@ theorem imageFactorization_eq {f : α → β} {s : Set α} :
     Subtype.val ∘ imageFactorization f s = f ∘ Subtype.val :=
   funext fun _ => rfl
 
-theorem surjective_onto_image {f : α → β} {s : Set α} : Surjective (imageFactorization f s) :=
+theorem imageFactorization_surjective {f : α → β} {s : Set α} :
+    Surjective (imageFactorization f s) :=
   fun ⟨_, ⟨a, ha, rfl⟩⟩ => ⟨⟨a, ha⟩, rfl⟩
 
+@[deprecated (since := "2025-08-18")] alias surjective_onto_image := imageFactorization_surjective
+
 /-- If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.
 -/
 theorem image_perm {s : Set α} {σ : Equiv.Perm α} (hs : { a : α | σ a ≠ a } ⊆ s) : σ '' s = s := by
@@ -879,7 +882,10 @@ theorem rangeFactorization_coe (f : ι → β) (a : ι) : (rangeFactorization f
 @[simp]
 theorem coe_comp_rangeFactorization (f : ι → β) : (↑) ∘ rangeFactorization f = f := rfl
 
-theorem surjective_onto_range : Surjective (rangeFactorization f) := fun ⟨_, ⟨i, rfl⟩⟩ => ⟨i, 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
   ext

Mathlib/Logic/Small/Set.lean

@@ -30,11 +30,11 @@ instance small_setPi {β : α → Type u2} (s : (a : α) → Set (β a))
 
 instance small_range (f : α → β) [Small.{u} α] :
     Small.{u} (Set.range f) :=
-  small_of_surjective Set.surjective_onto_range
+  small_of_surjective Set.rangeFactorization_surjective
 
 instance small_image (f : α → β) (s : Set α) [Small.{u} s] :
     Small.{u} (f '' s) :=
-  small_of_surjective Set.surjective_onto_image
+  small_of_surjective Set.imageFactorization_surjective
 
 instance small_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Small.{u} s] [Small.{u} t] :
     Small.{u} (Set.image2 f s t) := by

Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

@@ -567,7 +567,8 @@ theorem measurableSet_preimage_iff_preimage_val {f : X → Z} [CountablySeparate
     (hf : Measurable f) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet ((↑) ⁻¹' s : Set (range f)) :=
   have hf' : Measurable (rangeFactorization f) := hf.subtype_mk
-  hf'.measurableSet_preimage_iff_of_surjective (s := Subtype.val ⁻¹' s) surjective_onto_range
+  hf'.measurableSet_preimage_iff_of_surjective (s := Subtype.val ⁻¹' s)
+    rangeFactorization_surjective
 
 /-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
 countably separated measurable space and the range of `f` is measurable,

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

@@ -629,7 +629,7 @@ theorem _root_.Topology.IsEmbedding.aestronglyMeasurable_comp_iff [PseudoMetriza
   · let G : β → range g := rangeFactorization g
     have hG : IsClosedEmbedding G :=
       { hg.codRestrict _ _ with
-        isClosed_range := by rw [surjective_onto_range.range_eq]; exact isClosed_univ }
+        isClosed_range := by rw [rangeFactorization_surjective.range_eq]; exact isClosed_univ }
     have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable
     exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this
   · rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -742,7 +742,7 @@ theorem _root_.Embedding.comp_stronglyMeasurable_iff {m : MeasurableSpace α} [T
     have hG : IsClosedEmbedding G :=
       { hg.codRestrict _ _ with
         isClosed_range := by
-          rw [surjective_onto_range.range_eq]
+          rw [rangeFactorization_surjective.range_eq]
           exact isClosed_univ }
     have : Measurable (G ∘ f) := Measurable.subtype_mk H.measurable
     exact hG.measurableEmbedding.measurable_comp_iff.1 this

Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

@@ -683,7 +683,7 @@ theorem of_measurable_inverse_on_range {g : range f → α} (hf₁ : Measurable
     (hf₂ : MeasurableSet (range f)) (hg : Measurable g) (H : LeftInverse g (rangeFactorization f)) :
     MeasurableEmbedding f := by
   set e : α ≃ᵐ range f :=
-    ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective surjective_onto_range⟩,
+    ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective rangeFactorization_surjective⟩,
       hf₁.subtype_mk, hg⟩
   exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding
 

Mathlib/Order/Filter/Finite.lean

@@ -120,7 +120,7 @@ theorem exists_iInter_of_mem_iInf {ι : Sort*} {α : Type*} {f : ι → Filter 
   rw [← iInf_range' (g := (·))] at hs
   let ⟨_, _, V, hVs, _, _, hVU'⟩ := mem_iInf'.1 hs
   use V ∘ rangeFactorization f, fun i ↦ hVs (rangeFactorization f i)
-  rw [hVU', ← surjective_onto_range.iInter_comp, comp_def]
+  rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]
 
 theorem mem_iInf_of_finite {ι : Sort*} [Finite ι] {α : Type*} {f : ι → Filter α} (s) :
     (s ∈ ⨅ i, f i) ↔ ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i := by