It starts with the observation that for a function and a vector field , the Lie derivative is and the exterior derivative evaluated at is . That is, on functions.
Next we consider the differential of a function. If we apply to it, the nilpotency of the exterior derivative tells us that we automatically get zero. On the other hand, if we apply , we get , which it turns out is . To see this, we calculate
just as if we took and applied it to .
So on exact -forms, gives zero while gives . And on functions gives , while gives zero. In both cases we find that
and in fact this holds for all differential forms, which follows from these two base cases by a straightforward induction. This is Cartan’s formula, and it’s the natural extension to all differential forms of the basic identity on functions.