[proofplan] We prove the result in adapted local coordinates along the embedded submanifold $N$. In such coordinates, the conormal bundle is cut out in $T^*Q$ by the equations forcing the base point to lie in $N$ and the covector to vanish on the tangent directions of $N$. These equations show that $T_N^*Q$ is a smooth embedded submanifold of dimension $\dim Q$, and the [coordinate formula for the tautological one-form](/theorems/10042) then shows that $\lambda$ vanishes after restriction to $T_N^*Q$. Hence $\omega_{\mathrm{can}}=-d\lambda$ restricts to zero, and the half-dimensional isotropic submanifold is Lagrangian. [/proofplan] [step:Write the conormal bundle in coordinates adapted to $N$] Let $x\in N$. Since $N\subset Q$ is an embedded $k$-dimensional submanifold of the smooth $n$-manifold $Q$, the embedded submanifold local-coordinate theorem gives an open neighbourhood $U\subset Q$ of $x$ and a coordinate chart $(U,\varphi)$ with coordinate functions $q_1,\dots,q_n:U\to\mathbb R$ such that \begin{align*} N\cap U=\{y\in U:q_{k+1}(y)=\cdots=q_n(y)=0\}. \end{align*} Let $(q_1,\dots,q_n,p_1,\dots,p_n)$ denote the induced cotangent coordinates on $T^*U\subset T^*Q$, so that a covector $\alpha\in T_y^*Q$ with $y\in U$ is written as \begin{align*} \alpha=\sum_{i=1}^n p_i(\alpha)\,dq_i|_y. \end{align*} For $y\in N\cap U$, the tangent space $T_yN$ is spanned by the coordinate tangent vectors $\partial_{q_1}|_y,\dots,\partial_{q_k}|_y$. Therefore $\alpha$ vanishes on $T_yN$ if and only if \begin{align*} p_1(\alpha)=\cdots=p_k(\alpha)=0. \end{align*} Thus, inside $T^*U$, the conormal bundle is given by \begin{align*} T_N^*Q\cap T^*U=\{\alpha\in T^*U:q_{k+1}(\pi(\alpha))=\cdots=q_n(\pi(\alpha))=0\text{ and }p_1(\alpha)=\cdots=p_k(\alpha)=0\}. \end{align*} [guided] We want coordinates that make both conditions in the definition of $T_N^*Q$ visible. The first condition is that the base point lies in $N$; the second is that the covector kills every tangent vector to $N$. Since $N$ is an embedded $k$-dimensional submanifold of the $n$-manifold $Q$, the embedded submanifold local-coordinate theorem gives an open neighbourhood $U\subset Q$ of $x$ and coordinates $q_1,\dots,q_n:U\to\mathbb R$ such that \begin{align*} N\cap U=\{y\in U:q_{k+1}(y)=\cdots=q_n(y)=0\}. \end{align*} In these coordinates, the coordinate tangent vectors $\partial_{q_1}|_y,\dots,\partial_{q_k}|_y$ span $T_yN$ for every $y\in N\cap U$. Now pass to the cotangent bundle over $U$. The induced cotangent coordinates are $(q_1,\dots,q_n,p_1,\dots,p_n)$, meaning that every covector $\alpha\in T_y^*Q$ with $y\in U$ has the unique coordinate expression \begin{align*} \alpha=\sum_{i=1}^n p_i(\alpha)\,dq_i|_y. \end{align*} The condition $\pi(\alpha)\in N$ becomes \begin{align*} q_{k+1}(\pi(\alpha))=\cdots=q_n(\pi(\alpha))=0. \end{align*} The condition that $\alpha$ vanish on $T_{\pi(\alpha)}N$ is tested on the basis $\partial_{q_1}|_{\pi(\alpha)},\dots,\partial_{q_k}|_{\pi(\alpha)}$. Since \begin{align*} \alpha(\partial_{q_j}|_{\pi(\alpha)})=p_j(\alpha) \end{align*} for $1\le j\le k$, this vanishing condition is equivalent to \begin{align*} p_1(\alpha)=\cdots=p_k(\alpha)=0. \end{align*} Combining the base equations and the fiber equations gives the local description \begin{align*} T_N^*Q\cap T^*U=\{\alpha\in T^*U:q_{k+1}(\pi(\alpha))=\cdots=q_n(\pi(\alpha))=0\text{ and }p_1(\alpha)=\cdots=p_k(\alpha)=0\}. \end{align*} [/guided] [/step] [step:Deduce that the conormal bundle is a smooth half-dimensional submanifold] The coordinate description above shows that $T_N^*Q\cap T^*U$ is parametrized by the free coordinates \begin{align*} q_1,\dots,q_k,p_{k+1},\dots,p_n. \end{align*} Hence $T_N^*Q\cap T^*U$ is a smooth embedded submanifold of $T^*U$ of dimension \begin{align*} k+(n-k)=n. \end{align*} Since these adapted coordinate neighbourhoods cover $N$, the set $T_N^*Q$ is a smooth embedded submanifold of $T^*Q$ of dimension $n$. Also $\dim T^*Q=2n$, so \begin{align*} \dim T_N^*Q=\frac{1}{2}\dim T^*Q. \end{align*} [/step] [step:Show that the tautological one-form vanishes on the conormal bundle] Let $\lambda\in\Omega^1(T^*Q)$ be the tautological one-form. By the coordinate formula for the tautological form [citetheorem:10042], in the induced cotangent coordinates on $T^*U$ we have \begin{align*} \lambda=\sum_{i=1}^n p_i\,dq_i. \end{align*} Fix $\alpha\in T_N^*Q\cap T^*U$, and let $\xi\in T_\alpha(T_N^*Q)$ be a tangent vector. For $1\le i\le k$, the coordinate function $p_i$ vanishes on $T_N^*Q\cap T^*U$, so $p_i(\alpha)=0$. For $k+1\le i\le n$, the coordinate function $q_i$ is constant equal to $0$ on the base part of $T_N^*Q\cap T^*U$, so $dq_i(\xi)=0$. Therefore \begin{align*} \lambda_\alpha(\xi)=\sum_{i=1}^n p_i(\alpha)\,dq_i(\xi)=0. \end{align*} Since $\alpha$ and $\xi$ were arbitrary, the restricted one-form satisfies \begin{align*} \lambda|_{T_N^*Q}=0. \end{align*} [/step] [step:Restrict the canonical symplectic form and conclude the submanifold is Lagrangian] Let $\iota:T_N^*Q\hookrightarrow T^*Q$ denote the inclusion map. Since $\omega_{\mathrm{can}}=-d\lambda$, naturality of the [exterior derivative](/theorems/1525) under pullback gives \begin{align*} \iota^*\omega_{\mathrm{can}}=-\iota^*(d\lambda)=-d(\iota^*\lambda)=0. \end{align*} Thus $\omega_{\mathrm{can}}$ restricts to zero on $T_N^*Q$, so $T_N^*Q$ is isotropic. From the previous dimension computation, \begin{align*} \dim T_N^*Q=\frac{1}{2}\dim T^*Q. \end{align*} By the definition of a Lagrangian submanifold, an isotropic submanifold of half the ambient symplectic dimension is Lagrangian. Hence $T_N^*Q$ is a Lagrangian submanifold of $(T^*Q,\omega_{\mathrm{can}})$. [/step]