Kerodon

Proof. For $0 \leq i \leq n+1$, choose an element $\sigma _{i} \in \Sigma $ satisfying $[ \sigma _ i ] = \eta _ i$. Since $\vec{\eta }$ bounds, we can choose an $(n+1)$-simplex $\overline{\sigma }$ of $X$ satisfying $\sigma _ i = d^{n+1}_ i( \overline{\sigma } )$ for $0 \leq i \leq n+1$. Choose $\tau \in \Sigma $ satisfying $[\tau ] = \alpha $. Since $X$ is a Kan complex, we can choose $(n+1)$-simplices $\rho , \rho ': \Delta ^{n+1} \rightarrow X$ satisfying the identities

The definition of $m_ i$ supplies identities $m_{i}( \alpha , \eta _{i-1} ) = [ d^{n+1}_ i(\rho ) ]$ and $m_ i( \alpha , \eta _ i ) = [ d^{n+1}_ i(\rho ')]$. The tuple $( s^{n}_{i}(\sigma _0), \ldots , s^{n}_{i}( \sigma _{i-2}), \rho , \rho ', \bullet , \overline{\sigma }, s^{n}_{i+1}(\sigma _{i+2}), \ldots , s^{n}_{i+1}( \sigma _{n+1} ) )$ therefore determines a map of simplicial sets $\Lambda ^{n+2}_{i+1} \rightarrow X$ (Proposition 1.2.4.7). Since $X$ is a Kan complex, this map can be extended to an $(n+2)$-simplex of $X$. Let $\overline{\sigma }'$ denote the $(i+1)$st face of this simplex. By construction, we have

so that $\overline{\sigma }'$ witnesses that the tuple $( \eta _0, \ldots , \eta _{i-2}, m_ i( \alpha , \eta _{i-1}), m_ i( \alpha , \eta _{i} ), \eta _{i+1}, \ldots , \eta _{n+1} )$ bounds. $\square$