Proof of Bellman optimality equation for finite Markov Decision Processes This question has already been posed in Cross Validated without receiving a correct formal answer, so I reformulate it here to gain attention of mathematicians. I am referring to chapter 3 of Sutton and barto book "Reinforcement learning. An introduction" available here: 
1
Let us assume that we have three finite sets, $S$ the set of states, $A$ the set of actions, and $R\subset \mathbb{R}$ the set of rewards.
Let $p : S \times R  \times S \times A \rightarrow [0,1]$ be a function such that
$$\sum_{s'\in S} \sum_{r \in R} p(s',r,s,a)=1$$ for each $s\in S, a \in a$, so that it defines a joint discrete probability distribution on $S\times R$ for every choice of  $s\in S, a \in a$, and we denote it then, with a slight abuse of notation, as $p(s',r|s,a)$. From a probabilistic point of view, we can think that if at time $t$ we are in state $S_t=s$ and we perform an action $A_t=a \in A$ then the probability of the two random variables $S_{t+1},R_{t+1}$ representing respectively next state and the reward obtained is given exactly by $p$:
$$\mathbb{P}\{S_{t+1}=s',R_{t+1}=r|S_{t}=s,A_t=a\} = p(s',r|s,a)$$
and so that, for example, given present state $s$ and action $a$,  the expected value of immediate reward is $r(s,a)=\sum_{r \in R} r\sum_{s'\in S}p(s',r|s,a)$, and the state transition probability (again with a slight abuse of notation) is $p(s'|s,a)=\sum_{r\in R}p(s',r|s,a)$.
Let us define $G_t$ as the random variable representing the sum of discounted future rewards obtainable from time $t$
$$G_t=\sum_{k=0}^{+\infty} \gamma^k R_{t+1+k}$$
that it is immediate to prove having this representation
$$G_t= R_{t+1}+\gamma G_{t+1}$$
We define a policy $\pi$ as a function $\pi: A \times S \rightarrow [0,1]$ such that for every $s \in S$ $\sum_{a \in A}\pi(a,s)=1$, so that it defines, for every choice of $s \in S$ a probability distribution over $A$, and we denote it with $\pi(a|s)$. We also define the state-value function $v_{\pi}$ for a policy $\pi$ as
$$v_{\pi}(s)=\mathbb{E}_{\pi}[G_t|S_t=s]$$
that is the expected value cof $G_t$ conditioned on being in state $S_t=s$ and using policy $\pi$ to select (randomly) actions at present time and also in future time steps, and analogously the action-value function $q_{\pi}$ as
$$q_{\pi}(s,a) = \mathbb{E}_{\pi}[G_t |S_t=s,A_t=a]$$.
It is quite simple to prove that these two functions satisfy these two mutual relations
\begin{equation}
v_{\pi}(s)=\sum_{a \in A} \pi(a|s)q_{\pi}(s,a)\label{eq1}\\
q_\pi(s,a)=\sum_{r \in R}r\sum_{s'\in S} p(s',r|s,a)+\gamma \sum_{s'\in S}v_{\pi}(s')\sum_{r\in R}p(s',r|s,a)
\end{equation}
and the two recursive Bellman equations
\begin{equation}
v_{\pi}(s)=\sum_{a\in A}\pi(a|s)\sum_{s'\in S, r\in R}p(s',r|s,a)[r+\gamma v_{\pi}(s')]\\
q_{\pi}(s,a)=\sum_{s'\in S, r\in R}p(s',r|s,a)\sum_{a' \in A}\pi(a'|s')[r+\gamma q_{\pi}(s',a')]
\end{equation}
A policy $\pi$ is said to be better of another one $\pi'$ if and only if $\pi(s) \geq \pi'(s)$ for all $s\in S$; an optimal policy $\pi_*$ is a policy that is better than all other ones, that is $v_{\pi_*}(s) \geq v_{\pi}(s)$ for each $s \in S$ and for each policy $\pi$.
Let us assume that there exists at least one optimal policy (this also should be proved, but let's skip it in this question). Then we can define the optimal state-value function 
$$v_*(s) \doteq \max_\pi v_{\pi}(s)$$ 
for each $s \in S$, and it is clear that, for each optimal policy $\pi_*$, we have $v_{\pi_*}(s)=v_*(s)$ for each $s \in S$. The same apply to the optimal action-value function
$$q_*(s,a) \doteq \max_{\pi} q_\pi(s,a)$$
that is for each optimal policy $\pi_*$ it is $q_{\pi_*}(s,a)=q_*(s,a)$.
Finally, here it is my question:
why is it true that $$v_*(s) = \max_{a \in A} q_*(s,a)$$ for each $s \in S$?
It is obvious that, given an optimal policy $\pi_*$, if for each $s \in S$ we take $a_s \in \text{arg}\,\max\limits_{a \in A}q_{\pi_*}(s,a)$, then we have
$$v_*(s)=v_{\pi_*}(s)=\sum_{a \in A} \pi_*(a|s)q_{\pi_*}(s,a)\leq \sum_{a \in A} \pi_*(a|s)q_{\pi_*}(s,a_s)=q_{\pi_*}(s,a_s)=q_*(s,a)$$
but I couldn't find a simple way to prove the reverse inequality, neither directly nor by contradiction.
Can anybody help?
 A: If I have read through the text correctly, I would say that indeed $v_{\pi}(s) \le \max_{a \in A} q_{\pi}(s,a)$ for all policies $\pi$, since $v_{\pi}(s) = \mathbb{E}_{a}[q_{\pi}(s,a)] $ and the expected value should be less or equal to the maximum value.
Now with respect to your question, if
$$
v_{\pi_*}(s) < \max_{a \in A} q_{\pi_*}(s,a) = q_{\pi_*}(s,a_s)
$$
then there should be an even better policy $\pi_*'(a|s) = [a=a_s]$ that would select $a_s$ deterministically when in state s, giving $v_{\pi_*}(s) < v_{\pi_*'}(s) = q_{\pi_*}(s,a_s)$ and contradicting the fact that $\pi_*$ is an optimal policy.
A: Since the characters allowed for comments are not enough to express my doubts about your answer, I write them here.
I agree with you that one possible way to answer to my question by contradiction is the one you have provided, and intuitively this idea works, but I still believe that it should be formalized correctly.
Let me be more precise: what you are writing is that if there exists $\bar{s} \in S$ such that $v_*(\bar{s}) < \max_{a \in A} q_*(\bar{s},a)$, then taking an optimal policy $\pi_*$ and $a_{\bar{s}} \in  \text{arg}\,\max\limits_{a \in A}q_*(\bar{s},a)$ we can define a policy $\pi_{\bar{s}}$ such that 
$$\pi_{\bar{s}}(a|s) = \begin{cases}
   \pi_*(a|s) \qquad \text{if} \qquad s\not= \bar{s}\\
    1 \qquad \text{if} \qquad s= \bar{s}, a=a_{\bar{s}}\\
    0 \qquad \text{otherwise}
\end{cases}
$$
Then it is clear that for that policy $v_{\pi_{\bar{s}}}(\bar{s})=q_{\pi_{\bar{s}}}(\bar{s},a_{\bar{s}})$, so that if we prove that $q_{\pi_{\bar{s}}}(\bar{s},a_{\bar{s}})=q_*(\bar{s},a_{\bar{s}})$ we are done since we get the contradiction  $v_{\pi_{\bar{s}}}(\bar{s}) > v_*(\bar{s})$.
But my doubt is then exactly this:
why is it true that  $q_{\pi_{\bar{s}}}(\bar{s},a_{\bar{s}})=q_*(\bar{s},a_{\bar{s}})$?
A: $\newcommand{\plcypmf}[2]{\pi(#1\,|\,#2)}$
$\newcommand{\condpmf}[2]{p(#1\,|\,#2)}$
$\newcommand{\condpmfsym}[3]{#1(#2\,|\,#3)}$
$\newcommand{\cp}[2]{P\{#1\:|\, #2\}}$
$\newcommand{\cpwrt}[3]{P_{#1}\{#2\:|\, #3\}}$
$\newcommand{\Ecwrt}[3]{E_{#1}[#2\:|\, #3]}$
$\newcommand{\argmax}[1]{\text{arg max}_{#1}\,}$
$\newcommand{\cases}[1]{\begin{cases}#1\end{cases}}$
$\newcommand{\mcalA}{\mathcal{A}}$
$\newcommand{\mcalR}{\mathcal{R}}$
$\newcommand{\mcalS}{\mathcal{S}}$
$\newcommand{\qd}{\quad}$
$\newcommand{\wR}{\mathbb{R}}$
$\newcommand{\Bop}{\Big(}$
$\newcommand{\Bcp}{\Big)}$
$\newcommand{\Prn}[1]{\Bop #1\Bcp}$
$\newcommand{\align}[1]{\begin{align*}#1\end{align*}}$
$\newcommand{\wes}{\blacksquare}$
Let $T$ be the time step variable and let $t$ be a particular time step. 
Given an agent, we define a policy $\pi$ to be the conditional PMF that that agent takes a particular action given a particular state. That is, $\condpmfsym{\pi}{a}{s}$ is the probability that that agent takes action $a$ given the state $s$. More explicitly, let $\Pi$ denote the set of all possible policies on $\mcalS$ and $\mcalA$ and, for a policy $\pi$, we define
$$
\condpmfsym{\pi}{a}{s}\equiv\cpwrt{\pi}{A_T=a}{S_T=s}\equiv\cp{A_T=a}{S_T=s,\Pi=\pi}\qd\text{for all time steps }T
$$
Notice that the conditional PMF $\condpmfsym{\pi}{a}{s}$ is constant relative to the time step variable $T$. Many authors use this definition and hence assume that each policy behaves the same at all time steps.
But it is often helpful to define a policy where the conditional PMF's vary with the time step variable $T$. Indeed, there is no mathematical or probabilistic reason that precludes us from defining a policy with a different PMF at each time step. And when we learn about optimal policies (below), we can easily imagine some optimal policies whose behavior differs between time steps.
Hence, more generally, we define a policy $\pi$ by a set of conditional PMF's
$$
\condpmfsym{\pi}{a}{s}
 \equiv \cases{\cpwrt{\pi_{0}}{A_{0}=a}{S_{0}=s}\\\cpwrt{\pi_{1}}{A_{1}=a}{S_{1}=s}\\\vdots\\\cpwrt{\pi_{t}}{A_{t}=a}{S_{t}=s}\\\cpwrt{\pi_{t+1}}{A_{t+1}=a}{S_{t+1}=s}\\\vdots}
$$
such that
$$
1=\sum_{a\in\mcalA(s)}\cpwrt{\pi_{T}}{A_T=a}{S_T=s}\qd\text{for all }s\in\mcalS\text{ and all }T=0,1,2,\dots
$$
We assume that the Markov Property holds:
$$\align{
&\condpmf{g_{t+1}}{s',a,s}=\condpmf{g_{t+1}}{s'} \\\\
&\condpmf{g_{t+1}}{s',r,a,s}=\condpmf{g_{t+1}}{s'}\tag{MDP.0} \\\\
&\condpmf{r_{t+2}}{s',a,s}=\condpmf{r_{t+2}}{s'} \\\\
}$$
Proposition MDP.5 Let $s_0\in\mcalS$, let $a_0\in\mcalA(s_0)$, and let $\pi$ be any policy on $\mcalS$. Define the policy $\phi_t$ on $\mcalS$ by
$$
\cpwrt{\phi_t}{A_T=a}{S_T=s}=\condpmfsym{\phi_t}{a}{s}\equiv\cases{\condpmfsym{\pi}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_0\\0&\text{else}}
$$
Then, for all $a\in\mcalA(s_0)$, we have
$$
q_{\phi_{t}}(s_0,a) = q_{\pi}(s_0,a) \\
$$
Proof If $g_{t+1}$ is a possible outcome of $G_{t+1}$, then $\condpmf{g_{t+1}}{s',\phi_t}=\condpmf{g_{t+1}}{s',\pi}$ since $\phi_t=\pi$ for $T=t+1,t+2,\dots$. Also note that, for all $a\in\mcalA(s_0)$, we have 
$$\condpmf{s'}{s_0,a,\phi_t}=\condpmf{s'}{s_0,a,\pi}$$
That is, if we know the state and action in the current time step, then the policy is irrelevant to determining the next state. Hence, for all $a\in\mcalA(s_0)$, we have
$$\align{
q_{\phi_t}(s_0,a) &= \Ecwrt{\phi}{G_t}{S_t=s_0,A_t=a} \\
 &= \Ecwrt{\phi_t}{R_{t+1}+\gamma G_{t+1}}{S_t=s_0,A_t=a} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a}+\Ecwrt{\phi_t}{\gamma G_{t+1}}{S_t=s_0,A_t=a} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\condpmf{g_{t+1}}{s_0,a,\phi_t} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',s_0,a,\phi_t}\cdot\condpmf{s'}{s_0,a,\phi_t} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',\phi_t}\cdot\condpmf{s'}{s_0,a,\phi_t}\tag{by MDP.0} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',\pi}\cdot\condpmf{s'}{s_0,a,\pi} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',s_0,a,\pi}\cdot\condpmf{s'}{s_0,a,\pi} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\condpmf{g_{t+1}}{s_0,a,\pi} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a}+\Ecwrt{\pi}{\gamma G_{t+1}}{S_t=s_0,A_t=a} \\
 &= \Ecwrt{\pi}{R_{t+1}+\gamma G_{t+1}}{S_t=s_0,A_t=a} \\
 &= \Ecwrt{\pi}{G_t}{S_t=s_0,A_t=a} \\
 &= q_{\pi}(s_0,a) \\
}$$
$\wes$
Define $v_{*}:\mcalS\mapsto\wR$ by
$$
v_{*}(s)\equiv\max_{\pi}v_{\pi}(s)\qd\text{for all }s\in\mcalS
$$
Define $q_{*}:\mcalS\times\mcalA\mapsto\wR$ by
$$
q_{*}(s,a)\equiv\max_{\pi}q_{\pi}(s,a)\qd\text{for all }s\in\mcalS,a\in\mcalA(s)
$$
Proposition MDP.7 For all $s\in\mcalS$, we have
$$
v_{*}(s) = \max_{a\in\mcalA(s)}q_{*}(s,a)
$$
Proof Let $s_0\in\mcalS$ and define $a_{*}\in\argmax{a\in\mcalA(s_0)}q_{*}(s_0,a)$. Then for any policy $\pi$, we have
$$\align{
v_{\pi}(s_0) &= \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{\pi}(s_0,a) \\
 &\leq \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{*}(s_0,a) \\
 &\leq \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{*}(s_0,a_{*}) \\
 &= q_{*}(s_0,a_{*})\cdot\sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0} \\
 &= q_{*}(s_0,a_{*}) \\
 &= \max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
}$$
Since this is true for all policies $\pi$, then it must be that
$$
v_{*}(s_0)=\max_{\pi}v_{\pi}(s_0)\leq\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$
Suppose, by way of contradiction, that we have strict inequality:
$$
v_{*}(s_0)\lt\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
\tag{MDP.7.1}
$$
Define the policy $\pi_{**}$ by
$$
\pi_{**}\in\argmax{\pi}q_{\pi}(s_0,a_{*})
$$
Then
$$
q_{\pi_{**}}(s_0,a_{*}) = \max_{\pi}q_{\pi}(s_0,a_{*}) = q_{*}(s_0,a_{*}) = \max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$
Also define the policy $\phi_t$ by
$$
\cpwrt{\phi_t}{A_T=a}{S_T=s}=\condpmfsym{\phi_t}{a}{s}\equiv\cases{\condpmfsym{\pi_{**}}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_{*}\\0&\text{else}}
$$
Then MDP.5 gives the third equality:
$$\align{
v_{\phi_t}(s_0) = \sum_{a\in\mcalA(s_0)}\condpmfsym{\phi_t}{a}{s_0}q_{\phi_t}(s_0,a) = q_{\phi_t}(s_0,a_{*})= q_{\pi_{**}}(s_0,a_{*}) = \max_{a\in\mcalA(s_0)}q_{*}(s_0,a) \gt v_{*}(s_0)
}$$
This contradicts the definition of $v_{*}(s_0)\equiv\max_{\pi}v_{\pi}(s_0)$. Hence assumption MDP.7.1 is false and we have
$$
v_{*}(s_0)=\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$
Since $s_0\in\mcalS$ was chosen arbitrarily, then this equality holds for all $s\in\mcalS$.
$\wes$
A: $\newcommand{\align}[1]{\begin{align*}#1\end{align*}}$I had just the same question while learning RL these few days. I think the derivation on pages 31 and 32 in slides from https://www.cs.cmu.edu/~mgormley/courses/10601-s17/slides/lecture26-ri.pdf kind of gives us an intuition why $v_{\pi^{*}}(s)=\max_{a\in A} q_{\pi^*}(s,a)$ for all $s\in S$. Though the slides consider the case where ${\pi}$ is deterministic, it can be applied to the stochastic case $\pi(a|s)$. If there is any mistake below, please point it out.
If $\exists{s'}\in{S}$ such that a value function $v_\pi(s')< \max_{a\in A} q_\pi(s',a)$ then we can define a new policy
$$
{\pi'}\equiv\begin{cases}
1&if \space s=s' and \space a=\arg \max_{a\in A} q_\pi(s',a)\\
0&if \space s=s' and\space a\neq\arg \max_{a\in A} q_\pi(s',a)\\
{\pi}&if\space s \in S/\{s'\}
\end{cases}\tag{1}
$$
We break any tie in $\arg\max$ arbitrarily. Now we want to prove that $\pi'$ is a better policy than $\pi$ by using a recursive method similar to the one in the above slides.
define a notation 
$$
{\pi_{t}'}\equiv\begin{cases}
1&if \space s=s' and\space a=\arg \max_{a\in A} q_\pi(s',a)\space and\space T\leq t\\
0&if\space s=s' and\space a\neq\arg \max_{a\in A} q_\pi(s',a)\space and\space  T\leq t\\
{\pi}&else
\end{cases}\tag{2}
$$
for s', the value function for $\pi$,  
$$v_{\pi}(s') <v_{\pi_{0}'}(s')\leq v_{\pi_{1}'}(s')\leq v_{\pi_{2}'}(s') \leq ...\leq v_{\pi_{\infty}'}(s')\tag{3}$$
for $s\in{S/\{s'\}}$, the value function for $\pi$,  
$$v_{\pi}(s) \leq v_{\pi_{0}'}(s)\leq v_{\pi_{1}'}(s)\leq v_{\pi_{2}'}(s) \leq ...\leq v_{\pi_{\infty}'}(s)\tag{4}$$
the above inequality is true because we are simply replacing $v_{\pi}(s')$ with a bigger $\max_{a\in A} q_{\pi}(s',a)$ when calculating the value functions in (3) and (4). 
For example, ${Let}\space { a' }=\arg \max_{a\in A} q_\pi(s',a)$.
For $s_0=s'$,
$$\align{v_{\pi}(s_0) &< \max_{a\in A} q_\pi(s',a)\\&=v_{\pi_0'}(s')\\&= q_\pi(s',a')\\&=E_{s_1\in S}[r(s',a',s_1)+ \lambda v_{\pi}(s_1)]\\&=E_{s_1\in S}[r(s',a',s_1)+ \lambda E_{a_1\in A}[q_\pi(s_1,a_1)]]\\&=E_{s_1\in S/\{s'\}}[r(s',a',s_1)+ \lambda E_{a_1\in A}[q_\pi(s_1,a_1)]]+E_{s'}[r(s',a',s')+\lambda E_{a_1\in A}[q_\pi(s',a_1)]]\\&\leq E_{s_1\in S/\{s'\}}[r(s',a',s_1)+ \lambda E_{a_1\in A}[q_\pi(s_1,a_1)]]+E_{s'}[r(s',a',s')+\lambda \max_{a\in A}q_\pi(s',a)]\\&=v_{\pi_1'}(s')}\tag{5}$$ 
For $s_0\in$ S/{s'},
$$\align{v_{\pi}(s_0) &= E_{a_0\in A}[q_\pi(s_0,a_0)]\\&=v_{\pi_0'}(s_0)\\&=E_{a_0\in A}[E_{s_1\in S}[r(s_0,a_0,s_1)+ \lambda v_{\pi}(s_1)]]\\&=E_{a_0\in A}[E_{s_1\in S}[r(s_0,a_0,s_1)+ \lambda E_{a_1\in A}[q_\pi(s_1,a_1)]]]\\&=E_{a_0\in A}[E_{s_1\in S/\{s'\}}[r(s_0,a_0,s_1)+ \lambda E_{a_1\in A}[q_\pi(s_1,a_1)]]]+E_{a_0\in A}[E_{s'}[r(s_0,a_0,s')+ \lambda E_{a_1\in A}[q_\pi(s',a_1)]]]\\&\leq E_{a_0\in A}[E_{s_1\in S/\{s'\}}[r(s_0,a_0,s_1)+ \lambda E_{a_1\in A}[q_\pi(s_1,a_1)]]]+E_{a_0\in A}[E_{s'}[r(s_0,a_0,s')+ \lambda \max_{a\in A}q_\pi(s',a)]]\\&=v_{\pi_1'}(s_0)}\tag{6}$$
Note the difference between the strictly less than symbol and the less than symbol in (5) and (6). This is because the probability to replace $v_{\pi}(s')$ with a bigger $\max_{a\in A} q_{\pi}(s',a)$ might be zero.
We can approximate $v_{\pi_{\infty}'}(s)$ naively, pretty much as what we do in (5) and (6), by expanding the equation to t=t' that is big enough that the remainder would be negligible w.r.t our strictly less than inequality, that is $v_{\pi_{\infty}'}^{approx}(s') > v_{\pi}(s')$, and $v_{\pi_{\infty}'}^{approx}(s) > v_{\pi}(s)$ for $s\in S/\{s'\}$ if $v_{\pi_{\infty}'}(s) > v_{\pi}(s)$, and we let $v_{\pi_{\infty}'}^{approx}(s) = v_{\pi}(s)$ for the rest. And because $v_{\pi'}(s) \geq v_{\pi_{\infty}'}^{approx}(s)$ is also true for all $s\in S$. We get that $v_{\pi'}(s) >v_{\pi}(s)$ for $s\in S$ if $v_{\pi_{\infty}'}(s) > v_{\pi}(s)$, and $v_{\pi'}(s) \geq v_{\pi}(s)$ for the others. Thus, $\pi'$ is indeed a strictly better policy than $\pi$. 
The above derivation is true for all policy $\pi$, thus it is also true for an optimal policy $\pi^*$ if it exists.
So, together with $v_{\pi^*}(s) \leq \max_{a\in A}q_{\pi^*}(s,a)$ for all $s\in S$ and the proof by contradiction provided by other answers. We can conclude that if there exists an optimal policy $\pi^*$, then $v_{\pi^{*}}(s)=\max_{a\in A} q_{\pi^*}(s,a)$ for all $s\in S$.
We can also get other properties from this proof:(1) a very similar proof, slight modification is probably required, would shows that we only need to take into account deterministic policies, that is, for any stochastic policy we can always find a deterministic policy that is at least as good as the stochastic policy. (2)Another interesting consequence results from this proof is that if a policy $\pi$ satisfy $v_{\pi}(s)=\max_{a\in A} q_{\pi}(s,a)$ for all $s\in S$ then we can say that it is an optimal policy because we can prove that all other policies are only as good if there are multiple optimal policies, or worse than the policy $\pi$ by showing $\pi$ is better than all other policies using the same proof but replacing all bigger than operators with smaller than operators. (3)We can also show the existence of an optimal policy in finite MDP by the above proof. Because we only need to take into account deterministic policies and they are finite, we can continuously updating our policy using the above proof. Before we go over all possibilities, we would come upon a policy $\pi$ that satisfies $v_{\pi}(s)=\max_{a\in A} q_{\pi}(s,a)$ for all $s\in S$ because a policy cannot show up twice while we are updating our policy or it will be strictly better and strictly worse than policies in between at the same time.
A: I also had a hard time understanding the complete chain of arguments sourounding the bellmann optimality equations, but i think i found the subtle missing part, maybe it is exactly what your were looking for:
What can be proven based on previous answers in this thread is the following: if $\pi$ is a policy and there exists $a^*,s^*$ with
$$q_{\pi}(s^*,a^*)\geq v_{\pi}(s^*)$$
than you can define the modified policy
$$\tilde \pi(a|s) = 1(s^*=s)1(a=a^*) + 1(s^*\neq s)\pi(a|s)$$
which then satisfies
$$v_{\tilde \pi}(s) \geq v_{\pi}(s)~~\text{for all}~s.$$
But the proof also shows: in particular for $s=s^*$ it holds that
$$v_{\tilde \pi}(s^*) \geq q_{\pi}(s^*,a^*)\geq v_{\pi}(s^*)~~!!$$
Now we consider $v^*(s)=\max_{\pi\in\Pi}v_{\pi}(s)$ and $q^*(s,a)=\max_{\pi\in\Pi}q_{\pi}(s,a)$. The inequality $v^*(s)\leq \max_{a}q^*(s,a)$ for all $s$ is easy. Now for the reverse argument: Suppose by contradiction that there exists some $s^*$ such that
$$\max_{a}q^*(s^*,a) > v^*(s^*).$$
By definition there exist some policy $\pi'$ and some $a^*$ such that
$$q_{\pi'}(s^*,a^*) = \max_a q^*(s^*,a).$$
Because $v^*$ is the maximum over all $\pi$, in particular one get the inequality for $\pi=\pi'$ that is
$$q_{\pi'}(s^*,a^*) > v_{\pi'}(s^*).$$
So now one can apply the previously mentioned statement and obtain a policy $\tilde \pi$ (modifikation of $\pi'$) such that
$$v_{\tilde\pi}(s^*)\geq q_{\pi'}(s^*,a^*) > v_{\pi'}(s^*).$$
But because $q_{\pi'}(s^*,a^*)$ is strictly larger then $v_{\pi}(s^*)$ for any $\pi$, one gets the contradiction
$$v_{\tilde\pi}(s^*) > v_{\tilde\pi}(s^*)$$
and finally the desired
$$v^*(s) = \max_a q^*(s,a).$$
Hope that helped!
