Cartan formula for Steenrod squares on the cochain level Steenrod originally defined his squares using explicit cochain-level formulas for simplicial mod-2 cochains. To this end, he introduced higher cup products, which control the failure of the usual cup product to be supercommutative on the cochain level. On the other hand, H. Cartan formula tells us how Steenrod squares relate to the usual cup product of mod-2 cohomology classes. 
Questions.
(1) How does one show this using Steenrod's definition of Steenrod squares? 
(2) Is there some cochain-level relation between cup products of various degrees which implies 
Cartan's formula?
 A: I think that what you are searching for is explained in P. May's paper "A general algebraic approach to Steenrod operations".
In this paper you will find a very general treatment of cochain level cup-i product operations. In particular P. May introduces the concept of Cartan object and shows that the cohomology of Cartan object comes equipped with the action of Steenrod operations that satisfy the Cartan relations (see proposition 2.6). All the computations are made at the cochain level. The algebra of singular cochains of a topological space is a typical example of a Cartan object.
Moreover, we have an operadic interpretation:


*

*take an algebra $A$ over an $E_{\infty}$-algebra, then you have evaluation products $$\mu_r:E_{\infty}(r)\otimes A^{\otimes r}\rightarrow A$$ 
where each $E_{\infty}(r)$ is a projective resolution of the symmetric group $\Sigma_r$. 

*The evaluation product $\mu_2$ is risponsible for the action of cup-i products.

*If you take for $E_{\infty}$ the Baratt-Eclles operad $E$ it is a Hopf operad you have a coassiociative diagonal of operads $$\Delta:E\rightarrow E\otimes E.$$

*Cartan relations come from the Hopf operad structure AND the fact that $E$ is the resolution of the commutative operad $Com$.

*Cartan relations can be detected in the complex $E(4)$. 

