Solution (source code)

= Solution

Expand the language by constants for every element of $M$ and a new tuple $c$. Let $\operatorname{ElDiag}(M)$ be the <elementary diagram of a structure> associated with $M$. Every finite subset of
$$
\operatorname{ElDiag}(M)\cup p(c)
$$
is realized in the expansion of $M$, because the finitely many formulas from $p$ are simultaneously satisfiable in $M$. The <compactness theorem> gives a model $N'$ of the whole set. The interpretations of the named constants give an <elementary embedding> $M\to N'$, and the interpretation of $c$ realizes $p$. Identifying $M$ with its image produces an elementary extension $M\preceq N$ realizing $p$. This is the <finitely satisfiable type is realized in an elementary extension> argument.