[proofplan]
We construct the local Artin map by combining two ingredients: the Lubin--Tate isomorphism $U_K \cong \operatorname{Gal}(L_\infty/K)$ (sending $u$ to $\sigma_{u^{-1}}$) and the canonical map $\langle \pi \rangle \cong \operatorname{Frob}_K^{\mathbb{Z}}$ (sending $\pi^m$ to $\operatorname{Frob}_K^m$). Since $K^{\mathrm{ab}} = K^{\mathrm{ur}} \cdot L_\infty$ and $K^{\mathrm{ur}} \cap L_\infty = K$ (as $L_\infty/K$ is totally ramified and $K^{\mathrm{ur}}/K$ is unramified), the Weil group decomposes as $W(K^{\mathrm{ab}}/K) \cong \operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L_\infty/K)$, and the Artin map is the product of these two maps. We verify it is a well-defined homomorphism, and that it satisfies the defining properties of the local Artin map (compatibility with norm groups, surjectivity onto the Weil group).
[/proofplan]
[step:Decompose $K^\times$ and the Weil group into compatible factors]
Every element of $K^\times$ can be written uniquely as $\pi^m u$ with $m \in \mathbb{Z}$ and $u \in U_K = \mathcal{O}_K^\times$. This gives the decomposition
\begin{align*}
K^\times \cong \langle \pi \rangle \times U_K \cong \mathbb{Z} \times U_K.
\end{align*}
On the Galois side, the [Weil Group Decomposition](/theorems/2485) and the [Decomposition of the Maximal Abelian Extension](/theorems/2486) give $K^{\mathrm{ab}} = K^{\mathrm{ur}} \cdot L_\infty$. Since $L_\infty/K$ is totally ramified (as each $L_n/K$ is) and $K^{\mathrm{ur}}/K$ is unramified, the intersection $K^{\mathrm{ur}} \cap L_\infty = K$. Therefore
\begin{align*}
W(K^{\mathrm{ab}}/K) \cong \operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L_\infty/K),
\end{align*}
where $\operatorname{Frob}_K^{\mathbb{Z}} = W(K^{\mathrm{ur}}/K)$ is the Weil group of the unramified extension.
[/step]
[step:Define the map on each factor]
Define $\operatorname{Art}_K: K^\times \to W(K^{\mathrm{ab}}/K)$ by
\begin{align*}
\operatorname{Art}_K(\pi^m u) = (\operatorname{Frob}_K^m, \sigma_{u^{-1}}),
\end{align*}
where $\sigma_{u^{-1}} \in \operatorname{Gal}(L_\infty/K)$ is the automorphism defined by $\sigma_{u^{-1}}(\lambda) = [u^{-1}]_F(\lambda)$ for all $\lambda \in \bigcup_n F(n)$.
The map on the $\langle \pi \rangle$ factor sends $\pi^m \mapsto \operatorname{Frob}_K^m$, which is a group isomorphism $\langle \pi \rangle \xrightarrow{\sim} \operatorname{Frob}_K^{\mathbb{Z}}$.
The map on the $U_K$ factor sends $u \mapsto \sigma_{u^{-1}}$. By the [Galois Group of Lubin--Tate Extensions](/theorems/2394), this is a continuous group homomorphism $U_K \to \operatorname{Gal}(L_\infty/K) = \varprojlim_n \operatorname{Gal}(L_n/K)$. The kernel at level $n$ is $U_K^{(n)}$ (since $\sigma_{u^{-1}}|_{L_n} = \operatorname{id}$ iff $u \in U_K^{(n)}$), so the induced map $U_K/U_K^{(n)} \xrightarrow{\sim} \operatorname{Gal}(L_n/K)$ is an isomorphism for each $n$. Passing to the inverse limit, $U_K \xrightarrow{\sim} \operatorname{Gal}(L_\infty/K)$ is an isomorphism of profinite groups.
[guided]
Why do we use $u^{-1}$ rather than $u$? This is a normalization choice. The local Artin map is required to satisfy certain compatibility conditions with global class field theory and with the Frobenius element. The convention $u \mapsto \sigma_{u^{-1}}$ ensures that $\operatorname{Art}_K(N_{L_n/K}(x))$ acts directly on $L_n$ for all $x \in L_n^\times$. Concretely, this means that $\operatorname{Art}_K$ identifies $N(L_n/K)$ with the kernel of the restriction $W(K^{\mathrm{ab}}/K) \to \operatorname{Gal}(L_n/K)$, which is the defining property of the Artin map.
The inversion also ensures that $\operatorname{Art}_K(\pi)$ acts as $\operatorname{Frob}_K$ on $K^{\mathrm{ur}}$ and directly on $L_\infty$ (since $\pi$ has routine unit part). If we used $u$ instead of $u^{-1}$, the map would send norms to the wrong subgroup.
[/guided]
[/step]
[step:Verify $\operatorname{Art}_K$ is a group homomorphism]
Since $K^\times = \langle \pi \rangle \times U_K$ and $W(K^{\mathrm{ab}}/K) \cong \operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L_\infty/K)$ as direct products, and $\operatorname{Art}_K$ is defined as the product of two group homomorphisms (one on each factor), $\operatorname{Art}_K$ is automatically a group homomorphism.
More explicitly, for $\pi^{m_1} u_1, \pi^{m_2} u_2 \in K^\times$:
\begin{align*}
\operatorname{Art}_K(\pi^{m_1} u_1 \cdot \pi^{m_2} u_2) &= \operatorname{Art}_K(\pi^{m_1 + m_2} u_1 u_2) \\
&= (\operatorname{Frob}_K^{m_1 + m_2}, \sigma_{(u_1 u_2)^{-1}}) \\
&= (\operatorname{Frob}_K^{m_1} \cdot \operatorname{Frob}_K^{m_2}, \sigma_{u_1^{-1}} \circ \sigma_{u_2^{-1}}) \\
&= \operatorname{Art}_K(\pi^{m_1} u_1) \cdot \operatorname{Art}_K(\pi^{m_2} u_2),
\end{align*}
where $\sigma_{(u_1 u_2)^{-1}} = \sigma_{u_2^{-1} u_1^{-1}} = \sigma_{u_1^{-1}} \circ \sigma_{u_2^{-1}}$ because $[u_1^{-1} u_2^{-1}]_F = [u_1^{-1}]_F \circ [u_2^{-1}]_F$ (the $\mathcal{O}_K$-module structure is multiplicative on endomorphisms).
[/step]
[step:Verify $\operatorname{Art}_K$ is an isomorphism onto $W(K^{\mathrm{ab}}/K)$]
Since $\operatorname{Art}_K$ is the product of the isomorphism $\langle \pi \rangle \xrightarrow{\sim} \operatorname{Frob}_K^{\mathbb{Z}}$ and the isomorphism $U_K \xrightarrow{\sim} \operatorname{Gal}(L_\infty/K)$ (with the inversion on $U_K$, which is a group automorphism), the product map
\begin{align*}
\operatorname{Art}_K: K^\times = \langle \pi \rangle \times U_K \xrightarrow{\sim} \operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L_\infty/K) = W(K^{\mathrm{ab}}/K)
\end{align*}
is an isomorphism of groups.
[/step]
[step:Verify the norm group property]
We verify the key property: for each finite abelian extension $L_n/K$, $\ker(\operatorname{Art}_K \to \operatorname{Gal}(L_n/K)) = N(L_n/K)$.
The restriction of $\operatorname{Art}_K(\pi^m u)$ to $L_n$ acts as $\operatorname{Frob}_K^m$ on $L_n \cap K^{\mathrm{ur}} = K$ (since $L_n/K$ is totally ramified, so $L_n \cap K^{\mathrm{ur}} = K$) and as $\sigma_{u^{-1}}|_{L_n}$ on $L_n$. Therefore $\operatorname{Art}_K(\pi^m u)|_{L_n} = \operatorname{id}$ if and only if $\sigma_{u^{-1}}|_{L_n} = \operatorname{id}$, which holds if and only if $u \in U_K^{(n)}$. The condition on $m$ is vacuous (since the Frobenius acts directly on $L_n$, as $L_n/K$ is totally ramified). Hence
\begin{align*}
\ker(\operatorname{Art}_K \to \operatorname{Gal}(L_n/K)) = \langle \pi \rangle \times U_K^{(n)} = N(L_n/K),
\end{align*}
where the last equality is the [Norm Group of Lubin--Tate Extensions](/theorems/2395).
[/step]