Axiom of choice - to use or not to use I was wondering if there are examples of results in mathematics that were first proven using axiom of choice and later someone found a proof of the result without using the axiom of choice.
 A: If $G$ is a locally compact abelian group, then there exists a unique measure $\mu$ on the Borel sets of $G$ such that:


*

*$\mu(G)=1$,

*For every measurable $A$ and $x\in G$: $\mu(A)=\mu(A+x)$,


We can slightly enlarge the Borel sets to include all the subsets of measure zero sets, and thus have a complete measure.
This measure is called Haar measure. In the case of $\mathbb R$ this is exactly the Lebesgue measure.
Haar (the mathematician) proved its existence on separable compact groups in 1933, and von Neumann proved the uniqueness shortly after. 
The general case for locally compact Abelian groups was proved by Weil and relied on the axiom of choice. Henri Cartan later proved both existence and uniqueness of the general case without the axiom of choice.
A: Cantor-Schroder-Bernstein theorem was first proved by Cantor using the axiom of choice.  Proofs without using it came later. 
A: Things come full circle:  Constructive proofs of the Hilbert Basis theorem.
Click with all of your justice.
A: The issue is complicated by the fact that many (most?) "mainstream mathematicians" are not really keeping track of whether they are using some form of AC in their arguments.  Moreover, they often do not write their proofs in such a way which makes clear either whether they are using AC or whether this use of AC is really necessary.
Here is an example from my own experience.
Theorem (Luther Claborn): For every abelian group $A$, there exists a Dedekind domain $R$ such that the ideal class group of $R$ is isomorphic to $A$.
I know of three proofs of this theorem.

*

*Claborn's original 1966 proof:

http://alpha.math.uga.edu/~pete/claborn66.pdf


*C. Leedham-Green's 1972 proof:

http://alpha.math.uga.edu/~pete/leedhamgreen.pdf


*My 2008 proof:

http://alpha.math.uga.edu/~pete/ellipticded.pdf
Of these, the only one I am truly familiar with is my own.  My proof uses transfinite induction.  To be quite honest, I was pretty tickled by this: it was maybe the fourth time in my life that I had written down a transfinite induction argument and the first time that it was for any serious purpose.
Anyway, I soon heard from the eminent mathematician Bjorn Poonen (then at Berkeley) that he had been thinking about this very result because a student of Eisenbud's had recently given a seminar talk on Leedham-Green's proof (which I would describe as "clever and complicated").  The proof I had given was much more up his own alley, and he immediately found a way to recast / improve it.  Among other things, his recasting completely avoided use of the Axiom of Choice.  (But I hasten to add that there was more to it than that.)
We speculated briefly on the possibility that this modified argument was the first proof of Claborn's theorem to avoid AC.  I asked whether Leedham-Green's proof used AC and he told me that indeed it was also a transfinite induction argument.  So then I looked back at Claborn's paper and asked my student about it.  We were able to point to some part of Claborn's argument (which, if you look at the paper, you'll see is rather terse: I wish the paper were more than four pages long!) which we thought used AC.  But I don't remember what that was, and I am only moderately confident that we were right: if you told me otherwise, I wouldn't be too surprised.
And now I must tell you that I didn't include in my paper any hint that Poonen's modification would give an AC-less proof (and possibly the first such proof!)
of Claborn's theorem.  I felt that Poonen's argument was so nice that it deserved further exploration in its own right: I wanted to use it -- and still do -- to give a characterization of all abelian groups which can be the group of rational points on some elliptic curve over some field.  So in essence I have been keeping to myself the fact that this theorem of Claborn (which lots of people know about) can be proved independently of AC.  Sorry!
A: This  article is an example of sorts where Doyle and Conway prove without using AC that for any two sets $A,B$ such that there is a bijection between the sets $3\times A$ and $3\times B$, where $3=\{0,1,2\}$, there is a bijection between $A$ and $B$. http://www.math.dartmouth.edu/~doyle/docs/three/three.pdf
This should be relatively easy to prove using well ordering principle which is equivalent to axiom of choice.
