The Stacks project

Okay, I feel this proof can be slightly upgraded. First, lemma 10.44.2 only works in characteristic $p$. Of course, the characteristic zero case is obvious, but why not just use 10.43.6 instead?

Now for the tricky part. The term universal homeomorphism is not yet defined, it only appears in definition 29.45.1 and in the context of schemes, despite its use in the title of section 10.46 (maybe that's a bit confusing, but this is not the main issue here).

It seems that throughout the Stacks Project, a great care is taken to not use the term universal homeomorphism for morphisms of rings. Instead, it is written in terms of morphisms on spectra (for instance in the proof of lemma 58.14.2), or with a sentence such as "induces a universal homeomorphism on spectra" (see for instance lemma 29.46.11).

So if we want to keep this consistency, I propose to first say that by lemma 10.45.4 (or by definition) $k^{perf}/k$ is purely inseparable, so we can apply lemma 10.46.10 to find that $k^{perf}\otimes_{k}K$ has a unique prime ideal.

If this is not nitpicking for you, then I would suggest to also edit the very few remaining cases of universal homeomorphisms of rings in the Stacks Project: tags 29.47.6, 37.24.7, 110.40 (twice) and maybe 29.46.8.

Thanks for these comments. I have made your suggested changes, see this commit.