Trdeg-one essentially finite-type fields are finite over a simple transcendental adjunction

Let $K\subseteq E$ be a field extension that is essentially of finite type and of transcendence degree one. Then there exists an element $t\in E$, transcendental over $K$, such that $E$ is a finite-dimensional vector space over the simple transcendental extension $K(t)=K\langle t\rangle$.

This is the standard one-variable function-field presentation: a transcendence basis has cardinality one, the adjunction of that element is purely transcendental of degree one, and essential finite type upgrades algebraicity of $E/K(t)$ to finite dimensionality (Mathlib Algebra.finite_of_essFiniteType_of_isAlgebraic).