Every finite game has a mixed Nash equilibrium

Every game with a finite set of players and finite, nonempty strategy sets has a Nash equilibrium of mixed strategies — Nash's 1951 theorem, stated as Theorem 1.8 of Algorithmic Game Theory, and the goal of this mission. Formally: for every finite family $(S_i)_{i \in \iota}$ of finite nonempty strategy types and every payoff assignment $u_i : \prod_j S_j \to \mathbb{R}$, there is a mixed profile $\sigma = (\sigma_i)_i$ — each $\sigma_i$ a lottery on $S_i$, players randomizing independently — such that for every player $i$ and every lottery $\tau$ on $S_i$,

where $U_i$ is the expected payoff under the product distribution.

A note on the hypotheses. Both finiteness assumptions are load-bearing, as §1.3.5 of the book stresses: with infinitely many players, or with infinite strategy sets (the pricing game, Example 1.9), equilibria can fail to exist. Nonemptiness of each $S_i$ is likewise necessary — an empty strategy set admits no lottery at all. The player set itself may be empty, in which case the empty profile is vacuously an equilibrium. Deviations range over all mixed strategies, not only pure ones; the equivalence of the two conditions is a lemma a solution will likely prove along the way.