Second cup-product square: δ¹csmile y-csmileδ⁰y is a level coboundary

Fix a commutative ring $k$, a group $G$ and a homomorphism $r : G \to \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, together with $k$-linear $G$-representations $M',M,M'',D'',D,D',N$. Assume given morphisms $i : M' \to M$ and $\pi : M \to M''$ with $\pi$ surjective on underlying modules and with $\pi(m)=0$ if and only if $m$ lies in the image of $i$; and morphisms $\pi_D : D'' \to D$, $i_D : D \to D'$ with $i_D$ surjective and $i_D(x)=0$ if and only if $x$ lies in the image of $\pi_D$. Assume given $k$-bilinear pairings $\varphi' : M' \times D' \to N$, $\varphi : M \times D \to N$ and $\varphi'' : M'' \times D'' \to N$, where $\varphi$ satisfies $\varphi(\rho_M(g)a,\rho_D(g)b) = \rho_N(g)\varphi(a,b)$ for all $g,a,b$, subject to the compatibilities $\varphi(i(m'),x)=\varphi'(m',i_D(x))$ and $\varphi(m,\pi_D(y))=\varphi''(\pi(m),y)$. Assume further that every $x \in D$ is fixed by all $\rho_D(s)$ with $r(s)$ in the fixing subgroup of some finite extension $F/\mathbb{Q}$ inside $\overline{\mathbb{Q}}$ (a smoothness condition on $D$ relative to $r$). Let $c$ be a $1$-cocycle of $M''$ satisfying IsLevelConstant₁ r, and let $y \in D'$ be $G$-invariant. Then the $2$-cochain $(s,t) \mapsto \varphi'\bigl(\mathtt{deltaCochain₁}\,i\,\pi\,c\,(s,t),\ \rho_{D'}(st)y\bigr) - \varphi''\bigl(c(s),\ \rho_{D''}(s)(\mathtt{deltaCochain₀}\,\pi_D\,i_D\,y\,(t))\bigr)$, the second term being cupCochain φ'' applied to $c$ and the connecting $1$-cochain of $y$, belongs to levelCoboundaries₂ r N.

This is the cochain-level anticommutation of the cup product with the two connecting maps in bidegrees $(2,0)$ and $(1,1)$: it expresses that $\langle \delta^1 c, y\rangle$ and $\langle c, \delta^0 y\rangle$ agree in the level-constant (continuous) $H^2$ of $N$, for a level-constant $1$-cocycle $c$ of $M''$ and a $G$-invariant $y \in D'$. It is used in the proof that the duality map $\theta$ attached to a short exact sequence is bijective (groupCohomology.bijective_theta_of_shortExact).