The prefix differential at the first unit position

Let $M$ be a unital C*-algebra and $h$ a cochain of degree $n+1$, with $r<n+1$. For a cochain $h$ of degree $n+1$ and $r\in\mathbb N$, the prefix differential is $d_rh=h^{\mathrm{left}}+\sum_{j\le n,\ j<r}(-1)^{j+1}h^{\mathrm{mid}}_j$ (prefixDifferential h r), where $h^{\mathrm{left}}(v_0,\dots)=v_0h(v_1,\dots)$ and $h^{\mathrm{mid}}_j$ multiplies the inputs $v_j,v_{j+1}$. The cochain $h$ vanishes on units before $r$ (UnitZeroBefore h r) when $h(\dots,1,\dots)=0$ whenever the $1$ is inserted at a position $i<r$. If $h$ vanishes on units before $r$, then inserting $1$ at position $r$ gives

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.