[proofplan] We complexify the real-analytic CR data near the point $p$. The real-analytic local frame of $T_{0,1}M$ extends to a holomorphic frame on a complexification, and formal integrability implies that the extended holomorphic distribution is involutive. The holomorphic Frobenius theorem then supplies holomorphic first integrals whose differentials cut out exactly this distribution. Restricting these first integrals to the real slice gives CR functions, and the transversality condition for a hypersurface-type CR structure makes their joint differential injective on real tangent spaces; after shrinking, the resulting CR immersion is a local embedding. [/proofplan]

[step:Choose a real-analytic frame for the antiholomorphic CR bundle] Let $\dim_{\mathbb R}M=2m+1$. Fix $p\in M$. Since $T_{0,1}M\subset \mathbb C TM$ is a real-analytic complex vector subbundle of rank $m$, there is a real-analytic coordinate neighbourhood $U_0\subset M$ of $p$ and real-analytic sections $L_1,\dots,L_m\in \Gamma(U_0,T_{0,1}M)$ which form a complex frame for $T_{0,1}M$ over $U_0$. Because the CR structure is formally integrable, the space of local sections of $T_{0,1}M$ is closed under the Lie bracket. Hence, after possibly shrinking $U_0$, there are real-analytic functions $c_{jk\ell}:U_0\to \mathbb C$ such that, for every $1\le j,k\le m$, $[L_j,L_k]=\sum_{\ell=1}^m c_{jk\ell}L_\ell$. [/step]

[step:Extend the CR distribution holomorphically to a complexification]Since $U_0$ is real-analytic, shrink $U_0$ to a smaller real-analytic coordinate neighbourhood $U$ of $p$ which admits a complexification $U^{\mathbb C}$. This means that $U$ is embedded as a totally real real-analytic submanifold of a complex manifold $U^{\mathbb C}$ of complex dimension $2m+1$, and every real-[analytic function](/page/Analytic%20Function) or vector field on $U$ extends uniquely, after shrinking, to a [holomorphic function](/page/Holomorphic%20Function) or holomorphic vector field on $U^{\mathbb C}$. Let $\Gamma_{\mathrm{hol}}(U^{\mathbb C},T_{1,0}U^{\mathbb C})$ denote the space of holomorphic sections of the holomorphic tangent bundle $T_{1,0}U^{\mathbb C}$. Let \begin{align*} \widetilde L_j\in \Gamma_{\mathrm{hol}}(U^{\mathbb C},T_{1,0}U^{\mathbb C}) \end{align*} denote the holomorphic extension of $L_j$ for $1\le j\le m$, and let $\widetilde c_{jk\ell}:U^{\mathbb C}\to \mathbb C$ denote the holomorphic extension of $c_{jk\ell}$. Define the holomorphic rank-$m$ distribution $\mathcal L_q:=\operatorname{span}_{\mathbb C}\{\widetilde L_1(q),\dots,\widetilde L_m(q)\}\subset T_{1,0,q}U^{\mathbb C}$ for $q\in U^{\mathbb C}$, after shrinking $U^{\mathbb C}$ so that the $\widetilde L_j$ remain linearly independent. The holomorphic vector field $[\widetilde L_j,\widetilde L_k]-\sum_{\ell=1}^m \widetilde c_{jk\ell}\widetilde L_\ell$ vanishes on the real slice $U$. Since a holomorphic vector field on a complexification that vanishes on a totally real real-analytic submanifold vanishes in a neighbourhood of that submanifold, after shrinking $U^{\mathbb C}$ we have $[\widetilde L_j,\widetilde L_k]=\sum_{\ell=1}^m \widetilde c_{jk\ell}\widetilde L_\ell$. Thus $\mathcal L$ is an involutive holomorphic distribution.[/step]

[guided]The purpose of complexification is to replace the real-analytic CR problem by a holomorphic Frobenius problem. Since the coefficients of the vector fields $L_j$ are real-analytic in real coordinates on $U$, each coefficient has a holomorphic extension to a complex neighbourhood $U^{\mathbb C}$. Extending every coefficient gives holomorphic vector fields \begin{align*} \widetilde L_j\in \Gamma_{\mathrm{hol}}(U^{\mathbb C},T_{1,0}U^{\mathbb C}) \end{align*} whose restrictions to the real slice are exactly the original CR vector fields $L_j$. We must check that the extended distribution is still involutive. On the real slice, formal integrability gives real-analytic functions \begin{align*} c_{jk\ell}:U&\to \mathbb C \end{align*} with \begin{align*} [L_j,L_k]=\sum_{\ell=1}^m c_{jk\ell}L_\ell. \end{align*} Let $\widetilde c_{jk\ell}:U^{\mathbb C}\to\mathbb C$ be their holomorphic extensions. Consider the holomorphic vector field \begin{align*} A_{jk}:=[\widetilde L_j,\widetilde L_k]-\sum_{\ell=1}^m \widetilde c_{jk\ell}\widetilde L_\ell. \end{align*} By construction, $A_{jk}$ restricts to zero on $U$. A holomorphic function that vanishes on a totally real real-analytic slice vanishes in a neighbourhood of that slice; applying this coefficient by coefficient to $A_{jk}$ shows that $A_{jk}=0$ after shrinking $U^{\mathbb C}$. Hence \begin{align*} [\widetilde L_j,\widetilde L_k]=\sum_{\ell=1}^m \widetilde c_{jk\ell}\widetilde L_\ell, \end{align*} so the holomorphic distribution \begin{align*} \mathcal L_q=\operatorname{span}_{\mathbb C}\{\widetilde L_1(q),\dots,\widetilde L_m(q)\} \end{align*} is closed under Lie brackets. This is exactly the involutivity hypothesis needed for the holomorphic Frobenius theorem.[/guided]

