feat(data/set/basic): Added range_eq_iff (#11044)

This serves as a convenient theorem for proving statements of the form `range f = S`.

Author: vihdzp

src/data/set/basic.lean

@@ -1735,6 +1735,10 @@ subset.antisymm
 theorem range_subset_iff : range f ⊆ s ↔ ∀ y, f y ∈ s :=
 forall_range_iff
 
+theorem range_eq_iff (f : α → β) (s : set β) :
+  range f = s ↔ (∀ a, f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b :=
+by { rw ←range_subset_iff, exact le_antisymm_iff }
+
 lemma range_comp_subset_range (f : α → β) (g : β → γ) : range (g ∘ f) ⊆ range g :=
 by rw range_comp; apply image_subset_range