diff --git a/Mathlib.lean b/Mathlib.lean
index 7206497b94d35..da2558359008d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1116,8 +1116,10 @@ import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
 import Mathlib.Analysis.Calculus.BumpFunction.Normed
 import Mathlib.Analysis.Calculus.Conformal.InnerProduct
 import Mathlib.Analysis.Calculus.Conformal.NormedSpace
+import Mathlib.Analysis.Calculus.ContDiff.Analytic
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Bounds
+import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
 import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
diff --git a/Mathlib/Analysis/Analytic/Within.lean b/Mathlib/Analysis/Analytic/Within.lean
index 67e0db70351e1..fd9bd854f032d 100644
--- a/Mathlib/Analysis/Analytic/Within.lean
+++ b/Mathlib/Analysis/Analytic/Within.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Geoffrey Irving
 -/
 import Mathlib.Analysis.Analytic.Constructions
+import Mathlib.Analysis.Analytic.ChangeOrigin
 
 /-!
 # Properties of analyticity restricted to a set
@@ -40,8 +41,8 @@ lemma analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : {
     AnalyticWithinAt 𝕜 f s x := by
   rcases mem_nhdsWithin.mp h with ⟨t, ot, xt, st⟩
   rcases Metric.mem_nhds_iff.mp (ot.mem_nhds xt) with ⟨r, r0, rt⟩
-  exact ⟨constFormalMultilinearSeries 𝕜 E (f x), .ofReal r, {
-    r_le := by simp only [FormalMultilinearSeries.constFormalMultilinearSeries_radius, le_top]
+  exact ⟨constFormalMultilinearSeries 𝕜 E (f x), .ofReal r,
+  { r_le := by simp only [FormalMultilinearSeries.constFormalMultilinearSeries_radius, le_top]
     r_pos := by positivity
     hasSum := by
       intro y ys yr
@@ -63,10 +64,10 @@ lemma analyticOn_of_locally_analyticOn {f : E → F} {s : Set E}
   rcases h x m with ⟨u, ou, xu, fu⟩
   rcases Metric.mem_nhds_iff.mp (ou.mem_nhds xu) with ⟨r, r0, ru⟩
   rcases fu x ⟨m, xu⟩ with ⟨p, t, fp⟩
-  exact ⟨p, min (.ofReal r) t, {
-    r_pos := lt_min (by positivity) fp.r_pos
-    r_le := min_le_of_right_le fp.r_le
-    hasSum := by
+  exact ⟨p, min (.ofReal r) t,
+    { r_pos := lt_min (by positivity) fp.r_pos
+      r_le := min_le_of_right_le fp.r_le
+      hasSum := by
         intro y ys yr
         simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at yr
         apply fp.hasSum
@@ -88,8 +89,8 @@ lemma IsOpen.analyticOn_iff_analyticOnNhd {f : E → F} {s : Set E} (hs : IsOpen
   intro hf x m
   rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩
   rcases hf x m with ⟨p, t, fp⟩
-  exact ⟨p, min (.ofReal r) t, {
-    r_pos := lt_min (by positivity) fp.r_pos
+  exact ⟨p, min (.ofReal r) t,
+  { r_pos := lt_min (by positivity) fp.r_pos
     r_le := min_le_of_right_le fp.r_le
     hasSum := by
       intro y ym
@@ -200,3 +201,15 @@ lemma analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s
     exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
 
 alias ⟨AnalyticWithinAt.exists_analyticAt, _⟩ := analyticWithinAt_iff_exists_analyticAt'
+
+lemma AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn
+    [CompleteSpace F] {f : E → F} {s : Set E} {x : E} (h : AnalyticWithinAt 𝕜 f s x) :
+    ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u := by
+  obtain ⟨g, -, h'g, hg⟩ : ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x :=
+    h.exists_analyticAt
+  let u := insert x s ∩ {y | AnalyticAt 𝕜 g y}
+  refine ⟨u, ?_, ?_⟩
+  · exact inter_mem_nhdsWithin _ ((isOpen_analyticAt 𝕜 g).mem_nhds hg)
+  · intro y hy
+    have : AnalyticWithinAt 𝕜 g u y := hy.2.analyticWithinAt
+    exact this.congr (h'g.mono (inter_subset_left)) (h'g (inter_subset_left hy))
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Analytic.lean b/Mathlib/Analysis/Calculus/ContDiff/Analytic.lean
new file mode 100644
index 0000000000000..8ba3cda66b843
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/ContDiff/Analytic.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Analytic
+
+/-!
+# Analytic functions are `C^∞`.
+-/
+
+open Set ContDiff
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  {f : E → F} {s : Set E} {x : E} {n : WithTop ℕ∞}
+
+/-- An analytic function is infinitely differentiable. -/
+protected theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
+    ContDiffOn 𝕜 n f s := by
+  let t := { x | AnalyticAt 𝕜 f x }
+  suffices ContDiffOn 𝕜 ω f t from (this.of_le le_top).mono h
+  rw [← contDiffOn_infty_iff_contDiffOn_omega]
+  have H : AnalyticOnNhd 𝕜 f t := fun _x hx ↦ hx
+  have t_open : IsOpen t := isOpen_analyticAt 𝕜 f
+  exact contDiffOn_of_continuousOn_differentiableOn
+    (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr
+      fun  _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
+    (fun m _ ↦ (H.iteratedFDeriv m).differentiableOn.congr
+      fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
+
+/-- An analytic function on the whole space is infinitely differentiable there. -/
+theorem AnalyticOnNhd.contDiff [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f univ) :
+    ContDiff 𝕜 n f := by
+  rw [← contDiffOn_univ]
+  exact h.contDiffOn
+
+theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} :
+    ContDiffAt 𝕜 n f x := by
+  obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOnNhd
+  exact hf.contDiffOn.contDiffAt hs
+
+protected lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
+    (h : AnalyticWithinAt 𝕜 f s x) {n : ℕ∞} : ContDiffWithinAt 𝕜 n f s x := by
+  rcases h.exists_analyticAt with ⟨g, fx, fg, hg⟩
+  exact hg.contDiffAt.contDiffWithinAt.congr (fg.mono (subset_insert _ _)) fx
+
+protected lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
+    (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s :=
+  fun x m ↦ (h x m).contDiffWithinAt
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.contDiffOn := AnalyticOn.contDiffOn
diff --git a/Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean b/Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean
new file mode 100644
index 0000000000000..3a66c7c3d570a
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Analysis.Calculus.FDeriv.Analytic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+
+/-!
+# Higher smoothness of continuously polynomial functions
+
+We prove that continuously polynomial functions are `C^∞`. In particular, this is the case
+of continuous multilinear maps.
+-/
+
+open Filter Asymptotics
+
+open scoped ENNReal ContDiff
+
+universe u v
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+section fderiv
+
+variable {p : FormalMultilinearSeries 𝕜 E F} {r : ℝ≥0∞} {n : ℕ}
+variable {f : E → F} {x : E} {s : Set E}
+
+/-- A polynomial function is infinitely differentiable. -/
+theorem CPolynomialOn.contDiffOn (h : CPolynomialOn 𝕜 f s) {n : WithTop ℕ∞} :
+    ContDiffOn 𝕜 n f s := by
+  let t := { x | CPolynomialAt 𝕜 f x }
+  suffices ContDiffOn 𝕜 ω f t from (this.of_le le_top).mono h
+  rw [← contDiffOn_infty_iff_contDiffOn_omega]
+  have H : CPolynomialOn 𝕜 f t := fun _x hx ↦ hx
+  have t_open : IsOpen t := isOpen_cPolynomialAt 𝕜 f
+  exact contDiffOn_of_continuousOn_differentiableOn
+    (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr
+      fun  _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
+    (fun m _ ↦ (H.iteratedFDeriv m).analyticOnNhd.differentiableOn.congr
+      fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
+
+theorem CPolynomialAt.contDiffAt (h : CPolynomialAt 𝕜 f x) {n : WithTop ℕ∞} :
+    ContDiffAt 𝕜 n f x :=
+  let ⟨_, hs, hf⟩ := h.exists_mem_nhds_cPolynomialOn
+  hf.contDiffOn.contDiffAt hs
+
+end fderiv
+
+namespace ContinuousMultilinearMap
+
+variable {ι : Type*} {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
+  [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {n : WithTop ℕ∞} {x : Π i, E i}
+
+open FormalMultilinearSeries
+
+lemma contDiffAt : ContDiffAt 𝕜 n f x := f.cpolynomialAt.contDiffAt
+
+lemma contDiff : ContDiff 𝕜 n f := contDiff_iff_contDiffAt.mpr (fun _ ↦ f.contDiffAt)
+
+end ContinuousMultilinearMap
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 9141ffab19f41..48cb70ce773fd 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -7,7 +7,7 @@ import Mathlib.Analysis.Analytic.CPolynomial
 import Mathlib.Analysis.Analytic.Inverse
 import Mathlib.Analysis.Analytic.Within
 import Mathlib.Analysis.Calculus.Deriv.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
 import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Normed.Module.Completion
@@ -63,7 +63,7 @@ differentiability at points in a neighborhood of `s`. Therefore, the theorem tha
 
 open Filter Asymptotics Set
 
-open scoped ENNReal Topology ContDiff
+open scoped ENNReal Topology
 
 universe u v
 
@@ -192,6 +192,7 @@ theorem HasFPowerSeriesOnBall.fderiv_eq [CompleteSpace F] (h : HasFPowerSeriesOn
     fderiv 𝕜 f (x + y) = continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1) :=
   (h.hasFDerivAt hy).fderiv
 
+/-- If a function has a power series on a ball, then so does its derivative. -/
 protected theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F]
     (h : HasFPowerSeriesOnBall f p x r) :
     HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r := by
@@ -238,7 +239,7 @@ protected theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜
 alias AnalyticOn.fderiv := AnalyticOnNhd.fderiv
 
 /-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. See also
-`AnalyticOnNhd.iteratedFDeruv_of_isOpen`, removing the completeness assumption but requiring the set
+`AnalyticOnNhd.iteratedFDeriv_of_isOpen`, removing the completeness assumption but requiring the set
 to be open.-/
 protected theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
     AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s := by
@@ -269,44 +270,6 @@ lemma AnalyticOnNhd.hasFTaylorSeriesUpToOn [CompleteSpace F]
   · apply (DifferentiableAt.continuousAt (𝕜 := 𝕜) ?_).continuousWithinAt
     exact (h.iteratedFDeriv m x hx).differentiableAt
 
-/-- An analytic function is infinitely differentiable. -/
-protected theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s)
-    {n : WithTop ℕ∞} : ContDiffOn 𝕜 n f s := by
-  suffices ContDiffOn 𝕜 ω f s from this.of_le le_top
-  rw [← contDiffOn_infty_iff_contDiffOn_omega]
-  let t := { x | AnalyticAt 𝕜 f x }
-  suffices ContDiffOn 𝕜 ∞ f t from this.mono h
-  have H : AnalyticOnNhd 𝕜 f t := fun _x hx ↦ hx
-  have t_open : IsOpen t := isOpen_analyticAt 𝕜 f
-  exact contDiffOn_of_continuousOn_differentiableOn
-    (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr
-      fun  _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
-    (fun m _ ↦ (H.iteratedFDeriv m).differentiableOn.congr
-      fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
-
-/-- An analytic function on the whole space is infinitely differentiable there. -/
-theorem AnalyticOnNhd.contDiff [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f univ) {n : WithTop ℕ∞} :
-    ContDiff 𝕜 n f := by
-  rw [← contDiffOn_univ]
-  exact h.contDiffOn
-
-theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : WithTop ℕ∞} :
-    ContDiffAt 𝕜 n f x := by
-  obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOnNhd
-  exact hf.contDiffOn.contDiffAt hs
-
-protected lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
-    (h : AnalyticWithinAt 𝕜 f s x) {n : ℕ∞} : ContDiffWithinAt 𝕜 n f s x := by
-  rcases h.exists_analyticAt with ⟨g, fx, fg, hg⟩
-  exact hg.contDiffAt.contDiffWithinAt.congr (fg.mono (subset_insert _ _)) fx
-
-protected lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
-    (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s :=
-  fun x m ↦ (h x m).contDiffWithinAt
-
-@[deprecated (since := "2024-09-26")]
-alias AnalyticWithinOn.contDiffOn := AnalyticOn.contDiffOn
-
 lemma AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn [CompleteSpace F]
     (n : WithTop ℕ∞) (h : AnalyticWithinAt 𝕜 f s x) :
     ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
@@ -384,7 +347,7 @@ protected theorem AnalyticOn.iteratedFDerivWithin (h : AnalyticOn 𝕜 f s)
     apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
     apply LinearIsometryEquiv.analyticOnNhd
 
-lemma AnalyticOn.hasFTaylorSeriesUpToOn {n : WithTop ℕ∞}
+protected lemma AnalyticOn.hasFTaylorSeriesUpToOn {n : WithTop ℕ∞}
     (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
     HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s := by
   refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
@@ -546,26 +509,6 @@ theorem CPolynomialOn.iteratedFDeriv (h : CPolynomialOn 𝕜 f s) (n : ℕ) :
     case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
     simp
 
-/-- A polynomial function is infinitely differentiable. -/
-theorem CPolynomialOn.contDiffOn (h : CPolynomialOn 𝕜 f s) {n : WithTop ℕ∞} :
-    ContDiffOn 𝕜 n f s := by
-  suffices ContDiffOn 𝕜 ω f s from this.of_le le_top
-  let t := { x | CPolynomialAt 𝕜 f x }
-  suffices ContDiffOn 𝕜 ω f t from this.mono h
-  rw [← contDiffOn_infty_iff_contDiffOn_omega]
-  have H : CPolynomialOn 𝕜 f t := fun _x hx ↦ hx
-  have t_open : IsOpen t := isOpen_cPolynomialAt 𝕜 f
-  exact contDiffOn_of_continuousOn_differentiableOn
-    (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr
-      fun  _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
-    (fun m _ ↦ (H.iteratedFDeriv m).analyticOnNhd.differentiableOn.congr
-      fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
-
-theorem CPolynomialAt.contDiffAt (h : CPolynomialAt 𝕜 f x) {n : WithTop ℕ∞} :
-    ContDiffAt 𝕜 n f x :=
-  let ⟨_, hs, hf⟩ := h.exists_mem_nhds_cPolynomialOn
-  hf.contDiffOn.contDiffAt hs
-
 end fderiv
 
 section deriv
@@ -750,10 +693,6 @@ lemma cPolynomialAt : CPolynomialAt 𝕜 f x :=
 
 lemma cPolyomialOn : CPolynomialOn 𝕜 f ⊤ := fun x _ ↦ f.cPolynomialAt x
 
-lemma contDiffAt : ContDiffAt 𝕜 n f x := (f.cPolynomialAt x).contDiffAt
-
-lemma contDiff : ContDiff 𝕜 n f := contDiff_iff_contDiffAt.mpr f.contDiffAt
-
 end ContinuousMultilinearMap
 
 namespace FormalMultilinearSeries
@@ -797,8 +736,8 @@ private theorem factorial_smul' {n : ℕ} : ∀ {F : Type max u v} [NormedAddCom
     n ! • p n (fun _ ↦ y) = iteratedFDeriv 𝕜 n f x (fun _ ↦ y) := by
   induction n with | zero => _ | succ n ih => _ <;> intro F _ _ _ p f h
   · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-  · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag, ← smul_apply,
-      ih h.fderiv, iteratedFDeriv_succ_apply_right]
+  · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
+      ← ContinuousLinearMap.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]
     rfl
 
 variable [CompleteSpace F]
@@ -808,8 +747,8 @@ theorem factorial_smul (n : ℕ) :
     n ! • p n (fun _ ↦ y) = iteratedFDeriv 𝕜 n f x (fun _ ↦ y) := by
   cases n
   · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
-  · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag, ← smul_apply,
-      factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
+  · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
+      ← ContinuousLinearMap.smul_apply, factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
     rfl
 
 theorem hasSum_iteratedFDeriv [CharZero 𝕜] {y : E} (hy : y ∈ EMetric.ball 0 r) :
diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index 0151b54688137..dcf554692ab17 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Kontorovich, David Loeffler, Heather Macbeth, Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Calculus.ParametricIntegral
+import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
 import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.Fourier.FourierTransform
 import Mathlib.Analysis.Calculus.FDeriv.Analytic
@@ -369,7 +370,7 @@ lemma norm_iteratedFDeriv_fourierPowSMulRight
   have I₂ m : ‖iteratedFDeriv ℝ m (T ∘ (ContinuousLinearMap.pi (fun (_ : Fin n) ↦ L))) v‖ ≤
       (n.descFactorial m * 1 * (‖L‖ * ‖v‖) ^ (n - m)) * ‖L‖ ^ m := by
     rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ (ContinuousMultilinearMap.contDiff _)
-      _ le_top]
+      _ (mod_cast le_top)]
     apply (norm_compContinuousLinearMap_le _ _).trans
     simp only [Finset.prod_const, Finset.card_fin]
     gcongr
diff --git a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
index 846339ecb2f00..7a9ffe7ff6f72 100644
--- a/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
+++ b/Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 -/
 import Mathlib.Analysis.Complex.RealDeriv
+import Mathlib.Analysis.Calculus.ContDiff.Analytic
 import Mathlib.Analysis.Calculus.ContDiff.RCLike
+import Mathlib.Analysis.Calculus.FDeriv.Analytic
 import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
 import Mathlib.Analysis.SpecialFunctions.Exponential
 
diff --git a/Mathlib/Geometry/Manifold/AnalyticManifold.lean b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
index 9a1ab30e1daa9..ea26292a58a0d 100644
--- a/Mathlib/Geometry/Manifold/AnalyticManifold.lean
+++ b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Lee, Geoffrey Irving
 -/
 import Mathlib.Analysis.Analytic.Constructions
-import Mathlib.Analysis.Calculus.FDeriv.Analytic
+import Mathlib.Analysis.Calculus.ContDiff.Analytic
 import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
 
 /-!