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!