[proofplan] We prove the Leibniz rule $d(\phi \smile \psi) = (d\phi) \smile \psi + (-1)^k \phi \smile (d\psi)$ by direct computation on a singular $(k+\ell+1)$-simplex $\sigma: \Delta^{k+\ell+1} \to X$. The left-hand side $d(\phi \smile \psi)(\sigma) = (\phi \smile \psi)(d\sigma)$ expands into a sum of $k + \ell + 2$ terms. We split this sum at the shared vertex $v_k$ and show that the terms with $0 \leq i \leq k$ match $(d\phi) \smile \psi$ while the terms with $k+1 \leq i \leq k+\ell+1$ match $(-1)^k \phi \smile (d\psi)$, with the boundary terms at $i = k+1$ and $i = k$ cancelling. [/proofplan]

[step:Expand the left-hand side $d(\phi \smile \psi)(\sigma)$] Let $\phi \in C^k(X; R)$ and $\psi \in C^\ell(X; R)$, and let $\sigma: \Delta^{k+\ell+1} \to X$ be a singular $(k+\ell+1)$-simplex with vertices $v_0, \ldots, v_{k+\ell+1}$. The coboundary of the cup product evaluated on $\sigma$ is \begin{align*} d(\phi \smile \psi)(\sigma) &= (\phi \smile \psi)(d\sigma) = \sum_{i=0}^{k+\ell+1} (-1)^i (\phi \smile \psi)(\sigma \circ \delta_i), \end{align*} where $\delta_i: \Delta^{k+\ell} \to \Delta^{k+\ell+1}$ is the $i$-th face inclusion (omitting vertex $v_i$). By the definition of the cup product, each term is \begin{align*} (\phi \smile \psi)(\sigma \circ \delta_i) = \phi\!\left((\sigma \circ \delta_i)|_{[w_0, \ldots, w_k]}\right) \cdot \psi\!\left((\sigma \circ \delta_i)|_{[w_k, \ldots, w_{k+\ell}]}\right), \end{align*} where $w_0, \ldots, w_{k+\ell}$ are the vertices of $\Delta^{k+\ell}$ — that is, the vertices of $\Delta^{k+\ell+1}$ with $v_i$ omitted. We must track how omitting vertex $v_i$ from $\{v_0, \ldots, v_{k+\ell+1}\}$ affects the front $(k+1)$-vertex set and the back $(\ell+1)$-vertex set. [/step]

[step:Expand the right-hand side $(d\phi) \smile \psi + (-1)^k \phi \smile (d\psi)$] **First term:** $(d\phi) \smile \psi$ evaluated on $\sigma$ gives \begin{align*} ((d\phi) \smile \psi)(\sigma) &= (d\phi)\!\left(\sigma|_{[v_0, \ldots, v_{k+1}]}\right) \cdot \psi\!\left(\sigma|_{[v_{k+1}, \ldots, v_{k+\ell+1}]}\right) \\ &= \sum_{i=0}^{k+1} (-1)^i \phi\!\left(\sigma|_{[v_0, \ldots, \hat{v}_i, \ldots, v_{k+1}]}\right) \cdot \psi\!\left(\sigma|_{[v_{k+1}, \ldots, v_{k+\ell+1}]}\right). \end{align*} **Second term:** $(-1)^k (\phi \smile (d\psi))$ evaluated on $\sigma$ gives \begin{align*} (-1)^k (\phi \smile (d\psi))(\sigma) &= (-1)^k \phi\!\left(\sigma|_{[v_0, \ldots, v_k]}\right) \cdot (d\psi)\!\left(\sigma|_{[v_k, \ldots, v_{k+\ell+1}]}\right) \\ &= (-1)^k \phi\!\left(\sigma|_{[v_0, \ldots, v_k]}\right) \cdot \sum_{j=0}^{\ell+1} (-1)^j \psi\!\left(\sigma|_{[v_k, \ldots, \hat{v}_{k+j}, \ldots, v_{k+\ell+1}]}\right). \end{align*} We now match the LHS and RHS term by term. [/step]

[step:Match the terms for $0 \leq i \leq k$ on the LHS with the first sum on the RHS] For $0 \leq i \leq k$, the face $\sigma \circ \delta_i$ omits vertex $v_i$. The remaining vertices are $v_0, \ldots, \hat{v}_i, \ldots, v_{k+\ell+1}$. The front $k$-face of $\sigma \circ \delta_i$ uses the first $k+1$ of these remaining vertices: $v_0, \ldots, \hat{v}_i, \ldots, v_{k+1}$. The back $\ell$-face uses the last $\ell+1$ vertices: $v_{k+1}, \ldots, v_{k+\ell+1}$. Therefore \begin{align*} (-1)^i (\phi \smile \psi)(\sigma \circ \delta_i) = (-1)^i \phi\!\left(\sigma|_{[v_0, \ldots, \hat{v}_i, \ldots, v_{k+1}]}\right) \cdot \psi\!\left(\sigma|_{[v_{k+1}, \ldots, v_{k+\ell+1}]}\right). \end{align*} Summing over $0 \leq i \leq k+1$ on the RHS first term gives exactly the same expression, except the RHS first term also includes the $i = k+1$ term. [/step]

