One use of forcing as a tool to prove theorems that has not been mentioned in the answers is the method of generic ultrapowers, where we take an ideal $I$ on an uncountable regular cardinal $\kappa$ (in the sense of $M$), and consider the poset $P,\leq$ of those subsets of $\kappa$ that has positive measure (the ordering is by subset). A generic filter $F$ of that poset will end up being an $M$-ultrafilter in $M[G]$, which extends the filter dual to $I$. And if $I$ is {$\kappa$-complete, normal} in $M$, $G$ will be {$\kappa$-complete, normal}.

If $I$ indeed has the requisite properties, then in $M[G]$ we can form the ultrapower of $M$ by $G$, and an elementary embedding $j:V\to Ult(M,G)$. This way, we allow ourselves the liberty of "pretending" to have an elementary embedding $j:V\to M$ without being necessarily committed to the existence of large cardinals.

The generic ultrapower is not necessarily well-founded (an ideal is *precipitous* (which, incidentally, means příkrý in Czech) iff the generic ultrapower obtained is well-founded). But having such a construction at hand can be useful. Example 22.15 in Jech illustrates one such use.

**Theorem**. Let $\kappa$ be a singular cardinal of uncountable cofinality, and assume GCH holds below $\kappa$, then $2^\kappa=\kappa^+$.

The proof is to use the nonstationary ideal on $(cf(\kappa))^M$, then in the extension we obtain a normal $M$-measure on $(cf(\kappa))^M$, which we use to construct the ultrapower. One key observation is that the poset of positive measure subsets will have size $2^{cf(\kappa)}<\kappa$, so its cc property implies that cardinals above $\kappa$ are preserved. By studying the combinatorial properties of objects in $Ult$, we may infer that $(|\mathcal{P}^M(\kappa)|)^{M[G]}\leq(\kappa^+)^{M[G]}$, which can be transferred back to $M$ because of the observation.