Unnecessary uses of the axiom of choice 
What examples are there of habitual but unnecessary uses of the axiom of
choice, in any area of mathematics except topology?

I'm interested in standard proofs that use the axiom of choice, but where
choice can be eliminated via some judicious and maybe not quite obvious
rephrasing.  I'm less interested in proofs that were originally proved
using choice and where it took some significant new idea to remove the
dependence on choice.
I exclude topology because I already know lots of topological examples. For
instance, Andrej Bauer's Five stages of accepting constructive
mathematics
gives choicey and choice-free proofs of a standard result (Theorem 1.4):
every open cover of a compact metric space has a Lebesgue number. Todd
Trimble told me about some other topological examples, e.g. a compact
subspace of a Hausdorff space is closed, or the product of two compact
spaces is compact. There are more besides.
One example per answer, please. And please sketch both the habitual proof
using choice and the alternative proof that doesn't use choice.
To show what I'm looking for, here's an example taken from that paper of Andrej Bauer. It would qualify as an answer except that it comes from
topology.
Statement Every open cover $\mathcal{U}$ of a compact metric space
$X$ has a Lebesgue number $\varepsilon$ (meaning that for all $x \in X$, the
ball $B(x, \varepsilon)$ is contained in some member of $\mathcal{U}$).
Habitual proof using choice For each $x \in X$, choose some
$\varepsilon_x > 0$ such that $B(x, 2\varepsilon_x)$ is contained in some
member of $\mathcal{U}$. Then $\{B(x, \varepsilon_x): x \in X\}$ is a
cover of $X$, so it has a finite subcover $\{B(x_1, \varepsilon_{x_1}),
  \ldots, B(x_n, \varepsilon_{x_n})\}$.  Put $\varepsilon = \min_i
  \varepsilon_{x_i}$ and check that $\varepsilon$ is a Lebesgue number.
Proof without choice Consider the set of balls $B(x, \varepsilon)$
such that $x \in X$, $\varepsilon > 0$ and $B(x, 2\varepsilon)$ is
contained in some member of $\mathcal{U}$. This set covers $X$, so it has
a finite subcover $\{B(x_1, \varepsilon_1), \ldots, B(x_n,
  \varepsilon_n)\}$. Put $\varepsilon = \min_i
  \varepsilon_i$ and check that $\varepsilon$ is a Lebesgue number.
 A: Many uses of Zorn's lemma really only need transfinite recursion, without any use of AC.  Sometimes you don't even need transfinite recursion, but just normal recursion, or even less.
This is especially applicable in specific examples.  For instance, you don't need AC to get an algebraic closure of $\mathbb{Q}$.
A: It is a theorem of ZF that every sequentially continuous function $\mathbb{R}\to\mathbb{R}$ is continuous.  The proof is usually given in ZFC (and indeed, Choice is necessary to assert that sequential continuity at a point implies continuity at that point), but a proof can be given in ZF that sequential continuity everywhere implies continuity everywhere: see Herrlich, The Axiom of Choice (2006), theorem 3.15 and subsequent remarks on page 30.
(The proof in ZF is bizarre and somewhat counterintuitive, and since it only works for continuity everywhere, it seems quite defensible to use Choice to prove this.)
A: One of my papers, A comment on the construction of the maximal globally hyperbolic Cauchy development, did this for the existence of the maximal globally hyperbolic Cauchy development for the initial value problem in general relativity.
The TL;DR is that the original proof had a gratuitous use of Zorn's lemma. The fix is similar, but also somewhat different from, the fix removing the use of Zorn from maximal atlases.
A: The supremum of an arbitrary set of measurable functions from a $\sigma$-finite measure space into $\mathbb R\cup \{\pm\infty\}$ exists in the following sense:
Let $F$ be a set of such measurable functions. Then there is measurable $g$ such that $f\le g$ a.e. for all $f\in F$. And if $h$ is such that $f\le h$ a.e. for all $f\in F$, then $g\le h$.
The trick is that the inequalities are required in the a.e. sense. I have seen proofs that use Zorn's lemma (which is tempting), but there is a proof without it (see, e.g., Bogachev's monograph on measure theory, it uses monotone convergence).
The result is also surprising because many properties in measure/integration theory have countability built-in.
A: Sometimes people prove the Schröder–Bernstein theorem by saying it follows easily from the well-ordering theorem, which is equivalent to the axiom of choice. But it can be proved without the axiom of choice. The theorem states that if there is a one-to-one mapping from each of two sets into the other, then there is also a bijection.
A: It's common to use the axiom of choice to prove that nonzero commutative rings have the invariant basis number property: in other words, that for a nonzero commutative ring $ R $, the $ R $-modules $ R^m $ and $ R^n $ are isomorphic if and only if $ m = n $.
The most common proof of this uses Zorn's lemma to find a maximal ideal $ \mathfrak m $ of $ R $. We can then tensor any isomorphism $ R^m \to R^n $ with $ R/\mathfrak m $ to get an isomorphism of $ R/\mathfrak m $-vector spaces $ (R/\mathfrak m)^m \to (R/\mathfrak m)^n $, which implies $ m = n $ by linear algebra since $ R/\mathfrak m $ is a field.
In fact, however, using Zorn's lemma is unnecessary. One way to see this is by looking at the exterior powers of the modules $ R^n $. The exterior power $ {\bigwedge}^n R^n $ is nonzero because the determinant $ (R^n)^n \to R $ is a surjective map that factors through $ {\bigwedge}^n R^n $, while $ {\bigwedge}^m R^n $ is obviously zero for $ m > n $. Therefore the rank of a free module over a nonzero commutative ring corresponds to its highest order exterior power that doesn't vanish, proving the difficult part of the claim that $ m \neq n $ implies $ R^m \ncong R^n $.
A: My favourite example is from Reverse Mathematics, namely Pincherle's theorem stating that
a locally bounded function on Cantor space is bounded there.
The obvious proof proceeds by contradiction and uses AC:

