The standard proof of Cartan's magic formula is to study derivations of the exterior algebra. One can relatively easily find that a derivation $D:\Omega(M)\rightarrow\Omega(M)$ can be reconstruced if it is known how $D$ acts on $\Omega^ 0(M)$ and $\Omega^ 1(M)$. Given $d\circ i_X+i_X\circ d$, one can then show that this is a grade $0$ derivation, and for a function $f\in\Omega^ 0(M)$, $(d\circ i_X+i_X\circ d)f=i_Xdf=Xf=\mathcal{L}_Xf$ and for an 1-form $\omega\in\Omega^1(M)$, $$(d\circ i_X+i_X\circ d)\omega=di_X\omega+i_Xd\omega=d(X^\mu\omega_\mu)+i_X(\partial_\nu\omega_\mu dx^\nu\wedge dx^\mu)=dX^\mu\omega_\mu+X^\mu d\omega_\mu+\partial_\nu\omega_\mu(dx^\nu(X)dx^\mu-dx^\mu(X)dx^\nu)=(\frac{\partial X^\mu}{\partial x^\nu}\omega_\mu+X^\mu\frac{\partial \omega_\mu}{\partial x^\nu})dx^\nu+(X^\mu\partial_\mu\omega_\nu-X^\mu\partial_\nu\omega_\mu)dx^\nu=(X^\mu\partial_\mu\omega_\nu+\omega_\mu\partial_\nu X^\mu)dx^\nu=\mathcal{L}_X\omega,$$ so by the theorem on derivations, $\mathcal{L}_X=d\circ i_X+i_X\circ d$.
This proof however is rather unintuitive, and it is clear we already know what the result is. Furthermore, just looking at the geometric meaning of $\mathcal{L}_X$, it is absolutely not trivial that such a relationship between $\mathcal{L}_X,i_X$ and $d$ should even exist. I don't know if other proofs of this formula exist (probably yes), but I have tried on my own several times to use only the basic definitions of the three (anti-)derivations present in the formula to prove it, but I have failed very time.
In short, I think this result is absolutely not trivial and it's name (it's a "magic" formula after all) seems to imply the same.
I am curious how did Cartan originally realize this formula. Where did the idea came that there might be this relation after all?