Extremely messy proofs Currently in my undergraduate courses I am being taught how to set up various machinery using slick, short proofs and then how to apply that machinery.  What I am not being taught, largely, is what came before these slick, short proofs.  What did mathematicians do before so-and-so proved such-and-such lemma?  Where, in other words, are the tedious, long proofs that we can look to as examples of the horrible mess we are escaping?  What insights helped mathematicians escape those messes?  
Right now I am particularly interested in examples from measure theory.  What did people do before, for example, Dynkin's lemma or Caratheodory's extension theorem?  Or were these tools available from near the start?
An answer should include both some indication of how tedious and long the old approach was and how much slicker and shorter the modern approach is.  Ideally, it should also discuss how the transition between the two happened.
(If you prefer the old approach to the modern approach, for example for pedagogical reasons, that would also be interesting to hear about.)
 A: How about Gauss' Lemma? Gauss proved it in Disquisitiones Arithmeticae, the same work in which he developed modular arithmetic, but didn't use modular arithmetic to prove it. I once wrote a blog post about this, including his original proof and a modern one for comparison.  (The blog post was intended for an audience of teachers so attempts to assume no abstract algebra background.)
A: Hironaka's proof of resolution of singularities in characteristic 0 might count. His original proof was very complicated (over 200 pages), but today there exist proofs that are reasonably short and easy. See for example Kollár's Lectures on Resolution of Singularities or Hironaka desingularisation theorem -- new proofs in literature?
A: My favorite example is Élie Cartan's original classification of the simple Lie algebras over the real numbers, the so-called real forms.  The calculations and case analyses that he does in the five exceptional cases are complicated and ad hoc (though there are certainly themes that one can pick out to guide one's understanding of the over-all structure).  Still, the conceptual improvements that have been made in the intervening years (for example, see Helgason's account in his book Differential geometry, Lie groups, and symmetric spaces) have brought the proof within the reach of non-specialists.
A: An example from measure theory that might qualify is in the construction
of non-measurable sets. The first example is well known, Vitali's 1905
construction obtained by choosing a member from each coset modulo the
additive group of rationals. Less well known is the construction given by
van Vleck, in the 1908 Transactions of the AMS. pp. 237--244.(Here
if you have JSTOR.)
Van Vleck's construction is somewhat messy, but it becomes clearer when
one realizes that it is essentially based on an ultrafilter on $\omega$,
an idea that was made explicit in the construction of Sierpinski 1938 (eudml).
A: Not from measure theory, alas, but the example that jumps to my mind is Gauss's first proof of Quadratic Reciprocity. It appears in the Disquisitiones Mathematicae. The proof occupies arts. 135 through 144 (five and a half pages in the English edition published by Springer); the proof is by strong induction on $q$ (when $p\lt q$). I don't recall who, but someone once called it a proof by "mathematical revulsion."
The proof is quite messy. Gauss argues by cases, considering the congruence classes of $p$ and $q$ modulo $4$, and whether $p$ is or is not a quadratic residue modulo $q$. He actually casts his proof as if it were a proof by minimal counterexample, so he further assumes in some instances that the result does not hold (e.g., for $p\equiv q\equiv 1 \pmod{4}$, either $p$ is a quadratic residue modulo $q$ and $q$ is not one modulo $p$; or $p$ is not a quadratic residue modulo $q$ and $q$ is a quadratic residue modulo $p$). They fall into eight cases, though some of those cases themselves break into subcases. For example, Gauss looks at the case when $p$ and $q$ are both congruent to $1$ modulo $4$, and $\pm p$ is not a residue modulo $q$; then he takes a prime $\ell\neq p$ less than $q$ for which $q$ is not a quadratic residue, and considers the cases in which $\ell\equiv 1 \pmod{4}$ or $\ell\equiv 3 \pmod{4}$ separately; the first subcase itself breaks into four separate sub-subcases: since $p\ell$ is a quadratic residue modulo $q$, it is the square of some even $e$; then he considers the case when $e$ is not divisible by either $p$ or $\ell$, when it is divisible by $p$ but not $\ell$; when it is divisible by $\ell$ but not $p$; and when it is divisible by $\ell$ and $p$. And so on. By the time Gauss finally gets to the eighth and final case, he is clearly somewhat exhausted, writing merely "The demonstration is the same as in the preceding case."
On the one hand, the proof is pretty much the first proof that one might think to try when encountering the problem. But the different cases are just way too messy, and one quickly loses sight of the forest because one is so intently staring at the beetles in the bark of the tree directly in front. 
Plenty of other proofs would follow (including five more by Gauss), ranging from the clever to the almost magical (do this, do that, and oops, quadratic reciprocity falls out). 
A: Hilbert's original proof of the Hilbert Basis Theorem is 62 pages long and messy by any standard.  Emmy Noether's proof, using the ascending chain condition, is easily presented in a paragraph.
A: The Sylvester problem:  see https://en.wikipedia.org/wiki/Sylvester%E2%80%93Gallai_theorem
A finite set of plane points has the property that any line through two of them passes through a third point from the  set.  Then the points are collinear.
This claim was posed as a problem by J. J. Sylvester (1893). The first proof  by T. Gallai in 1933 is quite complicated.  L. M. Kelly gave a simple proof  in 1948.  See
https://www.cecm.sfu.ca/~pborwein/PAPERS/P48.pdf for more details and references to other proofs.
A: The structure of (complete) discretely valued fields. Today this is usually done with Teichmüller representatives and Witt vector machinery (e.g. Serre, Local Fields, ch. II §§4-6). But the main results had been proved with more complicated methods by H. Hasse and F. K. Schmidt (Crelle 170 (1934): 60 pages) before these tools were developed. Also, what is today called Artin-Schreier-Witt theory was developed by H. L. Schmid with very messy computations: These inspired Witt to invent his vectors, which then gave it a much more conceptual background. Cf. the "history" part of my answer here.
A: One nice example (from topology) is Tychonoff's Theorem (that a product of compact spaces is compact). No matter how many times I see it, I find the classic proof based on the (Alexandre Subbase Lemma) difficult and opaque. On the other hand if one first develops the theory of nets (aka Moore-Smith Convergence), not only is that a powerful tool for all sorts of other purposes, but its development is a natural and intuitive generalization of sequences, and the place where Zorn's Lemma enters (the proof that any net has a universal subnet) is much clearer than in the proof of the subbase lemma. And of course once one has universal nets, the proof of Tychonoff is the obvious generalization of the trivial proof that a finite product of sequentially compact spaces is sequentially compact.
A: Gray has a very nice paper on the evolution of the Riemann-Roch theorem (which started very messy indeed).
A: Arhangel'skii's positive solution to Alexandroff's problem (does every compact Hausdorff space with a countable local base at every point have cardinality at most the continuum?) was quite clever and complicated. Later proofs of Arhangel'skii Theorem by Pol and Shapirovskii are not only simpler, but they also provide a common framework for many cardinal inequalities which before had to be proved in ad hoc ways (ramification arguments, infinitary combinatorics...) The model-theoretic version of the Pol-Shapirovskii method makes that framework even more transparent and user-friendly.
I will mention another more recent example from Set-theoretic topology to remember a great mathematician who passed away just a few days ago. Mary Ellen Rudin's proof of Nikiel's Conjecture is almost 30 pages long! Rudin's theorem states that every compact monotonically normal space is the continuous image of a compact linearly ordered space. (Monotonically normal is an elegant common generalization of linearly ordered and metric spaces). I recall from his talk at one of the Spring Topology Conferences that Todd Eisworth had a project of using elementary submodels to clarify her proof and has already succeeded to do that for the separable case. But I don't know if his proof has already been published (he has a related paper on his website, but it does not contain that proof: Eisworth, Todd, Elementary submodels and separable monotonically normal compacta, Topol. Proc. 30, No. 2, 431-443 (2006). ZBL1145.54021, MR2352742. http://www.ohio.edu/people/eisworth/research/Preprints%20and%20Reprints/finalMN.pdf, Wayback Machine).
A: I nominate the homology version of Cauchy's theorem: a sufficient condition for a curve in a (multiply) connected region has $0$ contour integral for any function which is analytic in that region is that the winding number of the curve with respect to any point outside the region is $0$.
E. Artin's proof is pretty messy: he used grids to approximate the contour, and then we have to verify that the integrals around the grid is equal to the integral around the contour, as well as that they have the same topology.
J. Dixon's proof is very elementary (a little less intuitive than the approximation proof, though, only a little) and straight forward. The key step is no more than interchanging the integration order.
Serge Lang's book has both versions, in case anyone concerns.
A: The traditional way of proving Grothendieck duality is to first show it for proper maps and for open immersions, which already is quite a labour. Then one uses that any morphism of Noetherian schemes factors into such and pastes the partial results together. This requires an awful lot of non-trivial checking that certain diagrams are commutative. The extension of the result to Non-Noetherian schemes then requires yet more work.
In contrast, Neeman's proof of Grothendieck duality via Brown representability is slick, short (30 pages) and conceptual and a pure pleasure to read.
(but: the first approach gives you more insight into what the functors from Grothendieck duality actually do, so it is by no means worthless)
A: Another example is Birkhoff's ergodic theorem.
The modern proof uses Hopf's maximal ergodic lemma, which makes it much shorter than the classical proof is. See, for example, these notes (the proof given here is quite detailed, but not as complex as in the classical approach. I have seen shorter proofs of the exact same statement though, also using Hopf's lemma). It is possible to prove it even more briefly, for instance in this text, where Keane and Petersen prove a strengthened maximal ergodic lemma.
The original theorem stated by Birkhoff in 1931 can be found here, for example. So you can see 'what mathematicians did before E. Hopf proved the maximal ergodic lemma'. I wouldn't call this extremely messy, but it's definitely more complicated.
I cannot give any background as to how Hopf came to proving his lemma, but it must have appeared in his book about ergodic theory, published in 1937. So I conjecture it was inspired directly by Birkhoff's work. (I'd be happy to see comments or corrections concerning this)
A: Given a homogeneous polynomial ideal, we can ask how many linearly independent homogeneous polynomials of each degree there are, and thereby obtain a sequence of integers.  In a 1927 paper, Macaulay analyzed which sequences of integers could arise in this way.  Macaulay himself wrote:

