Stable group acting on a type definable set. We work inside a saturated $M \models T$ with $T$ $\omega$-stable. We may even assume $T = \mathsf{ACF}$.
Let $G$ be a connected definable group together with a transitive definable action of $G$ over a type definable set $Y$. Then $Y$ is definable.
I am thinking of proving it by using $Y = G \cdot y$ for any $y \in Y$, and somehow using compactness and definability of $(G, \cdot)$, but I need to find some $y \in Y$ such that $\{ y \}$ is definable (I believe). Something else I wanted to use is the descending chain condition for stable groups, and writing $Y = \bigcap_i  \phi_i(M)$ for some set of formulas, and then somehow go back to $G$ to prove $Y = \phi_{i_1}(M) \cap \dots \cap \phi_{i_n}(M)$, using transitivity in the process. I am however, unable to put these together or see intuitively why $Y$ should be definable.
Any help is appreciated.
 A: Your idea to define $Y$ as $G\cdot b$ for some $b\in Y$ is a good one. In general, there's no reason why there should be a definable element of $Y$. But why use one element of $Y$ when you can use them all? By which I mean: instead of using an arbitrary parameter, use the "canonical parameter" in $M^{\text{eq}}$.
Proof 1: Let $\varphi(x,y)$ be the formula expressing $x\in G\cdot y$. Let $E$ be the equivalence relation defined by $yEy'\iff \forall x\, (\varphi(x,y)\leftrightarrow \varphi(x,y'))$. Since the action of $G$ on $Y$ is transitive, for any $b\in Y$, $Y = [b]_E$. Since $Y$ is type-definable, $Y$ is fixed by all automorphisms, so the element $[b]_E$ in $M^{\text{eq}}$ is fixed by all automorphisms. Thus, $[b]_E$ is a definable element, and hence $Y$ is a definable set.
Essentially the same argument gives the following more general (and fundamental) result: Suppose $A\subseteq B$ and $Y$ is definable over $B$ and $A$-invariant (fixed setwise by all automorphisms that fix $A$ pointwise). Then $Y$ is definable over $A$.
But this is a rather abstract proof, which hides the key compactness argument, in a way. Unwinding, we can give the following less slick but more "concrete" proof. Here I'll actually use type-definability, not just invariance, to simplify the argument.
Proof 2: Let $\Phi(y)$ be the partial type defining $Y$. Since the action of $G$ on $Y$ is transitive, the following partial type is inconsistent: $\Phi(y)\cup \Phi(y')\cup \{\lnot (\exists x\in G\, x\cdot y = y')\}$. By compactness, there is some formula $\varphi(y)$ which is a finite conjunction of formulas in $\Phi(y)$, such that $\varphi(y)\land \varphi(y')\land \lnot (\exists x\in G\, x\cdot y = y')$ is inconsistent. Let $Y'$ be the set defined by $\varphi(y)$. The $Y\subseteq Y'$, and the action of $G$ on $Y'$ is transitive, so $Y = Y'$.
