Total Time Derivative cont Diff

lemma totalTimeDerivative_contDiff {δL : Time → X → X → ℝ} (h : IsTotalTimeDerivative δL):    ContDiff ℝ ∞ ↿δL := by rcases isTotalTimeDerivative_explicit.mp h with ⟨F, hContDiff, heq⟩ let Fder_v := Prod.map (fderiv ℝ ↿(fun t q => F t q)) (fun (v : X) => v ) let regroup := ↿(fun (t : Time) (q : X) (v : X) => ((t, q), v)) let appv := fun (FV : ((Time × X →L[ℝ] ℝ) × X )) => FV.fst (1, FV.snd) have hδL : ↿δL = appv ∘ Fder_v ∘ regroup := by   funext tqv   rcases tqv with ⟨t, q, v⟩   simp only [Function.comp_apply]   change δL t q v = appv (Fder_v (regroup (t, q, v)))   rw [heq t q v]   rfl rw [hδL] unfold appv unfold Fder_v unfold regroup fun_prop