Prove the coordinate-free formula for the exterior derivative

Question

I can prove the following :

There exist a unique map $d:\Omega^k(M)\to \Omega^{k+1}(M)$ such that

1. $d$ is $\mathbb{R}$-linear
2. $d^2=0$
3. For a $0$-differential form (a function) $d$ reduces to the usual differential
4. $d(\omega\wedge\eta)=(d\omega)\wedge \eta+(-1)^k\omega\wedge d\eta$.

And I can prove that such a map is locally given by $$d(\sum_I a_Idx_{i_1}\wedge \ldots dx_{i_k})=\sum_Ida_I\wedge dx_{i_1}\wedge\ldots\wedge dx_{i_k}$$

where $(X_1,\ldots,\hat X_i,\ldots, X_k)$ means "remove $X_i$ from $(X_1,\ldots,X_k)$". e.g : $(X_1,\hat X_2,X_3)=(X_1,X_3)$

(by the way, I prove the existence part using that formula and the uniqueness part)

Now I want to prove the coordinate-free formula

$$ (d\omega)(X_1,\ldots X_{k+1})=\sum_i(-1)^{i-1}X_i\big( \omega(X_1,\ldots, \hat X_i,\ldots,X_{k+1}) \big)+\sum_{i<j}(-1)^{i+j}\omega\big( [X_i,X_j],X_1,\ldots \hat X_i,\ldots,\hat X_j,\ldots, X_{k+1} \big). \qquad (1) $$

I see two ways to prove that formula.

1. Prove that it satisfies the 4 conditions.
2. Prove that it locally reduces to the local expression

This answer goes for options 1. In the hint it gives, it supposes that one already checked that formula (1) is a $(k+1)$-form. It seems to me extremely difficult to prove anti-symmetry (I got into very long unsuccessful computations).

In the same way, here on page 2 it says "simple but messy computation"...

QUESTION: How do I prove formula 1 ? Preferably without going into long and painful computations.

Related:

• Formula for the exterior derivative
• Exterior derivative well-defined

EDIT. Full proof here. Search for the labels PROPooUOQRooAdvYqx and PROPooTXFRooMtaVrU. Disclamer : I'm the author and the text is not proof-read. Too long to be posted here as answer.