The first example that occurs to me is Hindman's theorem: If the set of positive integers is partitioned into finitely many pieces, then there is an infinite set $H$ such that all sums of finitely many (distinct) elements of $H$ lie in the same piece. Hindman's original proof is very complicated (Hindman himself has suggested that it could be used to torture graduate students) but it has the advantage of being elementary --- it can be formalized in a system only slightly stronger than $ACA_0$. A later, easier proof by Galvin and Glazer, now considered the standard proof, has the advantage that one can easily remember or reconstruct it, but it requires more powerful tools, including an application of Zorn's lemma to a collection of subsemigroups of a certain semigroup whose elements are ultrafilters. There's also an "intermediate" proof due to Baumgartner.