Let $ X $ be a set and $ \sim $ an equivalence relation on $ X $.
In many proofs, a set of representatives of equivalence classes of $ X $ is used (e.g. coset or orbit representatives in groups, prime representatives in factorial rings, ...).
Do these proofs tacitly use the axiom of choice?
On
If you choose a representative without justification, you are using choice. However, for some situations, the hypothesis of the axiom of choice can be discharged if there is a better method of making the selection.
On
Sometimes you need AC and sometimes not. For example, consider the equivalence relation on the reals such that $x \sim y$ if $x - y \in \mathbb{Z}$. The set of equivalence classes is denoted $\mathbb{R}/\mathbb{Z}$. I can choose a representative from each class by noting that each class has exactly one member in $[0,1)$. So I just choose that member as a representative, and $[0,1)$ is a complete set of representatives, one per class, and no Choice is needed.
On the other hand if we do the same thing with $\mathbb{R}/\mathbb{Q}$, as in the construction of the Vitali set, we do need to apply AC because there's no way to specify a choice from each class.
Yes. Let $Y$ be the set of equivalence classes of $X$ under $\sim$. Then $X=\bigcup Y$ and choosing a representative of each equivalence class is equivalent to defining a function $f:Y \to X$ such that $f(A)\in A$ for every $A\in Y$. By definition, such $f$ is a choice function of $Y$ whose existence is assured only if you assume the axiom of choice.
Of course, if $Y$ is finite, this requires the axiom of finite choice, which is deducible from $ZF$, so there's no real problem here. But as soon as $Y$ is infinite, you cannot guarantee, in general, the existence of such $f$ from $ZF$.