I've been thinking about Monsky's Theorem that it is impossible to partition a square into an odd number of triangles of equal area. The proof depends on a theorem of Chevalley to extend the $2$-adic valaution on $\mathbb{Q}$ to a $2$-adic valuation on $\mathbb{R}$, and Chevalley's theorem relies on the axiom of choice for its proof. According to "Proofs from THE BOOK" (fifth edition, p.$151$) no other proof of Monsky's theorem is known.
If Monsky's theorem were false, the counterexample would be a finite, easily comprehensible object. All the other applications of the axiom of choice I can think of assert the existence of some infinite, complicated object that we don't expect to be able to construct: a Hamel basis for the reals over the rationals, a free ultrafilter, a bounded, non-measurable subset of the reals, and so on.
I recognize that Chevalley's theorem itself asserts the existence of just such an object, but I haven't been able to think of another example where the axiom or one of its consequences is used to prove the non-existence of some "concrete" finite object. I exclude the extensions of Monsky's theorem to other polygons and higher dimensions, of course.
Are such examples really rare? Can you supply any more?
Actually, there is a precise result which says that the axiom of choice cannot be necessary for too-concrete results (and in particular that it's not necessary to Monsky's theorem). This is Shoenfield absoluteness:
Actually Shoenfield says even more - e.g. CH won't be necessary either - but the above is already enough for the OP. It's also worth noting that Shoenfield is in fact completely constructive: it gives a very concrete way to transform a $\mathsf{ZFC}$-proof into a $\mathsf{ZF}$-proof.
"$\Pi^1_2$" is a purely syntactic notion: roughly speaking, a sentence is $\Pi^1_2$ if it has the form "For all $X$ there is some $Y$ such that $H(X,Y)$," where $X$ and $Y$ are "morally equivalent" to real numbers and $H$ involves only quantification over things "morally equivalent" to natural numbers. For example, finitely sets of points in $\mathbb{R}^n$ and continuous functions $\mathbb{R}^a\rightarrow\mathbb{R}^b$ are "morally equivalent" to real numbers, while rational numbers are "morally equivalent" to nautral numbers. Monsky's theorem falls into this category: a triangulation is specified by a finite tuple of reals, and the equal-area property amounts to saying that we can get approximations to the relevant areas which are within arbitrary positive rational differences from each other. (In fact this only involved one "interesting" quantification, namely over finite tuples of reals, so in fact Monsky's theorem is $\Pi^1_1$.)
Note that the above may not truly constitute an error in PftB: Shoenfield merely transforms an existing proof into a sharper proof, and one could still claim that we have no proof of Monsky's theorem whose idea doesn't use Choice. But on a purely technical level, choice cannot be necessary for the proof of such a concrete result.