Nonessential use of large cardinals 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$.
 A: I find it hard to believe that "Every set of reals has the Baire Property" was not mentioned yet.
Solovay proved that if we collapse an inaccessible cardinals to be $\omega_1$, then in $V(\Bbb R)$ every set of reals is Lebesgue measurable and has the Baire Property and $\sf DC$ holds.
Shelah later proved that the inaccessible is necessary for the Lebesgue measurability, but it is not necessary for the Baire Property.  This proof is different and much more technical than that of Solovay (which is arguably not very difficult once you have a few theorems about forcing under your belt).
A: When dealing with the singular cardinals hypothesis ($SCH$), one may face with many such examples, let me say a few:
$\star_1:$ The consistency of the failure of $SCH$ was proved first by silver using supercompact cardinals. Later, Woodin reduced it to large cardinals up to strong cardinals, and finally Gitik showed that a measurable cardinal with $o(\kappa)=\kappa^{++}$ is suffices (which is also necessary).
$\star_2:$ Magidor first proved the consistency of $GCH$ below $\aleph_\omega$ with $2^{\aleph_\omega}=\aleph_{\omega+2}$ from a supercompact cardinal and a huge cardinal above it. Later Woodin reduced it to  the level of strong cardinals, and finally it turned out that a measurable cardinal with $o(\kappa)=\kappa^{++}$ is suffices.
$\star_3:$ Foreman and Woodin proved the consistency of the total failure of $GCH$ from a supercompact cardinal and infinitely many inaccessibles above it. Later, it turned out that a $(\kappa+3)$-strong cardinal is suffices (and even less is needed).
A: 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.)
A: I think this example given at Richard Borcherds's blog would qualify, no? 
A: There is a fantastic (and not too well-known) result of Shelah stating that $L({\mathcal P}(\lambda))$ is a model of choice whenever $\lambda$ is a singular strong limit of uncountable cofinality. 
This is a consequence of a more general theorem that can be found in 4.6/6.7 of "Set Theory without choice: not everything on cofinality is possible", Archive for Math Logic 36 (1997) 81-125. 
(Understanding this argument is in my "immediate" to-do list. Alas, the list is longer each day.)  
Woodin has a nice, short argument when the cofinality of $\lambda$ is a Woodin cardinal, using stationary tower techniques. (I do not think Woodin's argument is published anywhere, though.) It certainly gives you an idea that the result is plausible, and that an analysis of ideals seems to be relevant.
A: This may not be quite the sort of thing you were looking for, but some of Harvey Friedman's examples of $\Pi^0_1$ statements unprovable in ZFC but provable using large cardinals can be used to produce $\Pi_0^0$ statements (i.e., statements whose truth can be verified with a finite computation) that have large-cardinal proofs that require at most (say) a million symbols to write down, but which have no ZFC-proofs less than 101000 symbols long.  See this post from the Foundations of Mathematics mailing list for example.
Since $\Pi_0^0$ statements are finitely checkable, they are in principle provable using ridiculously weak axioms (assuming that they are true).  In other words, strong axioms are certainly nonessential.  However, large cardinal axioms are required if you want a proof that can actually be written down in practice.
These examples are a little peculiar because if you don't believe large cardinal axioms then you may not believe these $\Pi_0^0$ statements—and yet they could in principle be directly checked if you just had enough computational power…
