Smoothness and derivative bound for x-derivative slices

Let $n$ be a natural number and let $\Phi:\mathbb{R}\times(\mathrm{Fin}\,n\to\mathbb{R})\to\mathbb{C}$ be a function which is $C^\infty$ over $\mathbb{R}$ (smoothness of order $\top$ in $\mathbb{N}_\infty$); fix $j\in\mathbb{N}$ and $x\in\mathbb{R}$. Consider the slice function $g$ sending $y'\in(\mathrm{Fin}\,n\to\mathbb{R})$ to $\mathrm{iteratedDeriv}\,j\,(t\mapsto\Phi(t,y'))\,x$, that is, the $j$-th derivative in the first variable of $\Phi$, taken at the point $x$, with the second variable frozen at $y'$. The conclusion is a conjunction: first, $g$ is $C^\infty$ over $\mathbb{R}$ on $(\mathrm{Fin}\,n\to\mathbb{R})$; second, for every $N\in\mathbb{N}$ and every $y\in(\mathrm{Fin}\,n\to\mathbb{R})$, the norm of the $N$-th iterated Fréchet derivative of $g$ at $y$, as a continuous multilinear map, is at most the norm of the $(N+j)$-th iterated Fréchet derivative of $\Phi$ at the point $(x,y)$. Thus the bound holds with constant $1$, uniformly in $N$ and $y$.

This is the quantitative slicing estimate for a smooth function of one real variable and $n$ further real variables: partial differentiation $j$ times in the first variable and restriction to the slice costs nothing in operator norm beyond shifting the order of the total derivative by $j$. It is used in the construction of smooth bounds for derivatives of oscillatory integrals, feeding MeasureTheory.exists_forall_contDiff_norm_iteratedDeriv_integral_cexp_mul_le_prod_of_contDiff.