The Stacks project

Proof. Choose a smooth surjective morphism $V \to \mathcal{U}$ whose source is a scheme, and let $v\in |V|$ be a point mapping to $u$. Then the composite $V \to \mathcal{U} \to \mathcal{X}$ is also smooth, and by Lemma 107.5.4 we have $\dim _ x(\mathcal{X}) = \dim _ v(V) - \dim _ v(V_ x),$ while $\dim _ u(\mathcal{U}) = \dim _ v(V) - \dim _ v(V_ u).$ Thus

Choose a representative $\mathop{\mathrm{Spec}}k \to \mathcal{X}$ of $x$ and choose a point $v' \in | V \times _{\mathcal{X}} \mathop{\mathrm{Spec}}k|$ lying over $v$, with image $u'$ in $|\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k|$; then by definition $\dim _ u(\mathcal{U}_ x) = \dim _{u'}(\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k),$ and $\dim _ v(V_ x) = \dim _{v'}(V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k).$

Now $V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k \to \mathcal{U}\times _{\mathcal{X}}\mathop{\mathrm{Spec}}k$ is a smooth surjective morphism (being the base-change of such a morphism) whose source is an algebraic space (since $V$ and $\mathop{\mathrm{Spec}}k$ are schemes, and $\mathcal{X}$ is an algebraic stack). Thus, again by definition, we have

Now $V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k \cong V\times _{\mathcal{U}} (\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k),$ and so Lemma 107.5.9 shows that $\dim _{v'}((V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k)_{u'}) = \dim _ v(V_ u).$ Putting everything together, we find that

as required. $\square$