Reversing a triple nested derivative of a C³ function

Let $G : \mathbb{R} \to \mathbb{R} \to \mathbb{R} \to \mathbb{C}$ be a complex-valued function of three real variables, let $U \subseteq \mathbb{R} \times \mathbb{R} \times \mathbb{R}$ be an open set containing the origin $(0,0,0)$, and suppose that the uncurried function $p \mapsto G(p_1, p_{2,1}, p_{2,2})$ is three times continuously differentiable on $U$ in the sense of real Fréchet differentiability (ContDiffOn ℝ 3). The conclusion equates two iterated one-variable derivatives, each taken at $0$ and each formed with Mathlib's deriv, which is defined unconditionally and returns $0$ at points of non-differentiability. On the left, the innermost derivative is in the third variable $u$, the next in the second variable $t$, and the outermost in the first variable $s$; on the right the order is reversed, the innermost derivative being in $s$, then $t$, then $u$. Thus the value at the origin of $\partial_s \partial_t \partial_u G$ agrees with that of $\partial_u \partial_t \partial_s G$, the derivatives being computed as nested derivatives of the partial functions rather than as components of a single third Fréchet derivative.

This is the symmetry of third-order partial derivatives (Schwarz's theorem, in the form of iterated one-variable derivatives of a $C^3$ function on an open neighbourhood of the origin), stated for functions valued in $\mathbb{C}$. It is used in the construction of the cubic Casimir operator, where LanglandsTunnell.CubicInduction.casimir_apply_eq_sum_deriv_archRealLift3_mul needs the freedom to reorder the three differentiations applied to a smooth lift of a real group element.