Conway's proof of Goldstine's theorem. In proving Goldstine's theorem, Conway states the following. Suppose $B$ is the weak-star closure of $J(B_X)$ in $B_{X''}$, and assume there is some $x_0'' \in B_{X''}\smallsetminus B$. He claims Hahn-Banach implies there is some $x'\in X'$ and $\alpha,\varepsilon$ such that
$$\langle x',x\rangle  < \alpha<\alpha+\varepsilon < \langle x',x_0''\rangle$$
for every $x\in B$. He asks the reader to figure out why this is true.  Could someone explain? His version of Hahn Banach is the usual one. I'm aware of certain geometric versions. In this case, $B$ is convex and weak-star closed, so it is convex and closed, and $\{x_0''\}$ is of course convex and compact, so I can separate them by a norm closed hyperplane, but I want a weak-star closed hyperplane (that is, I get some functional $\psi\in X'''$ that defines the hyperplane, but I want something in $X'$, right?)
 A: Whatever versions of the Hahn-Banach theorems are presented in a book, what I've never seen left out is the extension lemma

Let $E$ be a real vector space, and $p \colon E \to \mathbb{R}$ a sublinear functional. If $M$ is a subspace of $E$, and $f\colon M \to \mathbb{R}$ a linear functional such that $f(x) \leqslant p(x)$ for all $x\in M$, then there exists a linear functional $F \colon E \to \mathbb{R}$ with $F\lvert_M = f$ and $F(x) \leqslant p(x)$ for all $x\in E$.

So I assume we can use that.
By definition, $B$ is $\sigma(X'',X')$-closed, and $x_0'' \notin B$. Since $\sigma(X'',X')$ is a vector space topology, there is a $\sigma(X'',X')$-neighbourhood $U$ of $0$ such that
$$B \cap (x_0'' + U + U) = \varnothing.\tag{1}$$
Rearranging $(1)$ yields $(B - U) \cap (x_0'' + U) = \varnothing$. Define $V := B - U$. Since $\sigma(X'',X')$ is locally convex, we can assume that $U$ is convex and balanced, and since $B$ is also convex and balanced, $V = B - U = B + U$ is then a convex and balanced $\sigma(X'',X')$-neighbourhood of $0$. In particular, $V$ is a convex and absorbant subset of $X''$. Its Minkowski functional
$$\mu_V \colon x \mapsto \inf \{ t > 0 : x \in t\cdot V\}$$
is then a sublinear functional on $X''$. Since $V$ is also balanced, $\mu_V$ is even a seminorm (but that plays no role, it's just an aside remark).
Now from $(x_0'' + U)\cap V = \varnothing$, it follows that $\mu_V(x_0'') > 1$. Let $M = \mathbb{R}\cdot x_0''$ and define $f\colon M \to \mathbb{R}$ by $f(\alpha \cdot x_0'') = \alpha\cdot \mu_V(x_0'')$.
By the lemma, there is a linear $F \colon X'' \to \mathbb{R}$ with $F(x_0'') = \mu_V(x_0'') > 1$ and $F(x'') \leqslant \mu_V(x'')$ for all $x'' \in X''$. Since clearly $\mu_V(x'') \leqslant 1$ for all $x'' \in V$, we can find $\alpha \in \bigl(1,\mu_V(x_0'')\bigr)$ and $\varepsilon > 0$ with
$$F(x'') \leqslant 1 < \alpha < \alpha + \varepsilon < \mu_V(x_0'') = F(x_0'').\tag{2}$$
In particular, we have $F(x) < \alpha$ for all $x\in B$.
It remains to see that $F$ is the evaluation functional for some $x'\in X'$. And that is equivalent to $F$ being $\sigma(X'',X')$-continuous. But by construction $F$ is bounded on some $\sigma(X'',X')$-neighbourhood of $0$ - namely $V$, or any smaller neighbourhood, like $U$ - and that implies $F$ is $\sigma(X'',X')$-continuous.

If Conway proves the separation theorem for locally convex spaces [the above is essentially a proof of that, a few details need to be generalised], we can simply invoke that for the space $(X'',\sigma(X'',X'))$, since by construction $B$ is a $\sigma(X'',X')$-closed convex set, and $\{x_0''\}$ is a $\sigma(X'',X')$-compact convex set disjoint from $B$.
