Generic smoothness on the source

The field $k$ is perfect by [F8]. By [F2] the varieties $X$ and $Y$ are integral finite-type $k$-schemes with $f$ a $k$-morphism; the regular loci $X_{\mathrm{r}\mathrm{e}\mathrm{g}},Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$ are defined by [F4], and by [F3] the set $U=X_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap f^{-1}(Y_{\mathrm{r}\mathrm{e}\mathrm{g}})\cap D(H)$ is a nonempty open subset of $X$ contained in $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ with $f(U)\subseteq Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$, and $d_{x}f\text{\hspace{0.17em}⁣}:T_{x}X\to T_{f(x)}Y$ is surjective at every closed point $x\in U$. We keep these notations throughout.

Affine pieces. By [F11] the variety $X$ has a finite affine cover; choose a chart $X_0$ with $U\cap X_0\mathrm{\ne }\mathrm{\varnothing }$ and a point $x_0\in U\cap X_0$. Since principal opens form a basis of the topology [F10], there is $0\mathrm{\ne }h\in k[X_0]$ with $x_0\in D_{X_0}(h)\subseteq U\cap X_0$. Similarly $y_0=f(x_0)\in f(U)\subseteq Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$; choose an affine chart $Y_0$ of $Y$ with $y_0\in Y_0$ [F11] and $0\mathrm{\ne }g\in k[Y_0]$ with $y_0\in D_{Y_0}(g)\subseteq Y_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap Y_0$ [F10]. The set $D_{X_0}(h)\cap f^{-1}(D_{Y_0}(g))$ is a nonempty open subset of the affine variety $X_0$ containing $x_0$, so by [F10] there is $0\mathrm{\ne }{h}^{\mathrm{\prime }}\in k[X_0]$ with $x_0\in D_{X_0}(h^{\mathrm{\prime }})\subseteq D_{X_0}(h)\cap f^{-1}(D_{Y_0}(g))$. Put $V:=D_{X_0}(h^{\mathrm{\prime }})$ and $W:=D_{Y_0}(g)$, so that $V$ is a nonempty open subvariety of $X$ with $V\subseteq D_{X_0}(h)\subseteq U$, and $f(V)\subseteq W\subseteq Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$. By [F13] the principal opens $V$ and $W$ are affine varieties with coordinate rings $k[V]=k[X_0{]}_{h^{\mathrm{\prime }}}$ and $k[W]=k[Y_0{]}_g$. Since $X_0$ and $Y_0$ are nonempty open subsets of the irreducible varieties $X$ and $Y$, all four are irreducible [F12].

Points of $V$ and finite generation. By [F14] the coordinate ring $k[X_0]$ is reduced and generated over $k$ by finitely many coordinate classes; hence so is its localization $k[V]=k[X_0{]}_{h^{\mathrm{\prime }}}$, generated by those classes together with the inverse of $h^{\mathrm{\prime }}$ [F23]. So $V=\mathrm{Spec}k[V]$ is a finite-type $k$-scheme, and likewise $W=\mathrm{Spec}k[W]$. By [F13] and [F15] the points of the affine variety $V$ are the maximal ideals of $k[V]$, and by [F16] these are exactly the closed points of the scheme $V$; under the equivalence [F2] they are the classical points of $V$, hence closed points of the scheme $X$ lying in $V\subseteq U$. In particular every point $x$ of the classical variety $V$ is a closed point of $X$ and satisfies the conclusion of [F3], and its image $f(x)$ lies in $W$.

The varieties $V$ and $W$ are smooth over $k$. Let $z\in V$. Since $V\subseteq U\subseteq X_{\mathrm{r}\mathrm{e}\mathrm{g}}$, the open subscheme description [F5] and the cofinality of the neighbourhoods inside $V$ [F6] give ${\mathcal{O}}_{V,z}\cong {\mathcal{O}}_{X,z}$, which is regular because $z\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ [F4, F7]. Hence the finite-type $k$-scheme $V$ is regular, and $V\to \mathrm{Spec}k$ is smooth by [F9]. The same argument with $W\subseteq Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$ gives ${\mathcal{O}}_{W,z}\cong {\mathcal{O}}_{Y,z}$ regular for $z\in W$, and $W\to \mathrm{Spec}k$ smooth by [F9]. Each of $V$ and $W$ is a classical algebraic variety in the sense of [F10]: as an affine model it is a quasi-compact locally ringed space covered by itself, and it is separated because for regular maps $\phi ,\psi \text{\hspace{0.17em}⁣}:Z\to V$ from any classical prevariety $Z$ the coordinate components ${\phi }_i,{\psi }_i$ are regular functions on $Z$ (pullback of the coordinate functions of the affine model), so the equalizer is the finite intersection of the closed zero loci $\{{\phi }_i-{\psi }_i=0\}$ [F10]. In particular $V$ and $W$ are smooth classical varieties over $k$ in the sense of [F10] and [F20].

