How does one formally show that two lambda functions are $\alpha$ equivalent?
By definition of substitution we have
$$x [x \leftarrow z] = z$$
therefore
$$\lambda z . x [x \leftarrow z] = \lambda z . z \tag{1}$$
because $\lambda$-abstraction is a congruence (it preserves equality). By the definition of $\alpha$-equality we have
$$\lambda x . x = \lambda z . x [x \leftarrow z] \tag{2}.$$
By transitivity of equality we get from (1) and (2) that
$$\lambda x . x = \lambda z . z$$
If you require more details than this, you should use a computer proof assistant to check the details.