feat(logic/equiv/local_equiv): add forall_mem_target/`exists_mem_ta…

…rget` (#13805)

src/logic/equiv/local_equiv.lean

@@ -233,6 +233,12 @@ protected def to_equiv : equiv (e.source) (e.target) :=
 
 lemma image_source_eq_target : e '' e.source = e.target := e.bij_on.image_eq
 
+lemma forall_mem_target {p : β → Prop} : (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (e x) :=
+by rw [← image_source_eq_target, ball_image_iff]
+
+lemma exists_mem_target {p : β → Prop} : (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (e x) :=
+by rw [← image_source_eq_target, bex_image_iff]
+
 /-- We say that `t : set β` is an image of `s : set α` under a local equivalence if
 any of the following equivalent conditions hold:
 
@@ -249,7 +255,7 @@ variables {e} {s : set α} {t : set β} {x : α} {y : β}
 lemma apply_mem_iff (h : e.is_image s t) (hx : x ∈ e.source) : e x ∈ t ↔ x ∈ s := h hx
 
 lemma symm_apply_mem_iff (h : e.is_image s t) : ∀ ⦃y⦄, y ∈ e.target → (e.symm y ∈ s ↔ y ∈ t) :=
-by { rw [← e.image_source_eq_target, ball_image_iff], intros x hx, rw [e.left_inv hx, h hx] }
+e.forall_mem_target.mpr $ λ x hx, by rw [e.left_inv hx, h hx]
 
 protected lemma symm (h : e.is_image s t) : e.symm.is_image t s := h.symm_apply_mem_iff