Depth is additive for a flat local homomorphism

Write $d=\mathrm{depth}(R)$ and $e=\mathrm{depth}(S\mathrm{/}\mathfrak{m}S)$. Choose regular sequences of these finite maximal lengths. Under the stated Choice hypothesis, A flat local map splits regular sequences into base and fibre parts lifts their concatenation to an $S$-regular sequence, giving $\mathrm{depth}(S)\ge d+e$.

We prove the reverse inequality by induction on $d+e$, following Stacks Project, Tag 0338. If $d=e=0$, the depth-zero criterion supplies $0\mathrm{\ne }z\in R$ with $\mathfrak{m}z=0$. Flatness makes $S\mathrm{/}\mathfrak{m}S\to S$, $\bar{s}\mapsto zs$, injective. Choose a nonzero closed-fibre element $\bar{y}$ annihilated by $\mathfrak{n}\mathrm{/}\mathfrak{m}S$. Then $zy\mathrm{\ne }0$ and $\mathfrak{n}(zy)=0$, so the depth-zero criterion gives $\mathrm{depth}(S)=0$.

If $d>0$, choose an $R$-regular $x\in \mathfrak{m}$. Flatness makes $x$ $S$-regular, and the repaired split lemma gives $R\mathrm{/}(x)\to S\mathrm{/}(x)$ flat local with the same closed fibre. Induction and Depth drops by one after quotienting by a regular element give $\mathrm{depth}(S)-1=(d-1)+e$. If instead $d=0<e$, lift a closed-fibre regular element $\bar{y}$ to $y\in \mathfrak{n}$. The split lemma makes $y$ regular on $S$ and, crucially, makes $S\mathrm{/}(y)$ flat over $R$; its closed fibre has depth $e-1$. Induction again gives $\mathrm{depth}(S)-1=d+(e-1)$. The only use of Choice in these branches is through that split lemma. Thus in all cases $\mathrm{depth}(S)=d+e$.