Valuation Criterion for Proper Morphisms Let $Y$ a noetherian scheme and $f: X \to Y$ of finite type (so quasi compact and locally of finite type: here the definitions: https://stacks.math.columbia.edu/tag/01T0).
I want to know how to see that following valuation criterion holds:
$f$ is proper (so  separated, of finite type, and universally closed) if and only if in every diagram
$$
\require{AMScd}
\begin{CD}
Spec(F)  @>{a}  >> X   \\
@VViV  @VVfV   \\
Spec(R) @>{t}>> Y 
\end{CD}
$$
for every discrete valuation ring $R$ and $F = Frac(R)$ there exist $l:Spec(R) \to X$ such that $a = l \circ i$ and $t = f \circ l$ holds.
My attepts: I know that $Spec(R) = \{m_R, \eta\} = \{m_R\} \cup Spec(F)$.
Futhermore that because $f$ finite, locally $f$ induces integral ring extension, so the going-up therem for ring morphisms holds.
But I don't see how to use this informations to see the equivalence.
 A: Here is a precise statement for the valuative criteria you are interested in:
Theorem (Valuative criteria for noetherian schemes; see Hartshorne, Exer. II.4.11(b)). Let $f\colon X \to Y$ be a morphism of finite type of noetherian schemes. Consider the following diagram:
$$\require{AMScd}
\begin{CD}
  \operatorname{Spec}(K) @>>> X\\
  @ViVV @VVfV\\
  \operatorname{Spec}(R) @>>> Y
\end{CD}\label{eq:star}\tag{$*$}$$
where $R$ is a DVR, $K$ is the quotient field of $R$, and $i$ is the morphism induced by the inclusion $R \subseteq K$.


*

*The morphism $f$ is separated if and only if for every diagram of the form $\eqref{eq:star}$, there is at most one morphism $\operatorname{Spec}(R) \to X$ making the diagram commute.

*The morphism $f$ is proper if and only if for every diagram of the form $\eqref{eq:star}$, there exists a unique morphism $\operatorname{Spec}(R) \to X$ making the diagram commute.
The key commutative-algebraic input is the following:
Lemma (Hartshorne, Exer. II.4.11(a)). If $(\mathcal{O},\mathfrak{m})$ is a noetherian local domain with quotient field $K$, and if $L$ is a finitely generated field extension of $K$, then there exists a DVR $R$ of $L$ dominating $\mathcal{O}$.
Now to prove the Theorem, the direction $\Rightarrow$ follows from the usual valuative criteria [Hartshorne, Thms. II.4.3 and II.4.7], and the direction $\Leftarrow$ can be shown by replacing the applications of [Hartshorne, Thm. I.6.1A] in the proofs of [Hartshorne, Thms. II.4.3 and II.4.7] by the Lemma above.
I can give a thorough proof of this if you'd like, but while writing up the proof of the Lemma I realized that Hartshorne's sketch of the argument is fairly complete.
EDIT: As pointed out by Tibeku in the comments, there is something nontrivial that one must check in order to apply the Lemma for the valuative criterion for properness. Namely, one must prove that to check for universal closedness, it suffices to consider a base change $Y' \to Y$ that is of finite type. For this, see [Görtz–Wedhorn, Cor. 13.101] or [Stacks, Tags 05JX and 0205].
