Let $\hat{\land}, \hat{\lor}$ be binary operators denoting the infimum and supremum of two elements in a poset. I was given the following problem.
For a distributive lattice $\langle ~L, ~\hat{\lor}~, ~\hat{\land}~ \rangle$, show that if $x ~\hat{\land}~ a = y ~\hat{\land}~ a$ and $x ~\hat{\lor}~ a = y ~\hat{\lor}~ a$, then $x = y$.
My solution derives from two properties that I do not prove here and can be axiomatically accepted. First, $n \leq n ~\hat{\lor}~ m$. Secondly, that $n \leq m \implies n =n ~\hat{\land}~m$. Both properties hold for any $(n, m)$ pair in a poset $L$.
Now let us assume that $x ~\hat{\land}~ a = y ~\hat{\land} ~a$. Then, from the aforementioned properties, we have
\begin{align*} &x \leq x ~\hat{\lor}~ a \\ \Rightarrow & x = x ~\hat{\land}~ (x ~\hat{\lor}~ a) \\ &= (x ~\hat{\land}~ x) ~\hat{\lor}~ (x ~\hat{\land}~ a) \\ &= x ~\hat{\lor}~ (x ~\hat{\land}~ a) \\ &= x ~\hat{\lor}~ (y ~\hat{\land}~ a) ~ \text{{Assumption}}\\ &= (x ~\hat{\lor}~ y) ~\hat{\land}~ (x ~\hat{\lor}~ a) .\end{align*}
Using the exact same reasoning, $y = (y ~\hat{\lor}~ x) ~\hat{\land}~ (x ~\hat{\lor}~ a)$. Then $x = y$.
The reason I am unsure of this procedure is that I only made use of one of the preconditions stated in the problem. It seems superflous to assume $x ~\hat{\lor} ~ a = y ~\hat{\lor}~ a$ and it appears that the implication follows solely from assuming $x ~\hat{\land}~ a = y ~\hat{\land} ~a$.
I hinted in comments how to repair your proof, actually needing the two assumptions.
Here is a shorter one, close to yours and dual of that in Distributive lattice on nLab (Proposition 2.3):
$$\begin{align*} &x \le x ~\hat{\lor}~ a \\ \Rightarrow & x = x ~\hat{\land}~ (x ~\hat{\lor}~ a) \\ &= x ~\hat{\land}~ (y ~\hat{\lor}~ a) ~ \text{{Second assumption}}\\ &= (x ~\hat{\land}~ y) ~\hat{\lor}~ (x ~\hat{\land}~ a) .\end{align*} $$
Using the exact same reasoning, $y= (y~\hat{\land}~x) ~\hat{\lor}~ (y~\hat{\land}~ a).$ Therefore (by the first assumption) $x=y.$
Note that the proposition on nLab also sates the converse, i.e. any lattice satisfying this "cancellation law" is distributive.