The restriction is finite type. Write $g=f{\mathrm{\mid }}_V:V\to W$. Let $\iota \text{\hspace{0.17em}⁣}:V\hookrightarrow X$ and $\kappa \text{\hspace{0.17em}⁣}:W\hookrightarrow Y$ be the open immersions, so that $\kappa \circ (f{\mathrm{\mid }}_V)=f\circ \iota$. Write $B=k[V]$ and $C=k[W]$, affine coordinate rings as in step 2.1, and let $\phi \text{\hspace{0.17em}⁣}:C\to B$ be the $k$-algebra map induced by $f{\mathrm{\mid }}_V\text{\hspace{0.17em}⁣}:V\to W$. Choose finitely many $k$-algebra generators $b_1,\dots ,b_m$ of $B$ [F23]. Since $k\subseteq C$ and $C[b_1,\dots ,b_m]$ is a $C$-subalgebra of $B$ containing $k$ and all $b_i$, it contains the $k$-subalgebra generated by the $b_i$, which is $B$; hence $B=C[b_1,\dots ,b_m]$ is generated by finitely many elements over $C$ [F23]. Thus $\phi$ is of finite type, the morphism $f{\mathrm{\mid }}_V$ is locally of finite type on the affine charts, and it is quasi-compact because its source is affine; by [F24] the restriction $f{\mathrm{\mid }}_V\text{\hspace{0.17em}⁣}:V\to W$ is of finite type.

Differential comparison. Let $x$ be a point of the classical variety $V$ and put $y=f(x)\in W$. By step 2.1, $x$ is a closed point of $X$ lying in $U$, so $d_{x}f$ is surjective [F3]; in particular the case $T_{f(x)}Y=0$ is allowed and the conclusion is unaffected. The identity $\kappa \circ (f{\mathrm{\mid }}_V)=f\circ \iota$ of step 3.2, the functoriality of the differential, and the fact that the $k$-open immersions $\iota ,\kappa$ induce isomorphisms on tangent spaces [F19] give $d_x(f{\mathrm{\mid }}_V)=(d_{g(x)}\kappa {)}^{-1}\circ d_{x}f\circ d_x\iota$, where $d_{g(x)}\kappa \text{\hspace{0.17em}⁣}:T_{g(x)}W\to T_{f(x)}Y$ is an isomorphism; the tangent spaces are finite-dimensional over $k$ [F22]. Therefore $\mathrm{rank}{d}_x(f{\mathrm{\mid }}_V)=\mathrm{rank}{d}_{x}f={\dim }_k{T}_{f(x)}Y={\dim }_k{T}_{g(x)}W$, and $d_x(f{\mathrm{\mid }}_V)\text{\hspace{0.17em}⁣}:T_{x}V\to T_{g(x)}W$ is surjective at every point $x$ of the classical variety $V$.

The criterion at every point of $V$. Let $x$ be a point of the classical variety $V$; by step 2.1 it is a classical closed point of the affine variety $V$. The structure morphisms $V\to \mathrm{Spec}k$ and $W\to \mathrm{Spec}k$ are smooth [3.1], so $V$ and $W$ are smooth classical varieties over $k$ in the sense of [F18]; the morphism $f{\mathrm{\mid }}_V\text{\hspace{0.17em}⁣}:V\to W$ is of finite type [3.2] and its differential at $x$ is surjective [4.1]. By the submersion criterion [F18], the restriction $f{\mathrm{\mid }}_V$ is smooth at $x$. As $x$ was an arbitrary point of the classical variety $V$, the restriction is smooth at every point of $V$ in the classical sense.

