Solution (source code)

= Solution

For a <diffeomorphism>, the differential and its inverse preserve the natural pairing of a <vector> with a <covector>. Consequently the <mixed tensor pullback> commutes with every <tensor contraction> $C$:
$$
\phi_s^*(CT)=C(\phi_s^*T).
$$
Differentiating at zero gives $\mathcal L_X(CT)=C(\mathcal L_XT)$. The <mixed tensor pullback> also preserves <tensor products>, so
$$
\phi_s^*(S\otimes T)=\phi_s^*S\otimes\phi_s^*T.
$$
The ordinary <product rule> for differentiation therefore yields
$$
\boxed{\mathcal L_X(S\otimes T)=(\mathcal L_XS)\otimes T+S\otimes(\mathcal L_XT).}
$$
This proves the contraction and <Leibniz rule> properties for all smooth generators, without needing straightening coordinates.

The suggested <flow-box theorem> applies locally only where $X\ne0$. For example $X=x\partial_x$ vanishes at $x=0$, so it cannot equal a coordinate basis vector there. Its local flow is nevertheless $\phi_s(x)=e^sx$ and $\phi_s^*dx=e^s dx$, giving $\mathcal L_Xdx=dx$ even at that zero. This <Lie derivative at a zero of its generator> illustrates why the general flow proof is needed to cover every point.