Let $(X,\tau,\circ)$ be a compact Polish group. Is there necessarily a metric $d$ on $X$ inducing $\tau$ such that $d(x \circ a,x \circ b) = d(a \circ x, b \circ x) = d(a,b)$ for all $x,a,b \in X$?
If the answer is yes, I would appreciate a sketch of the argument establishing this.
Yes - the existence of a left-invariant metric on any Hausdorff first countable group is the Birkhoff-Kakutani theorem. Given a left-invariant metric $d$ on a compact group then just put $$ d'(a,b)=\sup_x d(ax,bx) \;. $$
PS Of course, the point is that all these metrics metrize the group topology.
Here's an alternative argument based on the Peter-Weyl theorem.
1) if $G$ is a connected compact Lie group, it has a bi-invariant Riemannian metric, which induces a bi-invariant distance.
2) if $G$ is a compact Lie group, choose a distance as in (1) on $G^0$, normalized so that the diameter is $\le 1$; extend it by left translation on each component, and say that any two points in different components have distance 1. This is a bi-invariant distance inducing the topology.
3) if $G$ is a product $\prod_nG_n$ of a sequence $(G_n)$ of compact Lie groups, choose a bi-invariant distance $d_n$ on $G_n$ of diameter $\le 1$ inducing the topology of $G_n$: then $d(g,h)=\sum_n2^{-n}d(g_n,h_n)$ is a bi-invariant distance inducing the topology of $G$.
4) if $G$ is an arbitrary compact metrizable topological group, it embeds, by the Peter-Weyl theorem, as a closed subgroup of $\prod_nG_n$ for some sequence $(G_n)$ of compact Lie groups. Using (3) and restricting, we get a bi-invariant distance on $G$ inducing the topology.
The answer is quite trivially yes. We have available to us some metric $d'$ inducing the topology $\tau$. We then define $$d(a,b) = \sup_{x \in \mathbf{X}} \quad \sup_{y \in \mathbf{X}} \quad d'(x \circ a \circ y, x \circ b \circ y)$$
Now $d$ inherits the property of being a metric from $d'$, and the bi-invariance is immediate from the construction.
As $\mathbf{X}$ is compact, $d$ is continuous w.r.t. $\tau$. As pointed out by YCor in the comments, whenever $(X,\tau)$ is compact Hausdorff and $d$ is a continuous metric on $(X,\tau)$, then $d$ already induces $\tau$ (as continuous bijections from compact spaces into Hausdorff spaces have continuous inverses).
The idea is taken from the answer by R W, but the use of Birkhoff-Kakutani is overkill here.