Upgrade to scheme points. Let $\mathrm{Sm}\subseteq V$ be the set of points at which $f{\mathrm{\mid }}_V$ is locally standard smooth, so that $\mathrm{Sm}$ contains every point of the classical variety $V$ by step 5.1. If $z\in \mathrm{Sm}$, then by [F20] there are affine neighbourhoods of $z$ and of $f{\mathrm{\mid }}_V(z)$ and a principal shrinking on which the induced ring map has a standard smooth presentation [F21]; the Jacobian minor of that presentation is a unit on the whole shrinking, hence remains a unit in every further localization, so the same presentation witnesses standard smoothness at every point of that shrinking. Therefore $\mathrm{Sm}$ is open in $V$. Suppose $V\setminus \mathrm{Sm}$ were nonempty. It is a nonempty closed subset of the affine finite-type $k$-scheme $V=\mathrm{Spec}B$ of step 2.1 and is a nonempty open subset of itself; by [F17] it contains a closed point $z$ of $\mathrm{Spec}B$. By [F16] the point $z$ is a maximal ideal of $B$, and by [F15] applied to the affine variety $V$ with coordinate ring $B$ [F13] it is a point of the classical variety $V$; this contradicts step 5.1. Hence $V\setminus \mathrm{Sm}=\mathrm{\varnothing }$, and $f{\mathrm{\mid }}_V\text{\hspace{0.17em}⁣}:V\to W$ is smooth in the sense of [F20].

Conclusion. The restriction $f{\mathrm{\mid }}_V\text{\hspace{0.17em}⁣}:V\to W$ is smooth [6.1], and $W$ is an open subscheme of $Y$ with $f(V)\subseteq W$. Since smoothness is local on the target [F20], the same standard smooth presentations witness smoothness of the restriction $f{\mathrm{\mid }}_V\text{\hspace{0.17em}⁣}:V\to Y$ at every point of $V$; the same applies to $V\to Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$ because $W\subseteq Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$. Thus $f$ is smooth at every point of the nonempty open subset $V$ of its source, with $V\subseteq U$ a principal open of an affine chart of $X$. Neither $X$ nor $Y$ is assumed smooth outside $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$, $Y_{\mathrm{r}\mathrm{e}\mathrm{g}}$, and no target-side generic smoothness is claimed here.

Boundary and scope dispositions. Empty: $X$ and $Y$ are nonempty because irreducible means nonempty [F12], so the charts $X_0,Y_0$ and the sets $U$, $V$, $W$ of steps 1.2 and 2.1 are nonempty; there is no empty-case convention to invoke, and the empty scheme is excluded by the hypothesis. Zero: relative dimension $0$ is allowed — if $\dim X=\dim Y$ the differential is an isomorphism at the points of $V$ and the conclusion is unaffected; if $Y$ is a point then $Y_{\mathrm{r}\mathrm{e}\mathrm{g}}=Y$, the chart $Y_0$ is the whole point, $W=Y_0$, and step 3.1 shows directly that $V\to W=\mathrm{Spec}k$ is smooth, so the criterion's conclusion in step 5.1 is consistent. One: nothing in the argument divides by a natural number or requires a generator count or relative dimension at least one; the lists $b_1,\dots ,b_m$ of step 3.2 may have any finite length, and the case ${\dim }_k{T}_{f(x)}Y=1$ is the first instance in which surjectivity of $d_{x}f$ is a genuine condition. Degenerate: neither $X$ nor $Y$ is assumed smooth, and $f$ is neither assumed finite nor flat; the set $V$ must be allowed to be a proper subset of $X$, as the example $t\mapsto t^2$ on ${\mathbb{A}}_k^1$ shows, where the differential vanishes at the origin and $V$ lies in $U={\mathbb{A}}_k^1\setminus \{0\}$; a differential of rank zero is compatible with $V\subseteq U$ exactly when the target tangent space is zero; in particular the structure map to $\mathrm{Spec}k$ has this property, and the case where $U$ is not affine is handled by passing to the principal open $V$ of a chart. Endpoints: the argument uses no closed-range or dimension endpoint claim; at one extreme $f$ may already be smooth on all of $X$, in which case the construction still returns some nonempty principal open $V$, and every such $V$ is dense in $X$ because $X$ is irreducible and $V$ is nonempty and open [F12]. Nonempty-choice: AC is declared in [F1] and is used exactly through the AC-assuming suppliers [F3] (generic differential surjectivity), [F18] (submersion criterion), [F9] (regularity versus smoothness), [F2] (classical-scheme dictionary), [F13] and [F15] (principal opens and the Nullstellensatz correspondence), [F17] (density of closed points), and [F12]/[F10] as used in steps 1.2 and 2.1; the finite choices of charts and principal open generators in step 1.2 and the localization argument of step 2.1 add no further choice principle. Biconditional directions: the corollary asserts only existence of $V$ and smoothness, with no converse; the only biconditional used as a supplier is the submersion criterion [F18], and step 5.1 applies its forward direction (surjective differential implies smooth at the point), never its reverse.