Joint smoothness of dslope

Stream: Is there code for X?

[Geoffrey Irving]

I believe we have

/-- `dslope f` is jointly smooth in both variables -/
lemma ContDiffAt.dslope {𝕜 E : Type} [NontriviallyNormedField 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {p : 𝕜 × 𝕜} {n m : ℕ}
    (d1 : ContDiffAt 𝕜 n f p.1) (d2 : ContDiffAt 𝕜 n f p.2) (le : m + 1 ≤ n) :
    ContDiffAt 𝕜 m (fun p : 𝕜 × 𝕜 ↦ dslope f p.1 p.2) p := sorry

but I don't see a way to prove it that isn't a horrible mess: the lemmas we have about dslope don't go up very far, and the explicit derivatives are annoying. Is there a clean route via existing Mathlib?

(Aside: possibly one needs [CharZero 𝕜] for this, I haven't got that far into the details.)