Proving that a Banach space is separable if its dual is separable

A normed space has the property (that all metric spaces have) that $X$ is separable then all subsets are separable too in their subspace topology. So $X^\ast$ (norm)-separable implies that $B_{X^\ast}$ is separable. The reverse also holds in all normed spaces $Y$ by "scaling": if $x \neq 0$ then choose $\alpha = \frac{1}{\|x_n\|}$ so that $\|\alpha x\| =1$. If we then (by separability of the unit ball) find a sequence $d_n$ on the ball $B_Y$ that converges to $\alpha x$, and also a sequence of rationals $q_n \to \frac{1}{\alpha}$. Then $q_n d_n \to \frac{1}{\alpha} (\alpha x) = x$. This essentially shows that if $D$ is countable and dense in $B_Y$ then $\{qd: q \in \mathbb{Q}, d \in D\}$ is (countable and) dense in $Y$. So $B_Y$ separable iff $Y$ separable. So we lose nothing by using the unit ball (here the sphere really). And the Hahn-Banach theorem which links things in $X$ to $X^\ast$, gives us functionals on $B_{X^\ast}$ anyway.

Using the unit sphere makes things easier, because you know the norm of all dense elements, namely 1, which allows for the choice of the $x_n$ (otherwise we'd need to scale there too which makes for a more messy proof). We have to prove something on $X$, so we can find points $x_n$ on which $f_n$ is relatively large: we know that $\|f_n\| = \sup \{|f_n(x)|: x \in B_X \}$, so we can find $x_n \in B_X$ such that $|f(x_n)|$ is as close to $1$ as we like. Here more than $\frac{1}{2}$ is sufficient.

As above a countable dense set in $B_X$ is enough to get one on $X$, using the span with rational coefficients. So try that for the $D = \{x_n: n \in \mathbb{N}\}$ we now have: taking finite sums from $D$ with rational coefficients we can approximate all members of the linear span of $D$ (just approximate real coefficients in $\mathbb{R}$ by members of $\mathbb{Q}$; we use that the field is separable). This $\operatorname{span}_{\mathbb{Q}}(D)$ is still countable (standard set theory argument: finite products of countable sets are countable and a union of countably many countable sets is countable). So $Y = \overline{\operatorname{span}(D)}$ has a countable dense set $\operatorname{span}_{\mathbb{Q}}(D)$. So we'd be done if $Y =X$. So assume it's not.

Then, Hahn-Banach allows us to find a functional $f$ (back to $B_{X^\ast}$ where we know something about the $f_n$) that has norm $1$ and is $0$ on $Y$. (In particular $f$ is such, that it is $0$ on the set $D$ where the $f_n$ are chosen to be large, and so the $f$ is very "different" from the $f_n$ and so we cannot approximate it in norm by the $f_n$.)

So we know $f(x_n) = 0$ (as $x_n \in Y$!) and the final part of the proof shows that if $f_n$ is chosen to be close to $f$, the point $x_n$ where $f_n$ is large shows that $f$ should also be at least $\frac{1}{4}$ in that point as well. This gives the needed contradiction.