Partial derivatives of explicit surfaces ℝ×ℝ → EuclideanSpace ℝ (Fin 3) in Lean

Define du f p := fderiv ℝ f p (1,0). To compute it for an explicit map like q ↦ !₂[r*cos q.1*cos q.2, ...]: (1) coordinates: (PiLp.hasFDerivAt_apply (𝕜 := ℝ) 2 (X p) i).comp p hX.hasFDerivAt gives du X p i = du (fun q ↦ X q i) p (needs import Mathlib.Analysis.Calculus.FDeriv.WithLp; then fin_cases i <;> rfl); (2) scalar: du f p = deriv (fun t ↦ f (t, p.2)) p.1 via hf.hasFDerivAt.comp_hasDerivAt p.1 ((hasDerivAt_id p.1).prodMk (hasDerivAt_const _ _)) — for the v-slot write (hasDerivAt_const p.2 p.1).prodMk ... with explicit args, else dot notation resolves to HasFDerivAtFilter and fails; (3) then simp (disch := fun_prop) only [du_eq_deriv]; simp evaluates the trig derivatives automatically. Smoothness: rw [contDiff_piLp]; intro i; fin_cases i <;> simp <;> fun_prop. sinh/cosh need import ...Trigonometric.DerivHyp or fun_prop says 'No theorems found for Real.cosh'.