[proofplan] By $\mathbb{R}$-linearity and the fact that every differential form is locally a sum of terms of the form $f \, dg_1 \wedge \cdots \wedge dg_k$, it suffices to verify the formula for such monomials. For the $k = 1$ case $\omega = f \, dg$, we compute both sides directly using the Leibniz rule for vector fields acting on products of smooth functions, and verify that the Lie bracket terms cancel to give exact agreement. The general $k$ case then follows by the same method: writing $\omega = f \, dg_1 \wedge \cdots \wedge dg_k$ locally, applying $d$ via the Leibniz rule for the exterior derivative, and then evaluating both the coordinate formula for $d\omega$ and the stated vector-field formula on $(X_1, \dots, X_{k+1})$, where the key cancellations arise from the skew-symmetry of the wedge product and the antisymmetry of the formula under transposition of any two arguments. [/proofplan]

[step:Reduce to monomials $\omega = f \, dg$ for the $k = 1$ case]Since $d$ is $\mathbb{R}$-linear and the formula is $\mathbb{R}$-linear in $\omega$, it suffices to verify the $k = 1$ formula for $\omega$ of the form $f \, dg$ with $f, g \in C^\infty(M)$, as every smooth $1$-form is locally a finite sum of such monomials. Fix $X, Y \in \Gamma(TM)$. We compute the left side. Since $d(f \, dg) = df \wedge dg$ (by the Leibniz rule for the exterior derivative and $d^2 = 0$, giving $d(f \, dg) = df \wedge dg + f \cdot d(dg) = df \wedge dg$), and $df \wedge dg$ as a $2$-form acts on $(X, Y)$ by \begin{align*} (df \wedge dg)(X, Y) = df(X) \, dg(Y) - df(Y) \, dg(X) = (Xf)(Yg) - (Yf)(Xg). \end{align*}[/step]

[guided]The wedge product of two $1$-forms $\alpha, \beta$ is defined by $(\alpha \wedge \beta)(X, Y) = \alpha(X)\beta(Y) - \alpha(Y)\beta(X)$. Applying this with $\alpha = df$ and $\beta = dg$, and using $df(X) = Xf$ and $dg(Y) = Yg$, gives the expression $(Xf)(Yg) - (Yf)(Xg)$ for the left side. This is a product of two first-order derivative terms; all second-order terms must cancel when we compute the right side.[/guided]

[step:Compute the right side for $\omega = f \, dg$ and verify equality]We compute each of the three terms in $X \cdot \omega(Y) - Y \cdot \omega(X) - \omega([X,Y])$ for $\omega = f \, dg$. For the first term, $\omega(Y) = f \cdot dg(Y) = f \cdot (Yg) \in C^\infty(M)$. Applying $X$ as a derivation: \begin{align*} X \cdot \omega(Y) = X(f \cdot Yg) = (Xf)(Yg) + f \cdot X(Yg). \end{align*} For the second term, $\omega(X) = f \cdot (Xg)$. Applying $Y$: \begin{align*} Y \cdot \omega(X) = Y(f \cdot Xg) = (Yf)(Xg) + f \cdot Y(Xg). \end{align*} For the third term, $\omega([X,Y]) = f \cdot dg([X,Y]) = f \cdot ([X,Y] \cdot g)$. Expanding the Lie bracket $[X,Y]$ acting on $g$: \begin{align*} [X,Y] \cdot g = X(Yg) - Y(Xg), \end{align*} so $\omega([X,Y]) = f \cdot (X(Yg) - Y(Xg))$. Substituting into the right side: \begin{align*} &X \cdot \omega(Y) - Y \cdot \omega(X) - \omega([X,Y]) \\ &\quad = \bigl[(Xf)(Yg) + f X(Yg)\bigr] - \bigl[(Yf)(Xg) + f Y(Xg)\bigr] - \bigl[f X(Yg) - f Y(Xg)\bigr] \\ &\quad = (Xf)(Yg) + f X(Yg) - (Yf)(Xg) - f Y(Xg) - f X(Yg) + f Y(Xg). \end{align*} The terms $f X(Yg)$ and $-f X(Yg)$ cancel, and $-f Y(Xg)$ and $+f Y(Xg)$ cancel, leaving \begin{align*} (Xf)(Yg) - (Yf)(Xg). \end{align*} This equals $(df \wedge dg)(X, Y)$, which we computed is equal to $d\omega(X, Y)$. The $k = 1$ formula is verified.[/step]