[step:Match the terms for $k+1 \leq i \leq k+\ell+1$ on the LHS with the second sum on the RHS] For $k+1 \leq i \leq k+\ell+1$, write $i = k + j$ with $1 \leq j \leq \ell+1$. The face $\sigma \circ \delta_i$ omits $v_{k+j}$. The remaining vertices are $v_0, \ldots, v_k, v_{k+1}, \ldots, \hat{v}_{k+j}, \ldots, v_{k+\ell+1}$. The front $k$-face uses $v_0, \ldots, v_k$, and the back $\ell$-face uses $v_k, v_{k+1}, \ldots, \hat{v}_{k+j}, \ldots, v_{k+\ell+1}$. Therefore \begin{align*} (-1)^{k+j} (\phi \smile \psi)(\sigma \circ \delta_{k+j}) = (-1)^{k+j} \phi\!\left(\sigma|_{[v_0, \ldots, v_k]}\right) \cdot \psi\!\left(\sigma|_{[v_k, \ldots, \hat{v}_{k+j}, \ldots, v_{k+\ell+1}]}\right). \end{align*} Comparing with the second sum on the RHS: the $j$-th term of $(-1)^k \phi(\sigma|_{[v_0,\ldots,v_k]}) \cdot (-1)^j \psi(\sigma|_{[v_k,\ldots,\hat{v}_{k+j},\ldots,v_{k+\ell+1}]})$ equals $(-1)^{k+j}$ times the same product. These match for $1 \leq j \leq \ell+1$, but the RHS second sum also includes the $j = 0$ term. [/step]

[step:Show the boundary terms at $i = k+1$ and $j = 0$ cancel]The "extra" term from the first sum on the RHS (at $i = k+1$) is \begin{align*} (-1)^{k+1} \phi\!\left(\sigma|_{[v_0, \ldots, v_k]}\right) \cdot \psi\!\left(\sigma|_{[v_{k+1}, \ldots, v_{k+\ell+1}]}\right). \end{align*} The "extra" term from the second sum on the RHS (at $j = 0$) is \begin{align*} (-1)^k \phi\!\left(\sigma|_{[v_0, \ldots, v_k]}\right) \cdot (-1)^0 \psi\!\left(\sigma|_{[v_{k+1}, \ldots, v_{k+\ell+1}]}\right). \end{align*} The first expression carries sign $(-1)^{k+1}$ and the second carries sign $(-1)^k$. Their sum is \begin{align*} \bigl((-1)^{k+1} + (-1)^k\bigr) \phi\!\left(\sigma|_{[v_0, \ldots, v_k]}\right) \cdot \psi\!\left(\sigma|_{[v_{k+1}, \ldots, v_{k+\ell+1}]}\right) = 0, \end{align*} since $(-1)^{k+1} + (-1)^k = 0$. Therefore these two boundary terms cancel.[/step]

[guided]This cancellation is the crux of the Leibniz rule. The cup product splits a $(k+\ell)$-simplex at vertex $v_k$. When we take the coboundary of the cup product, we get contributions from omitting each vertex of the $(k+\ell+1)$-simplex. Vertices in positions $0$ through $k$ affect only the "front" (the $\phi$ factor), producing $(d\phi) \smile \psi$. Vertices in positions $k+1$ through $k+\ell+1$ affect only the "back" (the $\psi$ factor), producing $\phi \smile (d\psi)$. But there is an overlap at the shared vertex $v_{k+1}$ (from the front's perspective, omitting $v_{k+1}$ from $[v_0,\ldots,v_{k+1}]$) and at $v_k$ (from the back's perspective, omitting $v_k$ from $[v_k,\ldots,v_{k+\ell+1}]$). Both of these produce the same product $\phi(\sigma|_{[v_0,\ldots,v_k]}) \cdot \psi(\sigma|_{[v_{k+1},\ldots,v_{k+\ell+1}]})$ but with opposite signs $(-1)^{k+1}$ and $(-1)^k$. Their cancellation is what forces the sign $(-1)^k$ in the Leibniz rule to be exactly right.[/guided]

[step:Assemble the identity] Combining the matched terms: - The LHS terms for $0 \leq i \leq k$ match the first $k+1$ terms of $(d\phi) \smile \psi$ (indices $i = 0, \ldots, k$). - The LHS terms for $k+1 \leq i \leq k+\ell+1$ match the last $\ell+1$ terms of $(-1)^k \phi \smile (d\psi)$ (indices $j = 1, \ldots, \ell+1$). - The extra term at $i = k+1$ from $(d\phi) \smile \psi$ and the extra term at $j = 0$ from $(-1)^k \phi \smile (d\psi)$ cancel. Therefore \begin{align*} d(\phi \smile \psi)(\sigma) = ((d\phi) \smile \psi)(\sigma) + (-1)^k (\phi \smile (d\psi))(\sigma) \end{align*} for every singular $(k+\ell+1)$-simplex $\sigma$. Since this holds for all $\sigma$, we conclude \begin{align*} d(\phi \smile \psi) = (d\phi) \smile \psi + (-1)^k \phi \smile (d\psi) \end{align*} as cochains in $C^{k+\ell+1}(X; R)$. [/step]