[proofplan] The regular value hypothesis first turns $F^{-1}(c)$ into a smooth $n$-dimensional submanifold whose tangent space at $x$ is $\ker dF_x$. Poisson commutativity implies that all Hamiltonian vector fields $X_{f_i}$ are tangent to this fiber, and regularity implies that these $n$ tangent vectors are linearly independent. Hence they form a basis for the fiber tangent space, and Poisson commutativity again shows that $\omega$ vanishes on this basis. Therefore each [connected component](/page/Connected%20Component) of the regular fiber is an isotropic submanifold of half the ambient dimension, so it is Lagrangian. [/proofplan] [step:Identify the regular fiber as an $n$-dimensional submanifold] Let $N := F^{-1}(c)$.Since $c$ is a regular value of the smooth map $F:M\to\mathbb R^n$, the regular level set theorem applied to $F$ at the value $c$ gives that $N$ is an embedded smooth submanifold of $M$ and, for every $x\in N$, $T_xN = \ker dF_x$.Moreover $dF_x:T_xM\to T_c\mathbb R^n$ is surjective for every $x\in N$. Since $\dim T_xM=2n$ and $\dim T_c\mathbb R^n=n$, the [rank-nullity theorem](/theorems/916) gives $\dim T_xN = \dim\ker dF_x = 2n - n = n$.Thus every connected component $L\subset N$ is an embedded smooth $n$-dimensional submanifold of $M$, with $T_xL = T_xN = \ker dF_x$.for every $x\in L$. [/step] [step:Show the Hamiltonian vector fields are tangent to the regular fiber] Fix $x\in N$. For each $i\in\{1,\dots,n\}$, the Hamiltonian vector field $X_{f_i}\in\mathfrak X(M)$ satisfies $\iota_{X_{f_i}}\omega = df_i$.To prove that $(X_{f_i})_x\in T_xN$, it is enough to prove that $dF_x((X_{f_i})_x)=0$. Let $\pi_j:\mathbb R^n\to\mathbb R$ denote the $j$th coordinate projection, so that $f_j=\pi_j\circ F$. For every $j\in\{1,\dots,n\}$, the chain rule gives \begin{align*} d(\pi_j)_c(dF_x((X_{f_i})_x))=df_j|_x((X_{f_i})_x). \end{align*} Using $\iota_{X_{f_j}}\omega=df_j$, we compute \begin{align*} df_j|_x((X_{f_i})_x) = \omega_x((X_{f_j})_x,(X_{f_i})_x) = \{f_j,f_i\}(x) = 0. \end{align*} Since all coordinate components of $dF_x((X_{f_i})_x)$ are zero, we have \begin{align*} dF_x((X_{f_i})_x)=0. \end{align*} Thus $(X_{f_i})_x \in \ker dF_x = T_xN$. [guided] Fix a point $x\in N=F^{-1}(c)$. We want to prove that the vector $(X_{f_i})_x\in T_xM$ is actually tangent to the level set $N$. Since the tangent space to the level set is $\ker dF_x$, this means we must prove \begin{align*} dF_x((X_{f_i})_x)=0. \end{align*} A vector in $T_c\mathbb R^n$ is zero exactly when all of its coordinate components are zero. Let $\pi_j:\mathbb R^n\to\mathbb R$ be the $j$th coordinate projection. Since $F=(f_1,\dots,f_n)$, the identity $f_j=\pi_j\circ F$ holds. Applying the chain rule at $x$ to the vector $(X_{f_i})_x$ gives \begin{align*} d(\pi_j)_c(dF_x((X_{f_i})_x))=df_j|_x((X_{f_i})_x). \end{align*} Now the Hamiltonian convention is exactly what converts this derivative into a symplectic pairing. Because $X_{f_j}$ is defined by $\iota_{X_{f_j}}\omega=df_j$, we have \begin{align*} df_j|_x((X_{f_i})_x)=\omega_x((X_{f_j})_x,(X_{f_i})_x). \end{align*} By the definition of the Poisson bracket used in the statement, \begin{align*} \omega_x((X_{f_j})_x,(X_{f_i})_x)=\{f_j,f_i\}(x). \end{align*} The completely integrable system hypothesis says that $\{f_j,f_i\}=0$ for all $i,j$, hence \begin{align*} d(\pi_j)_c(dF_x((X_{f_i})_x))=0 \end{align*} for every $j\in\{1,\dots,n\}$. Therefore every coordinate component of $dF_x((X_{f_i})_x)$ is zero, so \begin{align*} dF_x((X_{f_i})_x)=0. \end{align*} Thus $(X_{f_i})_x\in\ker dF_x=T_xN$. [/guided] [/step] [step:Use regularity to prove these tangent vectors form a basis] Fix $x\in N$. Suppose that [real numbers](/page/Real%20Numbers) $a_1,\dots,a_n\in\mathbb R$ satisfy $\sum_{i=1}^n a_i(X_{f_i})_x = 0$. For every $v\in T_xM$, bilinearity of $\omega_x$ and the defining equation $\iota_{X_{f_i}}\omega=df_i$ give \begin{align*} 0 = \omega_x\left(\sum_{i=1}^n a_i(X_{f_i})_x, v\right) = \sum_{i=1}^n a_i\,df_i|_x(v). \end{align*} Hence $\sum_{i=1}^n a_i\,df_i|_x = 0$ as an element of $T_x^*M$. Because $c$ is a regular value, $dF_x:T_xM\to T_c\mathbb R^n$ is surjective. Since $F=(f_1,\dots,f_n)$ in the sense that $f_i=\pi_i\circ F$, surjectivity of $dF_x$ is equivalent to [linear independence](/page/Linear%20Independence) of the coordinate covectors $df_1|_x,\dots,df_n|_x\in T_x^*M$. Therefore $a_i=0$ for every $i\in\{1,\dots,n\}$. Thus $(X_{f_1})_x,\dots,(X_{f_n})_x$.are linearly independent vectors in $T_xN$. Since $\dim T_xN=n$, these $n$ linearly independent vectors form a basis: $T_xN = \operatorname{span}\{(X_{f_1})_x,\dots,(X_{f_n})_x\}$.[/step] [step:Prove that the symplectic form vanishes on the tangent spaces] Fix $x\in N$. From the previous step, every $u\in T_xN$ and every $v\in T_xN$ can be written as $u = \sum_{i=1}^n a_i(X_{f_i})_x$ and $v = \sum_{j=1}^n b_j(X_{f_j})_x$ for real coefficients $a_1,\dots,a_n,b_1,\dots,b_n\in\mathbb R$. By bilinearity of $\omega_x$, \begin{align*} \omega_x(u,v) = \sum_{i=1}^n\sum_{j=1}^n a_i b_j\,\omega_x((X_{f_i})_x,(X_{f_j})_x). \end{align*} For each pair $(i,j)$, the Poisson commutativity hypothesis gives \begin{align*} \omega_x((X_{f_i})_x,(X_{f_j})_x) = \{f_i,f_j\}(x). \end{align*} Since $\{f_i,f_j\}=0$ for all $i,j$, it follows that \begin{align*} \omega_x((X_{f_i})_x,(X_{f_j})_x)=0 \end{align*} for every pair $(i,j)$. Therefore \begin{align*} \omega_x(u,v) = 0. \end{align*} So $\omega_x|_{T_xN}=0$ for every $x\in N$. [/step] [step:Conclude that each connected component is Lagrangian] Let $L$ be a connected component of $N=F^{-1}(c)$. From the first step, $L$ is an embedded smooth submanifold of $M$ and \begin{align*} \dim L = n. \end{align*} Since $\dim M = 2n$, this is equivalent to \begin{align*} \dim L = \frac{1}{2}\dim M. \end{align*} From the previous step, for every $x\in L$, \begin{align*} \omega_x|_{T_xL} = 0. \end{align*} Moreover, \begin{align*} \dim T_xL = n. \end{align*} Since $\dim T_xM = \dim M = 2n$, we also have \begin{align*} \dim T_xL = \frac{1}{2}\dim T_xM. \end{align*} Thus $T_xL$ is an isotropic subspace of the symplectic [vector space](/page/Vector%20Space) $(T_xM,\omega_x)$ of half the ambient dimension. Equivalently, $T_xL\subset T_xM$ is a maximal isotropic subspace, so by the standard characterization of Lagrangian subspaces, $T_xL$ is Lagrangian in $T_xM$ for every $x\in L$. Hence, by the definition of a Lagrangian submanifold, $L$ is a Lagrangian submanifold of $(M,\omega)$. Since $L$ was an arbitrary connected component of $F^{-1}(c)$, every connected component of $F^{-1}(c)$ is Lagrangian. [/step]