Leibniz rule for the cup product of inhomogeneous cochains

Let $k$ be a commutative ring, $G$ a group, and $A,B$ two $k$-linear representations of $G$ (objects of Rep k G), all in a single universe. Fix natural numbers $p,q$, an $A$-valued inhomogeneous $p$-cochain $f : G^p \to A$, a $B$-valued inhomogeneous $q$-cochain $g : G^q \to B$, and a tuple $\sigma : G^{p+q+1}$. Here $\mathrm{cochainCup}\,A\,B\,p\,q$ is the $k$-bilinear map sending $(f,g)$ to the $(A\otimes B)$-valued $(p+q)$-cochain whose value at $\tau \in G^{p+q}$ is $f(\tau \circ \mathrm{castAdd}) \otimes_k \rho_B\big(\tau_0\cdots\tau_{p-1}\big)\,g(\tau \circ \mathrm{natAdd})$, the first argument being the initial $p$ entries of $\tau$, the second the final $q$ entries, and the twisting element being Fin.partialProd of the initial segment evaluated at Fin.last p. The assertion is the pointwise identity, at the given $\sigma$, between the value of Mathlib's inhomogeneous differential $d^{p+q}$ on $f \cup g$ and the sum of two terms: the cochain $(d^p f) \cup g$ on $G^{(p+1)+q}$, evaluated at $\sigma$ precomposed with the reindexing Fin.cast coming from $(p+1)+q = p+q+1$, plus $(-1)^p$ times the value at $\sigma$ of $f \cup (d^q g)$, a cochain on $G^{p+(q+1)}$.

This is the Leibniz rule $d(f \cup g) = df \cup g + (-1)^p f \cup dg$ for the cup product on inhomogeneous cochains, stated pointwise at a tuple of group elements; the explicit Fin.cast records that $(p+1)+q = p+q+1$ is not a definitional identity in Lean, whereas $p+(q+1) = p+q+1$ is. It is the computational input for all cohomology-level properties of the cup product in this development, including the existence of a graded cup product, its compatibility with connecting homomorphisms, and the Tate-cohomology extension.