Schwarz symmetry for nested derivatives at the origin

Let $F : \mathbb{R} \to \mathbb{R} \to \mathbb{C}$ be a function of two real variables with complex values, let $U$ be a subset of $\mathbb{R} \times \mathbb{R}$, assume $U$ is open and that the origin $(0,0)$ lies in $U$, and assume that the uncurried function $p \mapsto F(p_1, p_2)$ is twice continuously differentiable on $U$ in the sense of ContDiffOn ℝ 2. Then the two nested one-variable derivatives at the origin agree: the derivative at $0$ of the function $s \mapsto \bigl(\text{derivative at } 0 \text{ of } t \mapsto F(s,t)\bigr)$ equals the derivative at $0$ of the function $t \mapsto \bigl(\text{derivative at } 0 \text{ of } s \mapsto F(s,t)\bigr)$. Here the derivatives are Mathlib's total deriv on functions $\mathbb{R} \to \mathbb{C}$, so in each nested expression the inner derivative is formed at the point $0$ for every value of the outer variable, including those for which the relevant slice need not meet $U$, and no differentiability is asserted of the intermediate functions beyond what the conclusion requires.

This is the Schwarz–Clairaut symmetry of second partial derivatives, in the shape needed when $F$ is only assumed $C^2$ on an open neighbourhood of the origin rather than on all of $\mathbb{R}^2$, and with the partial derivatives written as iterated one-variable derivs. It is used in the computation of the action of the Casimir element on archimedean lifts in LanglandsTunnell.CubicInduction.casimir_apply_eq_sum_deriv_archRealLift3_mul.