The Stacks project

Proof. If $f$ is proper, then $g$ is a formal modification by Lemma 88.24.3. Assume $g$ is a formal modification. By Lemmas 88.28.1 and 88.28.3 we see that $f$ is quasi-compact and separated.

By Cohomology of Spaces, Lemma 69.19.2 and Remark 69.19.3 it suffices to show that given any commutative diagram

where $R$ is a complete discrete valuation ring with fraction field $K$, there is a dotted arrow making the diagram commute. There are three cases: Case I: $p(\mathop{\mathrm{Spec}}(R)) \subset U$. This case is trivial because $U' \to U$ is an isomorphism. Case II: $p$ maps $\mathop{\mathrm{Spec}}(R)$ into $T$. This case follows from our assumption that $g : W \to X_{/T}$ is proper. Namely, if $Z$ denotes the reduced induced closed subspace structure on $T$, then $p$ factors through $Z$ and

is proper by assumption which implies we get the lifting property by Cohomology of Spaces, Lemma 69.19.2 applied to the displayed arrow. Case III: $p(\mathop{\mathrm{Spec}}(K))$ is not in $T$ but $p$ maps the closed point of $\mathop{\mathrm{Spec}}(R)$ into $T$. In this case the corresponding morphism

is an adic morphism (by Formal Spaces, Lemma 87.14.4 and Definition 87.23.2). Hence our assumption that $g : W \to X_{/T}$ be rig-surjective implies we can lift $g_{/T}$ to a morphism $\text{Spf}(R') \to W = X'_{/T}$ for some extension of complete discrete valuation rings $R \subset R'$. Algebraizing the composition $\text{Spf}(R') \to X'$ using Formal Spaces, Lemma 87.33.3 we find a morphism $\mathop{\mathrm{Spec}}(R') \to X'$ lifting $p$ as desired. $\square$