Cup product against connecting cochains is a level coboundary

Fix a commutative ring $k$, a group $G$ and a homomorphism $r \colon G \to \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ (the automorphism group of AlgebraicClosure ℚ over $\mathbb{Q}$), used only to speak of levels. Let $M', M, M'', D'', D, D', N$ be $k$-linear representations of $G$, with morphisms $i \colon M' \to M$ and $\pi \colon M \to M''$ such that $\pi$ is surjective on underlying modules and such that for every $m \in M$ one has $\pi(m) = 0$ if and only if $m$ lies in the image of $i$, and morphisms $\pi_D \colon D'' \to D$ and $i_D \colon D \to D'$ with $i_D$ surjective and $i_D(x) = 0$ if and only if $x$ lies in the image of $\pi_D$ (injectivity of $i$ and of $\pi_D$ is not assumed). Let $\varphi' \colon M' \otimes D' \to N$, $\varphi \colon M \otimes D \to N$, $\varphi'' \colon M'' \otimes D'' \to N$ be $k$-bilinear maps, with $\varphi$ equivariant in the sense that $\varphi(\rho_M(g)m, \rho_D(g)x) = \rho_N(g)\varphi(m,x)$ for all $g, m, x$, and compatible with the maps: $\varphi(i(m'), x) = \varphi'(m', i_D(x))$ and $\varphi(m, \pi_D(v)) = \varphi''(\pi(m), v)$. Let $c \in M''$ be $G$-invariant and let $y$ be a $1$-cocycle of $D'$ satisfying the level-constancy predicate IsLevelConstant₁ r. Then the $2$-cochain $(s,t) \mapsto \varphi'\bigl(\delta^0c(s), \rho_{D'}(s)(y(t))\bigr) + \varphi''\bigl(c, \delta^1y(s,t)\bigr)$, where $\delta^0 c =$ deltaCochain₀ i π hπ c and $\delta^1 y =$ deltaCochain₁ πD iD hiD y are the connecting cochains attached to the two sequences, belongs to levelCoboundaries₂ r N.

This is the cochain-level form of one of the two anticommutativity squares relating a cup-product pairing of a dual pair of extensions to the connecting homomorphisms of the associated long exact sequences: up to sign, $\langle \delta^0 c, y\rangle = -\langle c, \delta^1 y\rangle$ in the relevant degree-$2$ cohomology. It is used in the proof of groupCohomology.bijective_theta_of_shortExact.