In first-order set theory (and first-order logic in general), we always have $$(\forall x. P(x)) \rightarrow \exists x. P(x)$$
However, we do not have $(\forall x \in A. P(x)) \rightarrow \exists x \in A. P(x)$ unless $A$ is non-empty. Why? Because $\forall x \in A. P(x)$ abbreviates $\forall x. x \in A \rightarrow P(x)$, while $\exists x \in A. P(x)$ does not abbreviate $\exists x. x \in A \rightarrow P(x)$, but rather $\exists x. x \in A \wedge P(x)$.
If we take $A=\emptyset$, then $\forall x. x \in \emptyset \rightarrow P(x)$ is vacuously true, but $\exists x. x\in \emptyset \wedge P(x)$ is always false, since $x \in \emptyset$ never holds. So the former does not imply the latter, unless $A \neq \emptyset$.
In dependent type theory, the underlying formal theory of Lean, there is no direct equivalent to the "unbounded" quantifiers $\forall x$ and $\exists x$ of first-order logic. Whenever one writes
∃ x, p x in Lean, it's really just an abbreviation for
∃ x : T, p x, where
T is some type determined by the type of
p. For example, if we take
is_even from the Lean tutorial, then
∃ x, is_even x abbreviates
∃ x : ℕ, is_even x.
α is a type variable, then proving
(∀ x : α, p x) → ∃ x : α, p x is not possible: if it was, we would be able to substitute any type, including the
empty type (see here) for
α. However, if you fix any inhabited (~non-empty) type, e.g. by setting
α = ℕ, then you will be able to prove
(∀ x : ℕ, p x) → ∃ x : ℕ, p x.