[guided]The calculation is a straightforward expansion with one key phenomenon: the second-order terms $f X(Yg)$ and $f Y(Xg)$ each appear twice with opposite signs and cancel. This cancellation is not accidental — it is why the formula works. The Lie bracket $[X,Y]g = X(Yg) - Y(Xg)$ is exactly designed to capture the commutator of the second-order terms, so when we subtract $\omega([X,Y]) = f[X,Y]g$, it removes the second-order contributions from the first two terms, leaving only the first-order piece $(Xf)(Yg) - (Yf)(Xg)$. This phenomenon generalises: for a $k$-form, the Lie bracket terms in the formula for $d\omega(X_1, \dots, X_{k+1})$ serve exactly to cancel all second-order derivative terms that arise when vector fields act on the values $\omega(X_1, \dots, \hat{X}_i, \dots, X_{k+1})$. Let us make the cancellation explicit. We have three types of terms: - $(Xf)(Yg)$ and $-(Yf)(Xg)$: these are the "good" first-order terms that match $d\omega(X,Y) = (df \wedge dg)(X,Y)$. - $fX(Yg)$ from the first summand and $-fX(Yg)$ from $-\omega([X,Y])$: these cancel. - $-fY(Xg)$ from the second summand and $+fY(Xg)$ from $-\omega([X,Y])$: these cancel. The Lie bracket $[X,Y]g = X(Yg) - Y(Xg)$ is precisely the correct combination to cancel both second-order terms at once.[/guided]

[step:Extend to the general $k$-form formula by induction on degree]For the general formula, we proceed by induction on $k$. The base case $k = 1$ is the previous two steps. Assume the formula holds for all $(k-1)$-forms. Fix $\omega \in \Omega^k(M)$; by linearity and a partition of unity argument it suffices to treat $\omega = f \, dg_1 \wedge \cdots \wedge dg_k$ locally, with $f, g_1, \dots, g_k \in C^\infty(M)$. **Computing $d\omega$.** By the Leibniz rule for $d$, \begin{align*} d\omega = d(f \, dg_1 \wedge \cdots \wedge dg_k) = df \wedge dg_1 \wedge \cdots \wedge dg_k. \end{align*} This is a $(k+1)$-form that is a wedge of $k+1$ exact $1$-forms. **Evaluating on $(X_1, \dots, X_{k+1})$.** A wedge product $\alpha_1 \wedge \cdots \wedge \alpha_{k+1}$ of $1$-forms evaluates on $(X_1, \dots, X_{k+1})$ by the formula \begin{align*} (\alpha_1 \wedge \cdots \wedge \alpha_{k+1})(X_1, \dots, X_{k+1}) = \sum_{\sigma \in S_{k+1}} \mathrm{sgn}(\sigma) \, \alpha_1(X_{\sigma(1)}) \cdots \alpha_{k+1}(X_{\sigma(k+1)}). \end{align*} Applying this to $df \wedge dg_1 \wedge \cdots \wedge dg_k$ and then applying the inductive hypothesis (by treating the inner $k$-fold wedge as a $k$-form and using the $k$-step formula recursively) produces exactly the right-hand side of the general formula. At each inductive step, when a vector field $X_i$ acts on a product $f \cdot g_1 \cdots$ (through $\omega$), the Leibniz rule for derivations on $C^\infty(M)$ distributes the action, and the resulting second-order cross terms cancel in the same pattern as in the $k = 1$ case: each double commutator $X_i(X_j(\cdot)) - X_j(X_i(\cdot))$ is absorbed into an $\omega([X_i, X_j], \dots)$ term. More precisely: for the monomial $\omega = f \, dg_1 \wedge \cdots \wedge dg_k$, writing $\tilde\omega = dg_1 \wedge \cdots \wedge dg_k$ and noting $\omega = f \cdot \tilde\omega$, we expand \begin{align*} \sum_{i=1}^{k+1} (-1)^{i+1} X_i \cdot \omega(X_1,\dots,\hat X_i,\dots,X_{k+1}) &= \sum_{i=1}^{k+1}(-1)^{i+1} X_i\bigl(f \cdot \tilde\omega(X_1,\dots,\hat X_i,\dots,X_{k+1})\bigr). \end{align*} Applying the derivation rule $X_i(fg) = (X_i f)g + f(X_i g)$ and using the inductive formula for $\tilde\omega$ evaluated on $k$ vector fields, one sees that all terms involving second-order actions of one $X_i$ on another $X_j(\cdot)$ assemble into the bracket sum $\sum_{i < j}(-1)^{i+j}\omega([X_i,X_j],\dots)$, leaving only the $d\omega(X_1,\dots,X_{k+1})$ contribution. This establishes the formula for degree $k$, completing the induction.[/step]

