Galois action on primes above a prime is transitive

Given: The data and hypotheses of the statement.

Chinese remainder theorem for pairwise comaximal ideals: Let $R$ be a commutative ring and let $I_1,\dots ,I_r$ be pairwise comaximal ideals, where $r\ge 1$. Then the canonical map $R⟶{\prod }_{i=1}^{r}R\mathrm{/}{I}_i,x⟼(x+I_1,\dots ,x+I_r)$ is surjective, its kernel is ${\bigcap }_{i=1}^r{I}_i$, and ${\bigcap }_{i=1}^r{I}_i={\prod }_{i=1}^r{I}_i\mathrm{.}$ Equivalently, $R\mathrm{/}{\prod }_{i=1}^r{I}_i\cong {\prod }_{i=1}^{r}R\mathrm{/}{I}_i\mathrm{.}$

Integral ideal factorisation in a number field, in ZF: Every nonzero integral ideal $\mathfrak{a}$ of ${\mathcal{O}}_K$ has a unique finite factorisation $\mathfrak{a}={\prod }_{i=1}^r{\mathfrak{p}}_i^{e_i}$ into distinct nonzero prime ideals, with $e_i>0$. The finite choices in this construction are least-coded finite choices, so the assertion uses no Choice.

Norm and trace from embeddings, with the inseparable exponent in the norm formula: Let $K\mathrm{/}F$ be a finite field extension, let $\mathrm{\Omega }\mathrm{/}F$ be an algebraic closure, let $\mathrm{\Sigma }={\mathrm{Hom}}_F(K,\mathrm{\Omega })$, and let $[K:F{]}_i$ be the inseparable degree (def-inseparable-degree). Then for every $a\in K$, ${\mathrm{Tr}}_{K\mathrm{/}F}(a)=[K:F{]}_i{\sum }_{\sigma \in \mathrm{\Sigma }}\sigma (a),$ and $N_{K\mathrm{/}F}(a)={({\prod }_{\sigma \in \mathrm{\Sigma }}\sigma (a))}^{[K:F{]}_i}\mathrm{.}$ In particular, when $K\mathrm{/}F$ is separable these are the ordinary sum and product over the distinct $F$-embeddings of $K$ into $\mathrm{\Omega }$; and when $[K:F{]}_i>1$ in characteristic $p>0$, the trace map is identically zero because $[K:F{]}_i$ is a power of $p$.