feat: s ⊆ f '' t → f ⁻¹' s ⊆ t (#17788)

Mathlib/Data/Finset/Preimage.lean

@@ -95,6 +95,10 @@ theorem image_preimage_of_bij [DecidableEq β] (f : α → β) (s : Finset β)
     (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) : image f (preimage s f hf.injOn) = s :=
   Finset.coe_inj.1 <| by simpa using hf.image_eq
 
+lemma preimage_subset_of_subset_image [DecidableEq β] {f : α → β} {s : Finset β} {t : Finset α}
+    (hs : s ⊆ t.image f) {hf} : s.preimage f hf ⊆ t := by
+  rw [← coe_subset, coe_preimage]; exact Set.preimage_subset (mod_cast hs) hf
+
 theorem preimage_subset {f : α ↪ β} {s : Finset β} {t : Finset α} (hs : s ⊆ t.map f) :
     s.preimage f f.injective.injOn ⊆ t := fun _ h => (mem_map' f).1 (hs (mem_preimage.1 h))
 

Mathlib/Data/Set/Image.lean

@@ -168,6 +168,12 @@ theorem preimage_subtype_coe_eq_compl {s u v : Set α} (hsuv : s ⊆ u ∪ v)
   · intro hx
     exact Or.elim (hsuv x_in_s) id fun hx' => hx.elim hx'
 
+lemma preimage_subset {s t} (hs : s ⊆ f '' t) (hf : Set.InjOn f (f ⁻¹' s)) : f ⁻¹' s ⊆ t := by
+  rintro a ha
+  obtain ⟨b, hb, hba⟩ := hs ha
+  rwa [hf ha _ hba.symm]
+  simpa [hba]
+
 end Preimage
 
 /-! ### Image of a set under a function -/