From a9d837b633f986c0e766f70f00c50391d54b3d6a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 4 Jul 2024 14:52:17 -0500
Subject: [PATCH] feat(Data/Set/Image): add `preimage_subset_of_surjOn`

Cherry-picked from #11143 and renamed.

Co-authored-by: @YaelDillies
---
 Mathlib/Data/Set/Image.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean
index 7fe173774b0d16..877bc5ce3234d4 100644
--- a/Mathlib/Data/Set/Image.lean
+++ b/Mathlib/Data/Set/Image.lean
@@ -220,6 +220,10 @@ theorem _root_.Function.Injective.mem_set_image {f : α → β} (hf : Injective
   ⟨fun ⟨_, hb, Eq⟩ => hf Eq ▸ hb, mem_image_of_mem f⟩
 #align function.injective.mem_set_image Function.Injective.mem_set_image
 
+lemma preimage_subset_of_surjOn {t : Set β} (hf : Injective f) (h : SurjOn f s t) :
+    f ⁻¹' t ⊆ s := fun _ hx ↦
+  hf.mem_set_image.1 $ h hx
+
 theorem forall_mem_image {f : α → β} {s : Set α} {p : β → Prop} :
     (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x) := by simp
 #align set.ball_image_iff Set.forall_mem_image