A famous result of Jensen is the coding theorem showing that the universe can be extended by class forcing to a model of the form $L[a]$, with $a$ a real, in a way that the original ground model can be decoded from $a$. (Jensen's result is stronger than this.)
The argument is delicate even if $0^\sharp$ does not exist (in this case, other proofs are known, also involved. One is due to Shelah and Stanley).
The published proof appeared in the book Coding the universe by Beller, Jensen, and Welch; there are reworkings and extensions, for example by Friedman, but maintaining the same outline. It presents two different arguments, depending on whether $0^\sharp$ exists (the division is needed mainly because of the covering lemma).
(To be fair, as Mohammad indicates in a comment, Sy has a proof that does not require this splitting. Also, Sy has extensions of the result, where we are interested not just in the coding but also in preserving non-trivial large cardinal structure present in the universe. His latest advance in this direction is at the level of Woodin cardinals, see Genericity and Large Cardinals, Journal of Mathematical Logic, Vol. 5, No. 2, pp. 149-166, 2005.)
This is not exactly what you are asking, but I believe it is as close as we can get: A proof that splits in cases according to whether certain large cardinal assumption holds or not, requiring a different approach in either case.