Depth is additive for a flat local homomorphism

Write $d=\mathrm{depth}(R)$ and $e=\mathrm{depth}(S\mathrm{/}\mathfrak{m}S)$. Concatenating maximal regular sequences from the base and closed fibre by lem-flat-local-depth-formula-regular-sequence-split gives $\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 $R\mathrm{/}(x)\to S\mathrm{/}(x)$ is again flat local with the same closed fibre. Induction and lem-depth-quotient-by-regular-element give $\mathrm{depth}(S)-1=(d-1)+e\mathrm{.}$ If instead $d=0<e$, lift a closed-fibre regular element $\bar{y}$. The local flatness criterion makes $y$ regular on $S$ and makes $S\mathrm{/}(y)$ flat over $R$; its closed fibre has depth $e-1$. Induction again gives $\mathrm{depth}(S)-1=d+(e-1)$. Thus in all cases $\mathrm{depth}(S)=d+e$.