Proof of Cartan lemmma : why are the coefficients smooth?

I am new to differential geometry and I am struggling on the proof of the Cartan's lemma. The version I am trying to prove is the following.

Let $M$ be a smooth $n$-manifold, $\omega^1,...,\omega^k,\alpha^1,...,\alpha^k$ be smooth 1-forms such that

1. The $(\omega^i)$ are linearly independant
2. $\sum_{i=1}^k \alpha^i \wedge \omega^i= 0$.

Then the $(\alpha^i)$ are smooth linear linear combinations of the $(\omega^i)$.

I don't see how to prove the "smooth" part.

Here is how I managed to prove the fact that each $\alpha^i$ is linearly generated by the $(\omega^i)$. In the second assumption take the wedge product with $\omega^1 \wedge ... \wedge \omega^{k-1}$ to get $$ \alpha^k \wedge \omega^k \wedge \omega^1 \wedge ... \wedge \omega^{k-1} = 0. $$ I know that for covectors this means they are linearly dependant, so for all $p \in M$, $\alpha_p^1 , \omega^1_p,...,\omega^k_p$ are linearly dependant. Let $\lambda, \mu_1,...,\mu_k$ be reals not all null such that
$$ \lambda \alpha_p^k + \sum_{i=1}^k \mu_i\omega_p^i = 0. $$ We cannot have $\lambda = 0$ because then by the first assumption $\lambda = \mu_1 = ... = \mu_k = 0$. That is $\alpha_p^k \in \langle \omega_p^i \rangle_{i=1}^k$.

The same work can be done up to a change of index to prove that $\alpha_p^i \in \langle \omega_p^i \rangle_{i=1}^k$ for $i = 1,...,k$ arbitrary.

Now I don't know how to prove the coefficients are smooth, my idea would be to get a formula and see if it is smooth on $p$ but I don't see how to perform this operation.

Any hint in this direction, or a general fact about differential geometry that guaranty the coefficients to be smooth, would be appreciated.

Your reasoning is correct, I think the only "issue" is that you're losing a tiny bit of information at the step where you say "I know that for covectors this means [...]".

The $2$ hypotheses for Cartan's lemma are true for differential forms, but at that step, you're only proving it for covectors (ie, for differential forms restricted to one point of your manifold). So you lose the information of what's going on "around $p$".

While, actually, if you start with a smooth $1$-form $\omega$ on a manifold, it can be written locally as $\omega = \displaystyle\sum g_i \mathrm{d}x_i$ where the $g_i$ are smooth functions, and the $\{\mathrm{d}x_i\}$ form a local basis for the cotangent bundle (= a coframe, if you want a good explanation on this, check Prop. 11.18 of Intro to Smooth Manifolds, 2nd edition).

Then, your reasoning still holds, except now in the expression $\lambda \alpha^k + \displaystyle\sum_i \mu_i \omega^i$, the coefficients $\lambda$ and $\mu_i$ are smooth functions defined locally around $p$, instead of being scalars. Then, since you're only doing some basic operations on these sums to express each $\alpha$ in the $\{\omega\}$ basis, everything stays smooth :).

This is an interesting approach that I've never seen or thought of before. Here is a sketch of the standard approach, from which smoothness is a standard argument.

The lemma is this: Locally you can extend $\omega^1,\dots,\omega^k$ to a smooth basis of $1$-forms. (For example, in local coordinates, some choice of complementary set $dx^{j_1},\dots,dx^{j_{n-k}}$ will do it.)

Now write $\alpha^i = \sum_{j=1}^n f^i_j\omega^j$. The second condition allows you to see that $f^i_j = 0$ for $j>k$. Now argue directly that in this situation the $f^i_j$ must be smooth functions. (This boils down, again, in local coordinates, to the fact that the inverse of a smooth matrix function is smooth and the product of smooth functions is smooth.)