This proof of the theorem which has been assumed earlier is given only to place it on record. It is too long and complicated to provide any but the most tedious reading.

The proof was later shortened by Sperner (Über einen kombinatorischen Satz yon Macaulay und seine Anwendung auf die Theorie der Polynomideale, Abh. Math. Sere. Univ. Hamburg 7 (1930), 149–163; see also G. F. Clements and B. Lindström, A generalization of a combinatorial theorem of Macaulay, J. Combin. Theory 7 (1969), 230–238.).  However, I confess that I have not studied either proof so I cannot answer your question about what new insights enabled the shortening.
A: In 1917, Schur showed that there was no hope of proving Fermat's Last Theorem by ruling out the corresponding congruences. He applied a result from Ramsey Theory, but of course Ramsey Theory had not yet been invented in 1916, so he had to prove that result first. Nowadays we use finite Fourier series to prove Schur's theorem on congruences, and we not only get a simpler proof, but a sharper result.
A: Sometimes an alternative to proofs being messy because they were written before advanced methods were available is proofs being numerous because they were written before advanced methods were available.  An example is the proofs by Archimedes in his Mechanical Method.  They are stunningly beautiful, but you need a new brilliant trick for each elementary integral.
A: You may want to look into the history of the de Branges proof of the Bieberbach conjecture. Reader's Digest version: his original proof was over 100 pages, but others studying his proof got it down to about a dozen. 
A: This is not about measure theory or Dynkin's lemma or Caratheodory's extension theorem, but it is hard for me to resist sharing one of my favorite examples of improving proofs with modern machinery: the Intermediate Value Theorem. This theorem is so intuitively obvious, but the proof using classical analysis involves taking a supremum of the set of $a \leq x \leq b$ such that $f(x) \leq y$ (where $y$ is the desired output) and then showing using continuity that this supremum $c$ satisfies $f(c) = y$. There are lots of $\delta$'s and $\epsilon$'s and the proof feels uninspiring and technical at best.
Enter topology. The proof that the image of a connected set is connected for a continuous function is simple and intuitive, as is the notion of a connected set. Once this is established, the Intermediate Value Theorem is essentially just the statement that an interval is a connected set, so the image must be connected. This proof captures, in my opinion, the intuition of the Intermediate Value Theorem in a precise way.
A: Another example is Euler's original approach to the Königsberg bridge problem. Although not terribly messy, it seems unnecessarily complicated to anyone familiar with the modern approach. See for example, The truth about Königsberg, by Brian Hopkins and Robin J. Wilson and Early writings on graph theory: Euler circuits and The Königsberg bridge problem (Wayback Machine) by
Janet Heine Barnett.
A: An example from algebra is Albert's paper "On the Wedderburn norm condition for cyclic algebras" relating a 6-dimensional quadratic form to every biquaternion algebra (which is now known as the "Albert quadratic form"). His original paper is essentially one long (but of course extremely clever) computation. By now, we have much more conceptual proofs and we understand the situation much better (see for instance the Book of Involutions). I'm sure that there are many more examples of this style.
A: Invariant theory before Hilbert was quite messy and ad hoc, e.g. classical pre-Hilbert proofs of finite generation of various rings of invariants are quite unpleasant and long.
A: Nash's original proof of his famous isometric embedding theorem was extremely complicated. I'm under the impression that very few people ever read or understood the details. The hard step is a generalized implicit function theorem. His proof was simplified considerably by Moser and others (I learned the proof from a paper by Sergeraert). However, the proof of the isometric embedding theorem was dramatically simplified by Matthias Gunther, who found a way to use the standard contraction mapping argument and eliminate completely the need for the so-called Nash-Moser implicit function theorem.
However, Gunther's proof, unlike the other examples and the intent of the question, is for me just as mysterious and miraculous as Nash's original proof.
A: What about Wiener's proof that the reciprocal of a nowhere zero function on the circle with absolutely convergent Fourier series also has this property? Gelfand basically created the theory of Banach algebras in order to give a short, clean proof.
I think Halmos said something to the effect that Wiener didn't really understand his own theorem, because he didn't find Gelfand's proof.
A: Hindman's theorem states that if we finitely colour the naturals, there exists an infinite set $S$ such that the sum of every finite non-empty subset of $S$ has the same colour.
Hindman's original combinatorial proof of his theorem was very long and protracted. Baumgartner found a shorter combinatorial proof, which was still rather long, before Galvin and Glazer blew it out of the water with a beautiful proof involving defining a topology on the space $\beta \mathbb{N}$ of ultrafilters and proving various things about it.
The Galvin-Glazer idea of idempotent ultrafilters has been applied to many other problems, only some of which are related to Ramsey theory.
Interestingly, the longer proofs actually operate in weaker systems of mathematics: the original proof works in ACA_0, the second proof in a stronger second-order arithmetic, and the third proof requires full ZFC (without choice, one cannot prove the existence of any non-trivial ultrafilters, never mind an idempotent one). See https://arxiv.org/pdf/0906.3885.pdf for more details.
A: This isn't a proof, but I always liked Brownian motion as an example of a continuous, nowhere differentiable function.  As opposed to putting a lot of effort into artificially creating a series which converges and proving that it is continuous and nowhere differentiable, you take a natural, physical process and say "Ah ha!  It works."  The proof that it's nowhere differentiable is a pretty straightforward, though constructing a Brownian motion can be a pain...
A: The Quadratic Equation formula:   Al-Khawarizmi (c 800 AD) did not have negative numbers, nor zeros, and also did not possess the needed algebraic notation. Therefore he had to devote 6 chapters of his treatise on algebra ("Hisab al-jabr w'al-muqabala") to different types of quadratics, and the rules for solving each one of them.
See "Quadratic, cubic and quartic equations", MacTutor History of Mathematics archive.
A: Nowadays, no one looks at Lambert's proof of the irrationality of $\pi$. Mostly you will see (variations of) the far nicer proof by Niven. 
A: Poincare Duality
The original formulation was not only messy, but wrong. The modern formulation is more powerful, more elegant, and don't forget correct.
You can read about both approaches and some of the history on the wiki page.
A: The proof of the John-Nirenberg inequality is rather horrible (or maybe that's only the way it felt when I was an undergrad?)
A: Picard's own proof of his theorem, I remember, should have been long, and modern easy proofs have been produced.
A: I'm surprised that nobody's mentioned the classification of the simple finite groups. Apparently the full proof runs over ten thousand journal pages. The proof is bound to be messy!
