Cup product with the coboundary of a level-fixed vector

Let $k$ be a commutative ring, $G$ a group, and $r\colon G \to \mathrm{Aut}_{\mathbb Q}(\overline{\mathbb Q})$ a monoid homomorphism into the $\mathbb Q$-algebra automorphisms of the algebraic closure of $\mathbb Q$. Let $A$, $B$, $N$ be $k$-linear representations of $G$ and let $\varphi\colon A \to B \to N$ be $k$-bilinear and equivariant in the sense of Rep.IsEquivariantBilinear, i.e. $\varphi(\rho_A(s)a, \rho_B(s)b) = \rho_N(s)\varphi(a,b)$ for all $s \in G$, $a \in A$, $b \in B$. Let $f$ be a $1$-cocycle of $A$ satisfying the level-constancy predicate IsLevelConstant₁ r, and let $g$ be a $1$-cocycle of $B$. Assume there is a vector $b \in B$ and a finite-dimensional intermediate field $F$ of $\overline{\mathbb Q}/\mathbb Q$ such that $\rho_B(s)b = b$ whenever $r(s)$ lies in the fixing subgroup of $F$, and assume $g(s) = \rho_B(s)b - b$ for all $s$. Then the $2$-cochain underlying the cup product cup φ hφ f g, namely $(s,t) \mapsto \varphi\bigl(f(s), \rho_B(s)g(t)\bigr)$, lies in levelCoboundaries₂ r N: it is the coboundary, under d₁₂, of a $1$-cochain that is itself level-constant with respect to $r$.

This is the right-hand half of the verification that the explicit cup product on $1$-cochains descends to level-constant (continuous) cohomology, the coboundary directions in the two arguments being treated separately. It is used in the construction carried out by groupCohomology.exists_theta1.