[step:Apply holomorphic Frobenius to obtain independent first integrals] We now use the holomorphic Frobenius theorem in the standard rank-$m$ form for complex manifolds of dimension $2m+1$: if $X$ is such a manifold and $\mathcal D\subset T_{1,0}X$ is an involutive holomorphic subbundle of rank $m$, then near every point there exists a holomorphic submersion $Z:X\to \mathbb C^{m+1}$ whose differential satisfies $\ker dZ_q=\mathcal D_q$ at every point $q$ in the chosen neighbourhood. Equivalently, writing $Z=(Z_1,\dots,Z_{m+1})$, the component functions are holomorphic first integrals with linearly independent differentials and common kernel exactly $\mathcal D$. Applying this theorem to $\mathcal L$ at $p\in U^{\mathbb C}$, shrink $U^{\mathbb C}$ again and obtain holomorphic functions $Z_1,\dots,Z_{m+1}:U^{\mathbb C}\to \mathbb C$ such that, for the joint map $Z:U^{\mathbb C}\to\mathbb C^{m+1}$, $Z(q)=(Z_1(q),\dots,Z_{m+1}(q))$, the differential $dZ_q$ has complex rank $m+1$ and $\ker dZ_q=\mathcal L_q$ for every $q$ in the chosen neighbourhood. In component form this says $\widetilde L_j Z_\alpha=0$ for every $1\le j\le m$ and $1\le \alpha\le m+1$, and $\mathcal L_q=\bigcap_{\alpha=1}^{m+1}\ker dZ_{\alpha,q}$. Here $dZ_{\alpha,q}:T_qU^{\mathbb C}\to \mathbb C$ denotes the complex differential of $Z_\alpha$ at $q$. [/step]

[step:Restrict the first integrals to obtain CR functions] Define $f_\alpha:U\to \mathbb C$ by $f_\alpha(x)=Z_\alpha(x)$ for $x\in U$, where $U$ is viewed as the real slice of $U^{\mathbb C}$. Since $Z_\alpha$ is holomorphic on $U^{\mathbb C}$ and $U$ is real-analytic, each $f_\alpha$ is real-analytic. For every section $L\in \Gamma(U,T_{0,1}M)$, write $L=\sum_{j=1}^m a_jL_j$ with real-analytic functions $a_j:U\to\mathbb C$. Then, for every $1\le \alpha\le m+1$, $L f_\alpha=\sum_{j=1}^m a_j L_j(Z_\alpha|_U)=\sum_{j=1}^m a_j(\widetilde L_jZ_\alpha)|_U=0$. Thus each $f_\alpha$ is a CR function on $U$. [/step]

[step:Show that the CR functions give an immersion on the real slice] Define $F:U\to \mathbb C^{m+1}$ by $F(x)=(f_1(x),\dots,f_{m+1}(x))$. We prove that $dF_x:T_xM\to T_{F(x)}\mathbb C^{m+1}$ is injective after shrinking $U$. Fix $x\in U$ and let $v\in T_xM$ satisfy $dF_x(v)=0$. Complexify the real tangent space by setting $\mathbb C T_xM:=T_xM\otimes_{\mathbb R}\mathbb C$. The real-analytic inclusion $U\hookrightarrow U^{\mathbb C}$ induces a canonical complex-linear identification $\mathbb C T_xM\cong T_{1,0,x}U^{\mathbb C}$ under which the real slice corresponds to the fixed-point set of complex conjugation and the subspace $T_{0,1,x}M\subset \mathbb C T_xM$ identifies with the holomorphic distribution $\mathcal L_x$. Let $v_{1,0}$ denote the image of $v$ under this identification. Since $f_\alpha=Z_\alpha|_U$, the real differential $df_{\alpha,x}(v)$ equals $dZ_{\alpha,x}(v_{1,0})$. The equality $dF_x(v)=0$ therefore gives $dZ_{\alpha,x}(v_{1,0})=0$ for every $1\le \alpha\le m+1$. Hence $v_{1,0}\in \bigcap_{\alpha=1}^{m+1}\ker dZ_{\alpha,x}=\mathcal L_x$, so $v_{1,0}$ lies in $T_{0,1,x}M$. Because $v$ is real, this forces $v\in T_{1,0,x}M\cap T_{0,1,x}M=\{0\}$ by the hypersurface-type hypothesis. Therefore $v=0$, and $dF_x$ is injective. [/step]

[step:Shrink the neighbourhood so that the immersion is an embedding] The map $F:U\to\mathbb C^{m+1}$ is real-analytic because its components are real-analytic. The previous step shows that $F$ is an immersion near $p$. By the local normal form for immersions, after replacing $U$ by a smaller open neighbourhood of $p$, the map $F$ is a real-analytic embedding of $U$ onto a real-analytic submanifold of $\mathbb C^{m+1}$. Its components are the CR functions $f_1,\dots,f_{m+1}$ constructed above. Therefore $F$ is a real-analytic CR embedding of a neighbourhood of $p$ into $\mathbb C^{m+1}$. Taking $N=m+1$ proves the theorem. [/step]