[proofplan] We prove the result locally near each point of $C$. Regularity says that $F$ is a submersion along $C$, so after choosing suitable local coordinates, $F$ becomes projection onto the last $k$ coordinates. In those adapted coordinates, the constraint set is exactly the coordinate slice where those last $k$ coordinates vanish, which gives the submanifold structure and codimension. The tangent space formula then follows by comparing tangent vectors to that coordinate slice with the kernel of the differential of the projection. [/proofplan]

[step:Put the constraint map into submersion normal form near a constrained point]Fix $q \in C$. Since $0$ is a regular value of $F$, the differential \begin{align*} dF_q: T_qQ \to T_0\mathbb{R}^k \cong \mathbb{R}^k \end{align*} is surjective. In particular $k \le n$ whenever $C$ is nonempty. Choose a smooth chart $(U,\varphi)$ of $Q$ around $q$, where \begin{align*} \varphi: U \to \varphi(U) \subset \mathbb{R}^n \end{align*} is a diffeomorphism onto an open subset. Let $x = (x_1,\dots,x_n)$ denote the corresponding coordinates, and define the coordinate expression \begin{align*} f: \varphi(U) \to \mathbb{R}^k, \quad f := F \circ \varphi^{-1}. \end{align*} The rank of the Jacobian matrix $Jf_{\varphi(q)}$ is $k$. After reordering the coordinates $x_1,\dots,x_n$ if necessary, the $k \times k$ minor of $Jf_{\varphi(q)}$ using the last $k$ variables is invertible. Define the smooth map \begin{align*} G: \varphi(U) \to \mathbb{R}^n, \quad G(x_1,\dots,x_n) := (x_1,\dots,x_{n-k}, f_1(x),\dots,f_k(x)). \end{align*} The Jacobian matrix $JG_{\varphi(q)}$ is invertible because its lower-right $k \times k$ block is the chosen invertible minor of $Jf_{\varphi(q)}$. By the finite-dimensional [inverse function theorem](/theorems/51), after replacing $U$ by a smaller open neighbourhood of $q$, the map $G$ is a diffeomorphism from $\varphi(U)$ onto an open subset $V \subset \mathbb{R}^n$. Define the adapted chart \begin{align*} \psi: U \to V, \quad \psi := G \circ \varphi. \end{align*} Writing $y = (y_1,\dots,y_n)$ for the coordinates on $V$, the construction of $G$ gives \begin{align*} F \circ \psi^{-1}(y) = (y_{n-k+1},\dots,y_n) \end{align*} for every $y \in V$.[/step]

[guided]We want coordinates in which the constraint equations become as simple as possible. The regularity hypothesis gives exactly the linear algebra needed for this. Fix $q \in C$. Since $0$ is a regular value of $F$, the differential \begin{align*} dF_q: T_qQ \to T_0\mathbb{R}^k \cong \mathbb{R}^k \end{align*} is surjective. Choose a smooth chart $(U,\varphi)$ around $q$, with \begin{align*} \varphi: U \to \varphi(U) \subset \mathbb{R}^n. \end{align*} In this chart define \begin{align*} f: \varphi(U) \to \mathbb{R}^k, \quad f := F \circ \varphi^{-1}. \end{align*} The differential of $f$ at $\varphi(q)$ represents $dF_q$ in coordinates, so its Jacobian matrix $Jf_{\varphi(q)}$ has rank $k$. Therefore some $k$ coordinate directions give an invertible $k \times k$ minor. Reordering coordinates if needed, assume this invertible minor uses the variables $x_{n-k+1},\dots,x_n$. Now define \begin{align*} G: \varphi(U) \to \mathbb{R}^n, \quad G(x_1,\dots,x_n) := (x_1,\dots,x_{n-k}, f_1(x),\dots,f_k(x)). \end{align*} The point of this definition is that the first $n-k$ coordinates are left unchanged, while the last $k$ coordinates are replaced by the constraint functions. The Jacobian matrix $JG_{\varphi(q)}$ has an invertible lower-right $k \times k$ block, and the first $n-k$ output coordinates depend on the first $n-k$ input coordinates as the identity. Hence $JG_{\varphi(q)}$ is invertible. By the finite-dimensional inverse function theorem, after shrinking $U$ to a smaller open neighbourhood of $q$, the map $G$ is a diffeomorphism from $\varphi(U)$ onto an open subset $V \subset \mathbb{R}^n$. Define the adapted coordinate chart \begin{align*} \psi: U \to V, \quad \psi := G \circ \varphi. \end{align*} In these new coordinates $y = (y_1,\dots,y_n)$, the last $k$ coordinates are precisely the components of $F$. Thus \begin{align*} F \circ \psi^{-1}(y) = (y_{n-k+1},\dots,y_n). \end{align*} This is the local normal form for a submersion: near a constrained point, the constraint map is projection onto the last $k$ coordinates.[/guided]

