[Merged by Bors] - feat(Data/Finset/Image): add lemmas linking Finset.image with MapsTo/SurjOn/InjOn

Mathlib/Data/Finset/Image.lean

@@ -369,6 +369,22 @@ theorem image_subset_iff : s.image f ⊆ t ↔ ∀ x ∈ s, f x ∈ t :=
     s.image f ⊆ t ↔ f '' ↑s ⊆ ↑t := by norm_cast
     _ ↔ _ := Set.image_subset_iff
 
+lemma mapsTo_iff_image_subset : Set.MapsTo f s t ↔ s.image f ⊆ t := by
+  simp [Set.MapsTo, image_subset_iff]
+
+alias ⟨_root_.Set.MapsTo.finsetImage_subset, _⟩ := mapsTo_iff_image_subset
+
+lemma surjOn_iff_subset_image : Set.SurjOn f s t ↔ t ⊆ s.image f := by
+  simp only [Set.SurjOn]
+  norm_cast
+
+alias ⟨_root_.Set.SurjOn.subset_finsetImage, _⟩ := surjOn_iff_subset_image
+
+lemma image_eq_iff_surjOn_mapsTo : s.image f = t ↔ Set.SurjOn f s t ∧ Set.MapsTo f s t := by
+  grind [mapsTo_iff_image_subset, surjOn_iff_subset_image]
+
+alias ⟨_root_.Set.SurjOn.finsetImage_eq_of_mapsTo, _⟩ := image_eq_iff_surjOn_mapsTo
+
 theorem image_mono (f : α → β) : Monotone (Finset.image f) := fun _ _ => image_subset_image
 
 lemma image_injective (hf : Injective f) : Injective (image f) := by
@@ -504,6 +520,12 @@ theorem map_erase [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) :
   simp_rw [map_eq_image]
   exact s.image_erase f.2 a
 
+theorem iterate_image [DecidableEq α] (f : α → α) (n : ℕ) :
+    (Finset.image f)^[n] s = s.image f^[n] := by
+  induction n with
+  | zero => simp
+  | succ n ih => rw [iterate_succ_apply', iterate_succ', ih, image_image]
+
 end Image
 
 /-! ### filterMap -/