Suppose $X$ and $Z$ are standard normal random variables and define $$Y = X + Z.$$ Then $Y$ is also normal, has zero mean and its variance is two (Wikipedia). It should also be fair to assert that $Y|(X=x)$ has a normal distribution with unit variance and mean $x$.
I apply Bayes' Theorem and find $$ P_{X|Y}(x;y) = \frac{P_{Y|X}(y;x)P_X(x)}{P_Y(y)} = \frac{e^{-\frac{1}{4} (y-2 x)^2}}{\sqrt{\pi }}. $$
My intuition is that $X|(Y=y)$ would be normally distributed with mean $y$ and unit variance. After all, $X=Y - Z$. Where've I gone wrong?
After some thought, I can answer my own question. The key is using both definitions of $X$, which for clarity are $$ \begin{align} X &= Y - Z \\ X &= W, \end{align} $$ where $W$ is another standard normal random variable (this is just the original definition of $X$). Even given $Y=y$, the two equations are not inconsistent and simply give $$ X|(Y=y) = \frac{1}{2} \left( y - Z + W \right). $$ The result is a normal distribution with mean $y/2$ and a variance equal to $1/2$, which is also the result from Bayes' Theorem in my question. I wonder how you would approach a more complicated equation, say $$ \begin{align} Y &= f(X,Z) \\ X &= W, \end{align} $$ where you cannot solve for $X|(Y = y)$?