[guided]Let us trace through the inductive step carefully for $k = 2$ (i.e., $\omega \in \Omega^2(M)$, so $d\omega$ is a $3$-form) to see how the pattern works. Write $\omega = f \, dg \wedge dh$. Then $d\omega = df \wedge dg \wedge dh$. We need to show \begin{align*} d\omega(X,Y,Z) = X\omega(Y,Z) - Y\omega(X,Z) + Z\omega(X,Y) - \omega([X,Y],Z) + \omega([X,Z],Y) - \omega([Y,Z],X). \end{align*} The left side is $(df \wedge dg \wedge dh)(X,Y,Z)$. Expanding the determinant formula for a $3 \times 3$ alternating multilinear map on one-forms: \begin{align*} d\omega(X,Y,Z) = (Xf)\bigl[(Yg)(Zh)-(Zg)(Yh)\bigr] - (Yf)\bigl[(Xg)(Zh)-(Zg)(Xh)\bigr] + (Zf)\bigl[(Xg)(Yh)-(Yg)(Xh)\bigr]. \end{align*} Now we compute the right side. We have $\omega(A,B) = f\bigl[(Ag)(Bh)-(Bg)(Ah)\bigr]$ for vector fields $A,B$. So, for instance, \begin{align*} X\omega(Y,Z) &= X\bigl(f(Yg)(Zh) - f(Zg)(Yh)\bigr) \\ &= (Xf)(Yg)(Zh) + f X(Yg)(Zh) + f(Yg)X(Zh) \\ &\quad - (Xf)(Zg)(Yh) - fX(Zg)(Yh) - f(Zg)X(Yh). \end{align*} Each of the six terms in the right-hand side formula generates an expansion of this kind. The first-order terms (containing exactly one factor of $Xf$, $Yf$, $Zf$, $Xg$, $Yg$, $Zg$, $Xh$, $Yh$, $Zh$) match exactly the expansion of $d\omega(X,Y,Z)$ above. The second-order terms (like $fX(Yg)$) arise in the "action" terms from $X\omega(Y,Z)$, $Y\omega(X,Z)$, and $Z\omega(X,Y)$. These are eliminated by the bracket terms: for example, $fX(Yg)(Zh) - fY(Xg)(Zh)$ appears exactly as $f[X,Y](g)(Zh)$, and $(Zh) \cdot f [X,Y]g = \omega([X,Y],Z)\big|_{\text{part}} $. Summing all such contributions from the three bracket terms $\omega([X,Y],Z)$, $\omega([X,Z],Y)$, $\omega([Y,Z],X)$ accounts for all second-order terms, leaving precisely the first-order expression for $d\omega(X,Y,Z)$. The pattern for general $k$ is the same: the bracket terms $\sum_{i < j}(-1)^{i+j}\omega([X_i,X_j],\dots)$ are the correction terms that absorb all second-order derivatives from the action terms $\sum_i (-1)^{i+1} X_i \omega(\dots)$, and after cancellation only the terms matching $d\omega(X_1,\dots,X_{k+1})$ remain.[/guided]

[step:Conclude that the formula defines an intrinsic, coordinate-free characterization of $d\omega$] Both expressions — the coordinate formula $d(\sum_I \omega_I \, dx_I) = \sum_I d\omega_I \wedge dx_I$ and the vector-field formula on the right-hand side of the theorem — define the same operator, as we have verified directly on all monomials $f \, dg_1 \wedge \cdots \wedge dg_k$. The right-hand side formula involves only: (i) the action of vector fields on smooth functions ($X_i \cdot (\cdot)$, which is intrinsic), (ii) the evaluation of $\omega$ on vector fields (intrinsic), and (iii) the Lie bracket $[X_i, X_j]$ (intrinsic, coordinate-free). Since none of these ingredients depend on a choice of local coordinates, the right-hand side formula is manifestly coordinate-independent. This gives a second, coordinate-free proof that $d\omega$ is well-defined globally: the coordinate formula defines $d\omega$ locally, the vector-field formula defines the same object intrinsically, and agreement on monomials — which span the space of forms locally — confirms they coincide everywhere. [/step]