[step:Read the submanifold structure from the adapted coordinates] In the adapted chart $(U,\psi)$ obtained above, \begin{align*} C \cap U = \{p \in U : F(p) = 0\}. \end{align*} Applying $\psi$ and using the normal form for $F \circ \psi^{-1}$ gives \begin{align*} \psi(C \cap U) = V \cap \bigl(\mathbb{R}^{n-k} \times \{0\}\bigr), \end{align*} where $\{0\}$ denotes the singleton containing the zero vector in $\mathbb{R}^k$. The set $\mathbb{R}^{n-k} \times \{0\}$ is a linear subspace of $\mathbb{R}^n$ of dimension $n-k$. Therefore, in a neighbourhood of every point $q \in C$, the set $C$ is represented in a smooth chart as an open subset of this fixed linear subspace. These charts define a smooth embedded submanifold structure on $C$, and its dimension is $n-k$. Hence the codimension of $C$ in $Q$ is $k$. [/step]

[step:Identify tangent vectors to the coordinate slice with the kernel of $dF_q$] Fix $q \in C$, and use the adapted chart $(U,\psi)$ near $q$. Let \begin{align*} P: V \to \mathbb{R}^k, \quad P(y_1,\dots,y_n) := (y_{n-k+1},\dots,y_n) \end{align*} be the projection onto the last $k$ coordinates. The normal form says \begin{align*} F \circ \psi^{-1} = P. \end{align*} The tangent space of the coordinate slice $V \cap (\mathbb{R}^{n-k} \times \{0\})$ at $\psi(q)$ is \begin{align*} \mathbb{R}^{n-k} \times \{0\} \subset \mathbb{R}^n. \end{align*} Under the differential \begin{align*} d\psi_q: T_qQ \to T_{\psi(q)}\mathbb{R}^n \cong \mathbb{R}^n, \end{align*} the tangent space $T_qC$ is therefore carried to $\mathbb{R}^{n-k} \times \{0\}$. By the chain rule applied to $F = P \circ \psi$ on $U$, for every $v \in T_qQ$, \begin{align*} dF_q(v) = dP_{\psi(q)}(d\psi_q(v)). \end{align*} The differential $dP_{\psi(q)}: \mathbb{R}^n \to \mathbb{R}^k$ is the linear projection onto the last $k$ coordinates, so \begin{align*} \ker dP_{\psi(q)} = \mathbb{R}^{n-k} \times \{0\}. \end{align*} Thus \begin{align*} dF_q(v) = 0 \iff d\psi_q(v) \in \mathbb{R}^{n-k} \times \{0\} \iff v \in T_qC. \end{align*} Therefore \begin{align*} T_qC = \ker dF_q = \{v \in T_qQ : dF_q(v) = 0\}. \end{align*} Since $q \in C$ was arbitrary, the tangent space formula holds at every point of $C$. [/step]