Let $X$ be a locally convex space (topology induced by a family of seminorms $P$ which separates points) and $Y\subset X$ a closed subspace. Assume $x\in X\setminus Y$. Show that there exists a $f\in X^\ast$ such that $f|_Y=0$ and $f(x)=1$.
My attempt: $Z:= X/Y$ is also a LCS (closedness of $Y$ guarantees that $X/Y$ is Hausdorff) and then there exists a $g\in Z^*$ such that $g(x+Y) \neq 0$ (Here I use Hahn-Banach in the sense that the dual is separating points of a LCS). The quotient map $q: X \to X/Y$ is also continuous and therefore, normalizing $f:= g \circ q$ gives the desired functional.
Is this correct and is there a more direct proof? E.g. use Hahn-Banach with semi-norms and define an appropriate functional on $Y\oplus \text{span}(x)$. I tried this but could not achieve that the function $y+\lambda x \mapsto \lambda p(x)$ was dominated by the seminorm $p$.
I am also happy if someone could verify the proof or spot mistakes.
Your proof is correct, and in my opinion, that is the nicest proof of the assertion.
There is, however, one terminological glitch, you wrote "$X/Y$ separates points", but that should be "$X/Y$ is separated", or "$X/Y$ is Hausdorff". (The seminorms that separate points still controlled the muscle memory, I guess.) And maybe it would be better to say "normalize" before saying $f = g\circ q$ "will do the job". But that is pedantry.
We can use the Hahn-Banach theorem(s) of course also in different ways to prove it.
For example, since $x\notin Y$ and $Y$ is closed, there is a convex balanced neighbourhood $U$ of $0$ such that $(x+U)\cap Y = \varnothing$. Since $U$ is balanced, $x \notin Y + U$. The Minkowski functional $p$ of $Y+U$ is then a continuous seminorm on $X$, with $p(x) \geqslant 1$. Then the linear form $\lambda \colon \operatorname{span} \{x\} \to \mathbb{K}$ (where $\mathbb{K} \in \{\mathbb{R},\mathbb{C}\}$, whichever is the base field) given by $\alpha x\mapsto \alpha$ is dominated by $p$, and an extension $f$ of $\lambda$ to $X$ that is dominated by $p$ does the required. Domination by $p$ implies continuity, and since $p\lvert_Y \leqslant 1$ it follows that $p\lvert_Y \equiv 0$ and hence $f\lvert_Y \equiv 0$.