*

*Suppose $F:2^\mathbb{N}\rightarrow \mathbb{N}$ is unbounded, i.e. $(\forall n\in \mathbb{N})(\exists f \in 2^{\mathbb{N}})(F(f)>n)$.


*Apply (countable) choice to obtain a sequence $(f_n)_{n\in \mathbb{N}}$ such that $F(f_n)>n$ for all $n \in \mathbb{N}$.


*Use the sequential compactness of Cantor space to show that this sequence has a subsequence $(g_n)_{n\in \mathbb{N}}$ which converges to $g\in 2^\mathbb{N}$.


*Since $F$ is locally bounded, $F$ is bounded in a neighbourhood of $g$.  However, as $n$ increases, $g_n$ approaches $g$ and $F(g_n)$ becomes arbitrary large.  Contradiction.
There is a proof in ZF (and weaker systems) that is more delicate:
in step 2., one considers:
$(\forall n\in \mathbb{N})(\exists \sigma\in 2^{<\mathbb{N}})[(\exists f \in 2^{\mathbb{N}})(F(f)>n) \wedge \sigma = (f(0),..., f(|\sigma|) ]$.
One can apply `numerical choice' to obtain a sequence $(\sigma_n)_{n\in \mathbb{N}}$ such that:
$(\forall n\in \mathbb{N})[(\exists f \in 2^{\mathbb{N}})(F(f)>n) \wedge \sigma_n = (f(0),..., f(|\sigma_n|) ]$.
This `numerical' choice principle is provable in ZF.  Now use the sequence $(\sigma_n)_{n\in \mathbb{N}}$ instead of the sequence $(f_n)_{n\in \mathbb{N}}$; the rest of the proof then can be modified to obtain a contradiction on the same way.
A: The highly-upvoted, accepted answer (by Theo Johnson-Freyd) to another MO question, Why worry about the axiom of choice?, points out that the usual proof of the Poincaré–Birkhoff–Witt theorem assumes that every vector space has a basis and therefore uses the axiom of choice. However, the axiom of choice is not needed.
Johnson-Freyd uses this example to illustrate a wider point; namely, the analogue of the axiom of choice in other categories is "every epimorphism splits," which is false in other categories. Hence, a choice-free proof has the advantage of being easier to generalize to other settings.
A: A good number of theorems in Ramsey theory and related areas are what logicians call $\Pi^1_2$ statements—those of the form "for every set of integers $X$ there is a set of integers $Y$ satisfying some property which only quantifies over integers". Often, the easiest proofs of these results use AC, e.g. in the guise of using a nonprincipal ultrafilter or using nonstandard methods. But a consequence of Shoenfield's absoluteness theorem is that no theorem of this form can require choice for its proof.
A good example of this is Hindman's theorem (any finite coloring of $\mathbb N$ admits an infinite set whose set of finite sums is monochromatic). There's a very nice, quick proof through idempotent ultrafilters, which of course need (a fragment of) AC. There is an elementary proof, but it is much more involved and intricate, requiring you to do all the bookkeeping details by hand.
A: Turning ZM's comment into an answer: Zorn's lemma is sometimes invoked to show that the maximal atlas (in the definition of differentiable manifolds) exists, but it is unnecessary.
(This question is community wiki.)
A: The existence of a Haar measure on any locally compact group was first proven by Weil using the axiom of choice. Cartan later supplied a choice-free proof.
Because the Haar measure is unique up to a scalar factor, this is an example where it seems "obvious" that choice really shouldn't be necessary.
If anybody wants to edit to sketch one or both of the proofs, that would be most welcome!
A: It is easy to prove the following in Z+CC (Zermelo plus countable choice):

Every uncountable closed set of reals is in bijection with the reals.

I was informed by Asaf that it can be proven in ZF (no choice at all), but that proof appears to use replacement. I hence asked whether it could be proven in just Z, but till today there has been no answer. And whether the answer is yes or no, it would be very interesting. If yes, then the proof is likely to be far from obvious, maybe even not previously known. If no, then we have a theorem that needs either choice or replacement over Z, despite those two principles seeming to be completely unrelated.
A: I've seen Tychonoff's theorem be used to prove that the $ p $-adic integers are compact. The proof is easy: there is a natural embedding
$$ \mathbb Z_p \to \prod_{k=1}^{\infty} (\mathbb Z/p^k \mathbb Z) $$
whose image is closed, and the infinite product is compact by Tychonoff, so in particular we deduce that $ \mathbb Z_p $ is compact. (This strategy is used in general to show other profinite objects are compact, for instance, infinite Galois groups under the Krull topology.)
The use of Tychonoff (and by extension the axiom of choice) is unnecessary: we can simply adapt the usual proof of Heine-Borel over $ \mathbb R $ to show that $ \mathbb Z_p $ is compact. If there is an infinite open cover with no finite subcover, we can find an infinite descending chain of closed balls in $ \mathbb Z_p $ intersecting at a single point that need infinitely many open balls to cover them, and since an open ball including the single point will cover all sufficiently small closed balls including that point, we get a contradiction.
A: You can divide sets by two (or more): in classical ZF, if $A\sqcup A\simeq B\sqcup B$ then $A \simeq B$.
