Are there known examples of theorems of $\sf PA$ that were first proved in systems vastly more powerful than $\sf PA$, like $\sf ZFC$ for example, and then afterwards the proof of them in $\sf PA$ was discovered (I mean historically speaking)? and if there are such examples, were the prior proofs of them in the stronger systems of value in guiding the argument of proving them in $\sf PA$? like via proving a lot of the intermediate steps required for that proof in $\sf PA$.
I'm under the impression that stronger systems can shorten proofs, so a proof of a theorem in $\sf PA$ might take too many characters, while the proof of the same theorem in the language of $\sf ZFC$ (properly relativised) for example might be much shorter, and so easier to discover.
This is a question about the utility of stronger theories in conservatively extending weaker theories and so assisting theoretic provability in the weaker ones.