# Proving Wikipedia's formula on interior product of commutator of vector fields

During one of my daily exercises, I was looking for properties of the elements of Cartan calculus. I stumbled on Wikipedia's page about interior products (here), and I've noticed a property that sounds very useful: $$\iota_{[X,Y]}\omega=[\mathcal L_X,\iota_Y]\omega.$$ In Wikipedia's notations, $\iota$ is the interior product, $\mathcal L_X$ is the Lie derivative with respect to the vector field $X$ (and $X$ and $Y$ are vector fields). $\omega$ is a differential form on a manifold $M$. As there is no source given, I'm trying to prove this equality, and failing due to a sign. Maybe I'm doing some stupid error somewhere.

My attempt so far follows.

First: I note that the operator on the right has the property $$[\mathcal L_X,\iota _Y](\omega\wedge\eta)=[\mathcal L_X,\iota_Y]\omega\wedge\eta+(-1)^k\omega\wedge[\mathcal L_X,\iota_Y]\eta,$$ where $\omega$ is assumed to be a $k-$form, and $\eta$ is an arbitrary form. This is the same interaction with wedge product as the left hand side. It follows that I can decide the value of the right hand side locally, where I can expand any form as tensor product of the basis forms. Hence, if I prove that the equality holds for $0-$ and $1-$forms, I'm done.

I start with $0-$forms: I take a function $f$ from $M$ to the field, and compute left and right hand side. Well, "compute": the left hand side is the application of an inner product to a function, that is zero by definition, while on the right hand side I either have a contraction first, annulling $f$, or I have a Lie derivative acting first. The Lie derivative of a function is a function, so it follows that $\iota_Y\mathcal L f=0$, and I'm done for this case.

For $1-$forms: let $\alpha$ be such an $1-$form. The left hand side is $$\iota_{[X,Y]}\alpha=\alpha([X,Y]).$$ I split the calculation of the right hand side in two, and use Cartan's formula $\mathcal L_X=d\iota_X+\iota_Xd$ whenever necessary. Lie derivatives are ugly, all hail Cartan. $$\mathcal L_X\iota_Y\alpha=\mathcal L_X(\alpha (Y))=X(\alpha(Y)),\\ \iota_Y\mathcal L_X\alpha=\iota_Yd\iota_X\alpha+\iota_Y\iota_Xd\alpha=Y(\alpha(X))+\underline{d\alpha(Y,X)}.$$ Underlined for your convenience is the step in which it is most likely I've done an error, but I fail to see why. I state that $\iota_Y\iota_Xd\alpha=d\alpha(Y,X)$ as I am applying $X$ first, and $Y$ second, and $\iota$ places vectors at the beginning of a string. Is it correct? Was I stupid here?

Continuing: I use $$d\alpha(Y,X)=Y(\alpha(X))-X(\alpha(Y))-\alpha([Y,X]).$$ Here comes the failure. I'd expect stuff to cancel out, but that's not happening. The signs of $Y(\alpha(X))$ agree, so they do not cancel.

Where am I doing wrong? I strongly suspect that it is something in the underlined passage, but I need clarification about what I did wrong.

(p.s.: in some other places of this site there is a proof of that relying on a property of $\mathcal L_X$ acting on differential forms. As I said, I despise $\mathcal L_X$. I'd prefer to see the error in this proof, as it is short and nice. Lie has done many wonderful things, and an orrible derivative)
Yes, you are off by a sign on the term you figured. Remember that (for a $2$-form $\phi$) $\iota_X\phi(\cdot) = \phi(X,\cdot)$, so $\iota_Y\big(\iota_X\phi\big)=\phi(X,Y)$.
Be careful - the interior product places vectors in the first slot, but repeated applications should be read right-to-left, as function composition always is. That is, by definition we have $(i_X d \alpha)(Y) = d \alpha(X,Y);$ so applying $i_Y$ to the 1-form $i_X d \alpha$ yields this same result.