Every open cover of a compact Hausdorff space has a finite open star-refinement

Let $\mathcal V$ be the family of all open sets $V$ such that $\overline V\subseteq U$ for some $U\in\mathcal U$. This family covers $X$. Indeed, for $x\in U\in\mathcal U$, normality separates the closed sets $\{x\}$ and $X\setminus U$ by disjoint open sets; the open set containing $x$ has closure contained in $U$. This definition uses no choices indexed by $X$.

We record a finite shrinking construction. Given a finite open cover $A_0,\ldots,A_{m-1}$, recursively put $F_i=X\setminus\left(\bigcup_{j<i}B_j\cup\bigcup_{j>i}A_j\right).$ The earlier covering clauses imply $F_i\subseteq A_i$. Normality separates $F_i$ from $X\setminus A_i$, giving an open $B_i$ with $F_i\subseteq B_i\subseteq\overline{B_i}\subseteq A_i$. At the last stage the $B_i$ cover $X$. Thus every finite open cover has an open shrinking whose closures remain in the original members.

Compactness gives a finite subcover $V_0,\ldots,V_{n-1}$ of $\mathcal V$. Finite choice supplies $U_i\in\mathcal U$ with $\overline{V_i}\subseteq U_i$ for each $i<n$.

From a finite cover $A_i$ and an open shrinking $B_i$ as in step 1.2, form, for each nonempty $S\subseteq\{0,\ldots,m-1\}$, $W_S=\left(\bigcap_{i\in S}A_i\right) \setminus\left(\bigcup_{j\notin S}\overline{B_j}\right),$ discarding empty members. These finitely many sets are open and cover $X$: at $x$, take $S=\{i:x\in A_i\}$. Moreover, choose $k$ with $x\in B_k$. Every $W_S$ containing $x$ has $k\in S$, so $W_S\subseteq A_k$. Hence the point-star $\operatorname{St}(x,\mathcal W)$ lies in $A_k$. Call this a barycentric refinement of $(A_i)$.

Apply step 2.2 to the finite cover $(U_i)$ and its shrinking $(V_i)$ from step 2.1, obtaining a finite open barycentric refinement $\mathcal W$ of $\mathcal U$. Apply steps 1.2 and 2.2 again to $\mathcal W$, obtaining a finite open barycentric refinement $\mathcal Z$ of $\mathcal W$.

The cover $\mathcal Z$ star-refines $\mathcal U$. Fix $Z_0\in\mathcal Z$ and $x\in Z_0$. Barycentricity of $\mathcal W$ gives $U\in\mathcal U$ with $\operatorname{St}(x,\mathcal W)\subseteq U$. If $Z\in\mathcal Z$ meets $Z_0$ at $y$, barycentricity of $\mathcal Z$ gives $W_y\in\mathcal W$ containing $\operatorname{St}(y,\mathcal Z)$. Both $Z_0$ and $Z$ lie in $W_y$, and $x\in W_y$, so $Z\subseteq W_y\subseteq\operatorname{St}(x,\mathcal W)\subseteq U$. Thus $\operatorname{St}(Z_0,\mathcal Z)\subseteq U$.

The finite open cover $\mathcal Z$ is therefore a star-refinement of the original cover.