Fderiv Ccinfty

lemma FderivCcinfty {d : ℕ+} {n : ℕ} {U : Set (Fin d → ℝ)} (s : Fin n → Fin d)    {ψ : (Fin d → ℝ) → ℝ} (hψ : ψ ∈ Cc_inftyU d U)    : (fun x => (iteratedFDeriv ℝ n ψ x) (unitSeq s)) ∈ Cc_inftyU d U := by        let ψdev := fun x => (iteratedFDeriv ℝ n ψ x) (unitSeq s)       obtain ⟨ψ_comp, ψ_supp, ψ_diff⟩ := hψ       let eval_at_s := ContinuousMultilinearMap.apply (𝕜 := ℝ) (fun _ => Fin d → ℝ) ℝ (unitSeq s)        have ψdev_comp : HasCompactSupport ψdev := by        have h_comp := HasCompactSupport.iteratedFDeriv (𝕜 := ℝ) ψ_comp n        exact HasCompactSupport.comp_left (hf := h_comp) (g := eval_at_s.toLinearMap) (hg := map_zero _)        have ψdev_supp : tsupport ψdev ⊆ U :=          (closure_mono (Function.support_comp_subset (map_zero eval_at_s) _)).trans            ((tsupport_iteratedFDeriv_subset n).trans ψ_supp)        have ψdev_diff : ContDiff ℝ ((⊤: ℕ∞) : WithTop ℕ∞) ψdev := by         have h0 : ((⊤: ℕ∞): WithTop ℕ∞) + ((n : ℕ∞): WithTop ℕ∞) ≤ ((⊤: ℕ∞) : WithTop ℕ∞)           := by simp only [← WithTop.coe_add, top_add]; rfl         rw [show ψdev = eval_at_s ∘ iteratedFDeriv ℝ n ψ by rfl]         exact (contDiff_const.clm_apply contDiff_id).comp               (ContDiff.iteratedFDeriv_right ψ_diff h0)        exact ⟨ψdev_comp, ψdev_supp, ψdev_diff⟩