In Awfully sophisticated proof for simple facts, we are asked for examples of complex proofs of simple results. To quote from the questioner's post, we are asked for proofs that are akin to "nuking mosquitos." In set theory, a natural "nuke" with respect to a certain result is a large cardinal axiom with unnecessarily high consistency strength (i.e. applying to a much stronger collection of axioms than is required to provide a proof of the possibility of the result in question).
A research focus in set theory is a search for large cardinal axioms with the weakest consistency strength that can be used to prove the possibility of a certain result. My question is of an opposing nature:
Can you think of results that can be proven in a different manner by appealing to a large cardinal axiom with unnecessarily large consistency strength?
There are plenty such examples where the proofs become less technical (e.g., using a $\kappa^{++}$-supercompact cardinal $\kappa$ to show that the GCH can fail at a measurable cardinal is much more than is required), but I'm thinking of examples where the original proof was accomplished without such a strong large cardinal hypothesis or any large cardinal hypothesis at all. For example (from my post to the aforementioned question):
Theorem (ZFC + "There exists a supercompact cardinal."): There is no largest cardinal.
Proof: Let $\kappa$ be a supercompact cardinal, and suppose that there were a largest cardinal $\lambda$. Since $\kappa$ is a cardinal, $\lambda \geq \kappa$. By the $\lambda$-supercompactness of $\kappa$, let $j: V \rightarrow M$ be an elementary embedding into an inner model $M$ with critical point $\kappa$ such that $M^{\lambda} \subseteq M$ and $j(\kappa) > \lambda$. By elementarity, $M$ thinks that $j(\lambda) \geq j(\kappa) > \lambda$ is a cardinal. Then since $\lambda$ is the largest cardinal, $j(\lambda)$ must have size $\lambda$ in $V$. But then since $M$ is closed under $\lambda$ sequences, it also thinks that $j(\lambda)$ has size $\lambda$. This contradicts the fact that $M$ thinks that $j(\lambda)$, which is strictly greater than $\lambda$, is a cardinal.
For the people who are unfamiliar with large cardinal embeddings, let me mention that the critical point of an embedding $j$ is the first ordinal $\kappa$ that is moved (i.e., $j(\alpha) = \alpha$ for all $\alpha$ less than the critical point $\kappa$ and $j(\kappa) > \kappa$.) A cardinal $\kappa$ is $\theta$-supercompact if there exists an elementary embedding $j: V \rightarrow M$ into a transitive (proper class) $M$ with critical point $\kappa$ such that $M^{\theta} \subseteq M$ and $j(\kappa) > \theta$. A cardinal is supercompact if it is $\theta$-supercompact for all $\theta$.
Best Answer
This may not be the sort of thing you had in mind, but here goes anyway: The easiest way to prove Borel determinacy (which is a theorem of ZFC) is to assume there's a measurable cardinal and prove analytic determinacy. (Both results are due to Tony Martin. The proof of analytic determinacy from a measurable cardinal came well before the proof of Borel determinacy in ZFC. The exact consistency strength of analytic determinacy is the existence of sharps of all reals.)