I’m interested in examples of theorems of the form “If $P$ then $Q$“ that were either unsolved or thought to require difficult arguments until someone came up with an $X$ for which “If $P$ then $X$” and “If $X$ then $Q$” are significantly easier to prove.

22$\begingroup$ Is it important that there be only a single step $X$? Otherwise this seems like essentially a description of every mathematical proof. $\endgroup$ – LSpice Apr 6 at 14:12

1$\begingroup$ I agree that every time someone constructs a proof, they’re doing something like this. But I’m looking for a dramatic example, grounded in the history of mathematics; for a period of time the experts in the relevant topic knew only complicated proofs of “$P$ implies $Q$”, but once someone suggested $X$ as an intervening step, it became clear that this gave a much simpler proof. $\endgroup$ – James Propp Apr 6 at 14:41

1$\begingroup$ I’m guessing that there are theorems of the form “Every bandersnatch is slithy” that were unproved (or only had a very complicated proof) until someone came up with the concept of frumiousness and showed in a straightforward manner that every bandersnatch is frumious and that frumiousness implies slithiness. $\endgroup$ – James Propp Apr 6 at 14:51

5$\begingroup$ maybe the proof of Fermat's last theorem? Modularity for semistable elliptic curves is much more structured setting than these wild diophantine equations. Indeed, most of them, including some looking similar to Fermat's, will not be resolved for a long time, most probably. $\endgroup$ – user137767 Apr 6 at 15:56

1$\begingroup$ @TeoBanica That's not necessarily true. If you are looking for a path in a graph (for example, the space of provable statements), if an oracle gives you a good intermediate point, that actually makes things easier. In fact, if they give you all the intermediate points, they have basically given you the path/proof. $\endgroup$ – verret Apr 7 at 19:35
This is an example of the special case: an inclusion $P \subseteq Q$ which seems difficult or impossible to prove, until someone comes up with an $X$, with the property that $P \subseteq X$ and $X \subseteq Q$ are relatively easy to prove.
Let $Z$ be a finite set of points in projective space $\mathbb{P}^n$, let $I$ be the homogenous ideal of $Z$, and let $m$ be a positive integer. Let $P$ be the ideal of homogeneous forms that vanish to order $mn$ at each point of $Z$. This is the $mn$’th symbolic power of $I$, denoted $I^{(mn)}$. And let $Q$ be the $m$’th ordinary power, $I^m$. Then $P \subseteq Q$, or $I^{(mn)} \subseteq I^m$.
This is not obvious. Say $F$ vanishes to order $4$ at each point of $Z$. Then $F$ can be written as a sum of products $G_i H_i$, where each $G_i,H_i$ vanishes at each point of $Z$. Why? It’s not easy to see, and this is just the $m=2$ case.
This was proved by EinLazarsfeldSmith [1] using $X=$ an asymptotic multiplier ideal, which was introduced in this paper (they introduce asymptotic multiplier ideals and give several applications, one of which is the theorem $P \subseteq Q$), and simultaneously proved by HochsterHuneke [2] using $X=$ a tight closure ideal. The theorems are more general than I’ve stated, e.g., for ELS, $Z$ can be a reduced scheme on a smooth variety; HH work in an arbitrary reduced Noetherian ring. Yet, I don’t believe there is, to this day, any “elementary” proof known, even in the case of points in the projective plane $\mathbb{P}^2$, in characteristic zero. BocciHarbourne proved it by “elementary” means when $Z$ is a general set of points in $\mathbb{P}^2$, but not for arbitrary $Z$.
I might be wrong. Since ELS and HH in around 2001 there has been a ton of work on this topic, under the heading of “containment problems” or more specifically, the problem of containments of symbolic powers. Lots of generalizations, strengthenings, special cases, etc. But if anyone found a proof of the original, basic result $P \subseteq Q$, without going through some “nonelementary” $X$ like an asymptotic multiplier ideal or test ideal (only using “classical” plane geometry), I missed the news.
Three examples come to mind, all with $P=ZF$ or some other base theory.
1) Fermat / HeathBrown / Zagier:
 $Q$ = "every prime of the form $4n+1$ is the sum of two squares";
 $X$ = "the map $$(x,y,z)\mapsto \begin{cases} (x+2z,~z,~yxz),\quad \textrm{if}\,\,\, x < yz \\ (2yx,~y,~xy+z),\quad \textrm{if}\,\,\, yz < x < 2y\\ (x2y,~xy+z,~y),\quad \textrm{if}\,\,\, x > 2y \end{cases} $$ is an involution with an odd number of fixed points on the set $\{(x,y,z)\in\mathbb{N}^3:x^2+4yz=p\}$.
2) Hadamard / de la Vallee Poussin / Newman / Zagier:
 $Q$ = the prime number theorem;
 $X_1,\ldots,X_7$ = Zagier's statements $IVI$ and the Analytic Theorem.
 $Q$ = the Lebesguemeasurable sets are closed under countable unions;
 $X$ = the Caratheodorymeasurable sets are closed under countable unions.
I think giving the statements $X$ and asking for proofs could be a reasonable homework or group project for a graduate class in Number Theory, Complex Analysis, or Real Analysis, which is saying something given the significance of the $Q$.

1$\begingroup$ The famous "A proof that Euler missed" paper recounting Apery's result also breaks down the argument into steps which could be considered exercises for students. $\endgroup$ – Sam Hopkins Apr 14 at 20:32

2$\begingroup$ Interestingly, the second line of the Zagier article you link to is "[Hadamard and de la Vallee Poussin's] proof had two elements: showing that Riemann's zeta function $\zeta(s)$ has no zeros with $\Re(s) = 1$, and deducing the prime number theorem from this. " Although neither step could be considered easy, I feel that this itself is an example of what the OP is asking for since the Riemann Zeta function is a bit of a deus ex machina here (nothing in the original formulation of the PNT is helpful even in realizing that $\zeta$ would exist) without which everything is even more complicated $\endgroup$ – Vincent Apr 15 at 7:51