diff --git a/Mathlib.lean b/Mathlib.lean
index 137a6ad1e6f16..008af882b8dc9 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1252,6 +1252,7 @@ import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
 import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
 import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.ContDiff.RCLike
 import Mathlib.Analysis.Calculus.ContDiff.WithLp
 import Mathlib.Analysis.Calculus.DSlope
diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
index 30d9e9d2f658c..4a672cb0645eb 100644
--- a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
+++ b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
 import Mathlib.Data.Fintype.Perm
 
diff --git a/Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean b/Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
index 104a452fe5423..b01bd97552b2a 100644
--- a/Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
+++ b/Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 
 /-!
 # Smooth affine maps
diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Basic.lean b/Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
index 2f7721e6ffc3c..d8b3ea4a1a920 100644
--- a/Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
+++ b/Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Normed.Module.FiniteDimension
 
 /-!
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
index e502a68a8bc15..4f74997699bc5 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
@@ -7,13 +7,12 @@ import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
 import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Mul
-import Mathlib.Analysis.Calculus.Deriv.Inverse
 
 /-!
-# Higher differentiability of usual operations
+# Higher differentiability of composition
 
-We prove that the usual operations (addition, multiplication, difference, composition, and
-so on) preserve `C^n` functions. We also expand the API around `C^n` functions.
+We prove that the composition of `C^n` functions is `C^n`.
+We also expand the API around `C^n` functions.
 
 ## Main results
 
@@ -1216,756 +1215,6 @@ theorem ContDiff.contDiff_fderiv_apply {f : E → F} (hf : ContDiff 𝕜 n f) (h
   rw [← fderivWithin_univ, ← univ_prod_univ]
   exact contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn
 
-/-!
-### Smoothness of functions `f : E → Π i, F' i`
--/
-
-section Pi
-
-variable {ι ι' : Type*} [Fintype ι] [Fintype ι'] {F' : ι → Type*} [∀ i, NormedAddCommGroup (F' i)]
-  [∀ i, NormedSpace 𝕜 (F' i)] {φ : ∀ i, E → F' i} {p' : ∀ i, E → FormalMultilinearSeries 𝕜 E (F' i)}
-  {Φ : E → ∀ i, F' i} {P' : E → FormalMultilinearSeries 𝕜 E (∀ i, F' i)}
-
-theorem hasFTaylorSeriesUpToOn_pi {n : WithTop ℕ∞} :
-    HasFTaylorSeriesUpToOn n (fun x i => φ i x)
-        (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
-      ∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s := by
-  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
-  set L : ∀ m : ℕ, (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i := fun m =>
-    ContinuousMultilinearMap.piₗᵢ _ _
-  refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
-  · exact h.continuousLinearMap_comp (pr i)
-  · ext1 i
-    exact (h i).zero_eq x hx
-  · intro m hm x hx
-    exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
-      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx
-  · intro m hm
-    exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm
-
-@[simp]
-theorem hasFTaylorSeriesUpToOn_pi' {n : WithTop ℕ∞} :
-    HasFTaylorSeriesUpToOn n Φ P' s ↔
-      ∀ i, HasFTaylorSeriesUpToOn n (fun x => Φ x i)
-        (fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap
-          (P' x m)) s := by
-  convert hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i); ext; rfl
-
-theorem contDiffWithinAt_pi :
-    ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x := by
-  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
-  refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
-  match n with
-  | ω =>
-    choose u hux p hp h'p using h
-    refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
-      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
-    set L : (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i :=
-      ContinuousMultilinearMap.piₗᵢ _ _
-    change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
-    apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
-    exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
-  | (n : ℕ∞) =>
-    intro m hm
-    choose u hux p hp using fun i => h i m hm
-    exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
-      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩
-
-theorem contDiffOn_pi : ContDiffOn 𝕜 n Φ s ↔ ∀ i, ContDiffOn 𝕜 n (fun x => Φ x i) s :=
-  ⟨fun h _ x hx => contDiffWithinAt_pi.1 (h x hx) _, fun h x hx =>
-    contDiffWithinAt_pi.2 fun i => h i x hx⟩
-
-theorem contDiffAt_pi : ContDiffAt 𝕜 n Φ x ↔ ∀ i, ContDiffAt 𝕜 n (fun x => Φ x i) x :=
-  contDiffWithinAt_pi
-
-theorem contDiff_pi : ContDiff 𝕜 n Φ ↔ ∀ i, ContDiff 𝕜 n fun x => Φ x i := by
-  simp only [← contDiffOn_univ, contDiffOn_pi]
-
-theorem contDiff_update [DecidableEq ι] (k : WithTop ℕ∞) (x : ∀ i, F' i) (i : ι) :
-    ContDiff 𝕜 k (update x i) := by
-  rw [contDiff_pi]
-  intro j
-  dsimp [Function.update]
-  split_ifs with h
-  · subst h
-    exact contDiff_id
-  · exact contDiff_const
-
-variable (F') in
-theorem contDiff_single [DecidableEq ι] (k : WithTop ℕ∞) (i : ι) :
-    ContDiff 𝕜 k (Pi.single i : F' i → ∀ i, F' i) :=
-  contDiff_update k 0 i
-
-variable (𝕜 E)
-
-theorem contDiff_apply (i : ι) : ContDiff 𝕜 n fun f : ι → E => f i :=
-  contDiff_pi.mp contDiff_id i
-
-theorem contDiff_apply_apply (i : ι) (j : ι') : ContDiff 𝕜 n fun f : ι → ι' → E => f i j :=
-  contDiff_pi.mp (contDiff_apply 𝕜 (ι' → E) i) j
-
-end Pi
-
-/-! ### Sum of two functions -/
-
-section Add
-
-theorem HasFTaylorSeriesUpToOn.add {n : WithTop ℕ∞} {q g} (hf : HasFTaylorSeriesUpToOn n f p s)
-    (hg : HasFTaylorSeriesUpToOn n g q s) : HasFTaylorSeriesUpToOn n (f + g) (p + q) s := by
-  exact HasFTaylorSeriesUpToOn.continuousLinearMap_comp
-    (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F) (hf.prod hg)
-
--- The sum is smooth.
-theorem contDiff_add : ContDiff 𝕜 n fun p : F × F => p.1 + p.2 :=
-  (IsBoundedLinearMap.fst.add IsBoundedLinearMap.snd).contDiff
-
-/-- The sum of two `C^n` functions within a set at a point is `C^n` within this set
-at this point. -/
-theorem ContDiffWithinAt.add {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
-    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x :=
-  contDiff_add.contDiffWithinAt.comp x (hf.prod hg) subset_preimage_univ
-
-/-- The sum of two `C^n` functions at a point is `C^n` at this point. -/
-theorem ContDiffAt.add {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
-    ContDiffAt 𝕜 n (fun x => f x + g x) x := by
-  rw [← contDiffWithinAt_univ] at *; exact hf.add hg
-
-/-- The sum of two `C^n`functions is `C^n`. -/
-theorem ContDiff.add {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
-    ContDiff 𝕜 n fun x => f x + g x :=
-  contDiff_add.comp (hf.prod hg)
-
-/-- The sum of two `C^n` functions on a domain is `C^n`. -/
-theorem ContDiffOn.add {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
-    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x + g x) s := fun x hx =>
-  (hf x hx).add (hg x hx)
-
-variable {i : ℕ}
-
-/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
-See also `iteratedFDerivWithin_add_apply'`, which uses the spelling `(fun x ↦ f x + g x)`
-instead of `f + g`. -/
-theorem iteratedFDerivWithin_add_apply {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x)
-    (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
-    iteratedFDerivWithin 𝕜 i (f + g) s x =
-      iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x := by
-  have := (hf.eventually (by simp)).and (hg.eventually (by simp))
-  obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
-  have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
-  have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
-  have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
-  have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
-    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
-  rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
-    ← iteratedFDerivWithin_congr_set H]
-  exact .symm (((hft.ftaylorSeriesWithin hut).add
-      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)
-
-/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
-This is the same as `iteratedFDerivWithin_add_apply`, but using the spelling `(fun x ↦ f x + g x)`
-instead of `f + g`, which can be handy for some rewrites.
-TODO: use one form consistently. -/
-theorem iteratedFDerivWithin_add_apply' {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x)
-    (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
-    iteratedFDerivWithin 𝕜 i (fun x => f x + g x) s x =
-      iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x :=
-  iteratedFDerivWithin_add_apply hf hg hu hx
-
-theorem iteratedFDeriv_add_apply {i : ℕ} {f g : E → F}
-    (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
-    iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x := by
-  simp_rw [← iteratedFDerivWithin_univ]
-  exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)
-
-theorem iteratedFDeriv_add_apply' {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 i f x)
-    (hg : ContDiffAt 𝕜 i g x) :
-    iteratedFDeriv 𝕜 i (fun x => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x :=
-  iteratedFDeriv_add_apply hf hg
-
-end Add
-
-/-! ### Negative -/
-
-section Neg
-
--- The negative is smooth.
-theorem contDiff_neg : ContDiff 𝕜 n fun p : F => -p :=
-  IsBoundedLinearMap.id.neg.contDiff
-
-/-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
-this point. -/
-theorem ContDiffWithinAt.neg {s : Set E} {f : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) :
-    ContDiffWithinAt 𝕜 n (fun x => -f x) s x :=
-  contDiff_neg.contDiffWithinAt.comp x hf subset_preimage_univ
-
-/-- The negative of a `C^n` function at a point is `C^n` at this point. -/
-theorem ContDiffAt.neg {f : E → F} (hf : ContDiffAt 𝕜 n f x) :
-    ContDiffAt 𝕜 n (fun x => -f x) x := by rw [← contDiffWithinAt_univ] at *; exact hf.neg
-
-/-- The negative of a `C^n`function is `C^n`. -/
-theorem ContDiff.neg {f : E → F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => -f x :=
-  contDiff_neg.comp hf
-
-/-- The negative of a `C^n` function on a domain is `C^n`. -/
-theorem ContDiffOn.neg {s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) :
-    ContDiffOn 𝕜 n (fun x => -f x) s := fun x hx => (hf x hx).neg
-
-variable {i : ℕ}
-
--- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: define `Neg` instance on `ContinuousLinearEquiv`,
--- prove it from `ContinuousLinearEquiv.iteratedFDerivWithin_comp_left`
-theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
-    iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x := by
-  induction' i with i hi generalizing x
-  · ext; simp
-  · ext h
-    calc
-      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
-          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
-        rfl
-      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
-        rw [fderivWithin_congr' (@hi) hx]; rfl
-      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
-        rw [Pi.neg_def, fderivWithin_neg (hu x hx)]; rfl
-      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := rfl
-
-theorem iteratedFDeriv_neg_apply {i : ℕ} {f : E → F} :
-    iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x := by
-  simp_rw [← iteratedFDerivWithin_univ]
-  exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)
-
-end Neg
-
-/-! ### Subtraction -/
-
-/-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
-at this point. -/
-theorem ContDiffWithinAt.sub {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
-    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x := by
-  simpa only [sub_eq_add_neg] using hf.add hg.neg
-
-/-- The difference of two `C^n` functions at a point is `C^n` at this point. -/
-theorem ContDiffAt.sub {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
-    ContDiffAt 𝕜 n (fun x => f x - g x) x := by simpa only [sub_eq_add_neg] using hf.add hg.neg
-
-/-- The difference of two `C^n` functions on a domain is `C^n`. -/
-theorem ContDiffOn.sub {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
-    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x - g x) s := by
-  simpa only [sub_eq_add_neg] using hf.add hg.neg
-
-/-- The difference of two `C^n` functions is `C^n`. -/
-theorem ContDiff.sub {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
-    ContDiff 𝕜 n fun x => f x - g x := by simpa only [sub_eq_add_neg] using hf.add hg.neg
-
-/-! ### Sum of finitely many functions -/
-
-theorem ContDiffWithinAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E}
-    (h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x) :
-    ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x := by
-  classical
-    induction' s using Finset.induction_on with i s is IH
-    · simp [contDiffWithinAt_const]
-    · simp only [is, Finset.sum_insert, not_false_iff]
-      exact (h _ (Finset.mem_insert_self i s)).add
-        (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
-
-theorem ContDiffAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {x : E}
-    (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) :
-    ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x := by
-  rw [← contDiffWithinAt_univ] at *; exact ContDiffWithinAt.sum h
-
-theorem ContDiffOn.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E}
-    (h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t) :
-    ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t := fun x hx =>
-  ContDiffWithinAt.sum fun i hi => h i hi x hx
-
-theorem ContDiff.sum {ι : Type*} {f : ι → E → F} {s : Finset ι}
-    (h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) : ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x := by
-  simp only [← contDiffOn_univ] at *; exact ContDiffOn.sum h
-
-theorem iteratedFDerivWithin_sum_apply {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E}
-    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 i (f j) s x) :
-    iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j ·) s x =
-      ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x := by
-  induction u using Finset.cons_induction with
-  | empty => ext; simp [hs, hx]
-  | cons a u ha IH =>
-    simp only [Finset.mem_cons, forall_eq_or_imp] at h
-    simp only [Finset.sum_cons]
-    rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
-
-theorem iteratedFDeriv_sum {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ}
-    (h : ∀ j ∈ u, ContDiff 𝕜 i (f j)) :
-    iteratedFDeriv 𝕜 i (∑ j ∈ u, f j ·) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j) :=
-  funext fun x ↦ by simpa [iteratedFDerivWithin_univ] using
-    iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (mem_univ x) (h · · |>.contDiffWithinAt)
-
-/-! ### Product of two functions -/
-
-section MulProd
-
-variable {𝔸 𝔸' ι 𝕜' : Type*} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [NormedCommRing 𝔸']
-  [NormedAlgebra 𝕜 𝔸'] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
-
--- The product is smooth.
-theorem contDiff_mul : ContDiff 𝕜 n fun p : 𝔸 × 𝔸 => p.1 * p.2 :=
-  (ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.contDiff
-
-/-- The product of two `C^n` functions within a set at a point is `C^n` within this set
-at this point. -/
-theorem ContDiffWithinAt.mul {s : Set E} {f g : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x)
-    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x :=
-  contDiff_mul.comp_contDiffWithinAt (hf.prod hg)
-
-/-- The product of two `C^n` functions at a point is `C^n` at this point. -/
-nonrec theorem ContDiffAt.mul {f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
-    ContDiffAt 𝕜 n (fun x => f x * g x) x :=
-  hf.mul hg
-
-/-- The product of two `C^n` functions on a domain is `C^n`. -/
-theorem ContDiffOn.mul {f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
-    ContDiffOn 𝕜 n (fun x => f x * g x) s := fun x hx => (hf x hx).mul (hg x hx)
-
-/-- The product of two `C^n`functions is `C^n`. -/
-theorem ContDiff.mul {f g : E → 𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
-    ContDiff 𝕜 n fun x => f x * g x :=
-  contDiff_mul.comp (hf.prod hg)
-
-theorem contDiffWithinAt_prod' {t : Finset ι} {f : ι → E → 𝔸'}
-    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x :=
-  Finset.prod_induction f (fun f => ContDiffWithinAt 𝕜 n f s x) (fun _ _ => ContDiffWithinAt.mul)
-    (contDiffWithinAt_const (c := 1)) h
-
-theorem contDiffWithinAt_prod {t : Finset ι} {f : ι → E → 𝔸'}
-    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) :
-    ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x := by
-  simpa only [← Finset.prod_apply] using contDiffWithinAt_prod' h
-
-theorem contDiffAt_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
-    ContDiffAt 𝕜 n (∏ i ∈ t, f i) x :=
-  contDiffWithinAt_prod' h
-
-theorem contDiffAt_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
-    ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x :=
-  contDiffWithinAt_prod h
-
-theorem contDiffOn_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
-    ContDiffOn 𝕜 n (∏ i ∈ t, f i) s := fun x hx => contDiffWithinAt_prod' fun i hi => h i hi x hx
-
-theorem contDiffOn_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
-    ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s := fun x hx =>
-  contDiffWithinAt_prod fun i hi => h i hi x hx
-
-theorem contDiff_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
-    ContDiff 𝕜 n (∏ i ∈ t, f i) :=
-  contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod' fun i hi => (h i hi).contDiffAt
-
-theorem contDiff_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
-    ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y :=
-  contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod fun i hi => (h i hi).contDiffAt
-
-theorem ContDiff.pow {f : E → 𝔸} (hf : ContDiff 𝕜 n f) : ∀ m : ℕ, ContDiff 𝕜 n fun x => f x ^ m
-  | 0 => by simpa using contDiff_const
-  | m + 1 => by simpa [pow_succ] using (hf.pow m).mul hf
-
-theorem ContDiffWithinAt.pow {f : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (m : ℕ) :
-    ContDiffWithinAt 𝕜 n (fun y => f y ^ m) s x :=
-  (contDiff_id.pow m).comp_contDiffWithinAt hf
-
-nonrec theorem ContDiffAt.pow {f : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (m : ℕ) :
-    ContDiffAt 𝕜 n (fun y => f y ^ m) x :=
-  hf.pow m
-
-theorem ContDiffOn.pow {f : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (m : ℕ) :
-    ContDiffOn 𝕜 n (fun y => f y ^ m) s := fun y hy => (hf y hy).pow m
-
-theorem ContDiffWithinAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') :
-    ContDiffWithinAt 𝕜 n (fun x => f x / c) s x := by
-  simpa only [div_eq_mul_inv] using hf.mul contDiffWithinAt_const
-
-nonrec theorem ContDiffAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffAt 𝕜 n f x) (c : 𝕜') :
-    ContDiffAt 𝕜 n (fun x => f x / c) x :=
-  hf.div_const c
-
-theorem ContDiffOn.div_const {f : E → 𝕜'} {n} (hf : ContDiffOn 𝕜 n f s) (c : 𝕜') :
-    ContDiffOn 𝕜 n (fun x => f x / c) s := fun x hx => (hf x hx).div_const c
-
-theorem ContDiff.div_const {f : E → 𝕜'} {n} (hf : ContDiff 𝕜 n f) (c : 𝕜') :
-    ContDiff 𝕜 n fun x => f x / c := by simpa only [div_eq_mul_inv] using hf.mul contDiff_const
-
-end MulProd
-
-/-! ### Scalar multiplication -/
-
-section SMul
-
--- The scalar multiplication is smooth.
-theorem contDiff_smul : ContDiff 𝕜 n fun p : 𝕜 × F => p.1 • p.2 :=
-  isBoundedBilinearMap_smul.contDiff
-
-/-- The scalar multiplication of two `C^n` functions within a set at a point is `C^n` within this
-set at this point. -/
-theorem ContDiffWithinAt.smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
-    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x • g x) s x :=
-  contDiff_smul.contDiffWithinAt.comp x (hf.prod hg) subset_preimage_univ
-
-/-- The scalar multiplication of two `C^n` functions at a point is `C^n` at this point. -/
-theorem ContDiffAt.smul {f : E → 𝕜} {g : E → F} (hf : ContDiffAt 𝕜 n f x)
-    (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x • g x) x := by
-  rw [← contDiffWithinAt_univ] at *; exact hf.smul hg
-
-/-- The scalar multiplication of two `C^n` functions is `C^n`. -/
-theorem ContDiff.smul {f : E → 𝕜} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
-    ContDiff 𝕜 n fun x => f x • g x :=
-  contDiff_smul.comp (hf.prod hg)
-
-/-- The scalar multiplication of two `C^n` functions on a domain is `C^n`. -/
-theorem ContDiffOn.smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffOn 𝕜 n f s)
-    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x • g x) s := fun x hx =>
-  (hf x hx).smul (hg x hx)
-
-end SMul
-
-/-! ### Constant scalar multiplication
-
-Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: generalize results in this section.
-
-1. It should be possible to assume `[Monoid R] [DistribMulAction R F] [SMulCommClass 𝕜 R F]`.
-2. If `c` is a unit (or `R` is a group), then one can drop `ContDiff*` assumptions in some
-  lemmas.
--/
-
-section ConstSMul
-
-variable {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F]
-variable [ContinuousConstSMul R F]
-
--- The scalar multiplication with a constant is smooth.
-theorem contDiff_const_smul (c : R) : ContDiff 𝕜 n fun p : F => c • p :=
-  (c • ContinuousLinearMap.id 𝕜 F).contDiff
-
-/-- The scalar multiplication of a constant and a `C^n` function within a set at a point is `C^n`
-within this set at this point. -/
-theorem ContDiffWithinAt.const_smul {s : Set E} {f : E → F} {x : E} (c : R)
-    (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun y => c • f y) s x :=
-  (contDiff_const_smul c).contDiffAt.comp_contDiffWithinAt x hf
-
-/-- The scalar multiplication of a constant and a `C^n` function at a point is `C^n` at this
-point. -/
-theorem ContDiffAt.const_smul {f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) :
-    ContDiffAt 𝕜 n (fun y => c • f y) x := by
-  rw [← contDiffWithinAt_univ] at *; exact hf.const_smul c
-
-/-- The scalar multiplication of a constant and a `C^n` function is `C^n`. -/
-theorem ContDiff.const_smul {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
-    ContDiff 𝕜 n fun y => c • f y :=
-  (contDiff_const_smul c).comp hf
-
-/-- The scalar multiplication of a constant and a `C^n` on a domain is `C^n`. -/
-theorem ContDiffOn.const_smul {s : Set E} {f : E → F} (c : R) (hf : ContDiffOn 𝕜 n f s) :
-    ContDiffOn 𝕜 n (fun y => c • f y) s := fun x hx => (hf x hx).const_smul c
-
-variable {i : ℕ} {a : R}
-
-theorem iteratedFDerivWithin_const_smul_apply (hf : ContDiffWithinAt 𝕜 i f s x)
-    (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
-    iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x :=
-  (a • (1 : F →L[𝕜] F)).iteratedFDerivWithin_comp_left hf hu hx le_rfl
-
-theorem iteratedFDeriv_const_smul_apply (hf : ContDiffAt 𝕜 i f x) :
-    iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x :=
-  (a • (1 : F →L[𝕜] F)).iteratedFDeriv_comp_left hf le_rfl
-
-theorem iteratedFDeriv_const_smul_apply' (hf : ContDiffAt 𝕜 i f x) :
-    iteratedFDeriv 𝕜 i (fun x ↦ a • f x) x = a • iteratedFDeriv 𝕜 i f x :=
-  iteratedFDeriv_const_smul_apply hf
-
-end ConstSMul
-
-/-! ### Cartesian product of two functions -/
-
-section prodMap
-
-variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
-variable {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
-
-/-- The product map of two `C^n` functions within a set at a point is `C^n`
-within the product set at the product point. -/
-theorem ContDiffWithinAt.prod_map' {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {p : E × E'}
-    (hf : ContDiffWithinAt 𝕜 n f s p.1) (hg : ContDiffWithinAt 𝕜 n g t p.2) :
-    ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p :=
-  (hf.comp p contDiffWithinAt_fst (prod_subset_preimage_fst _ _)).prod
-    (hg.comp p contDiffWithinAt_snd (prod_subset_preimage_snd _ _))
-
-theorem ContDiffWithinAt.prod_map {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {x : E}
-    {y : E'} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g t y) :
-    ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y) :=
-  ContDiffWithinAt.prod_map' hf hg
-
-/-- The product map of two `C^n` functions on a set is `C^n` on the product set. -/
-theorem ContDiffOn.prod_map {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type*}
-    [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'}
-    (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g t) : ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t) :=
-  (hf.comp contDiffOn_fst (prod_subset_preimage_fst _ _)).prod
-    (hg.comp contDiffOn_snd (prod_subset_preimage_snd _ _))
-
-/-- The product map of two `C^n` functions within a set at a point is `C^n`
-within the product set at the product point. -/
-theorem ContDiffAt.prod_map {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffAt 𝕜 n f x)
-    (hg : ContDiffAt 𝕜 n g y) : ContDiffAt 𝕜 n (Prod.map f g) (x, y) := by
-  rw [ContDiffAt] at *
-  convert hf.prod_map hg
-  simp only [univ_prod_univ]
-
-/-- The product map of two `C^n` functions within a set at a point is `C^n`
-within the product set at the product point. -/
-theorem ContDiffAt.prod_map' {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffAt 𝕜 n f p.1)
-    (hg : ContDiffAt 𝕜 n g p.2) : ContDiffAt 𝕜 n (Prod.map f g) p := by
-  rcases p with ⟨⟩
-  exact ContDiffAt.prod_map hf hg
-
-/-- The product map of two `C^n` functions is `C^n`. -/
-theorem ContDiff.prod_map {f : E → F} {g : E' → F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
-    ContDiff 𝕜 n (Prod.map f g) := by
-  rw [contDiff_iff_contDiffAt] at *
-  exact fun ⟨x, y⟩ => (hf x).prod_map (hg y)
-
-theorem contDiff_prod_mk_left (f₀ : F) : ContDiff 𝕜 n fun e : E => (e, f₀) :=
-  contDiff_id.prod contDiff_const
-
-theorem contDiff_prod_mk_right (e₀ : E) : ContDiff 𝕜 n fun f : F => (e₀, f) :=
-  contDiff_const.prod contDiff_id
-
-end prodMap
-
-/-!
-### Inversion in a complete normed algebra (or more generally with summable geometric series)
--/
-
-section AlgebraInverse
-
-variable (𝕜)
-variable {R : Type*} [NormedRing R] [NormedAlgebra 𝕜 R]
-
-open NormedRing ContinuousLinearMap Ring
-
-/-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
-invertible element, as it is analytic. -/
-theorem contDiffAt_ring_inverse [HasSummableGeomSeries R] (x : Rˣ) :
-    ContDiffAt 𝕜 n Ring.inverse (x : R) := by
-  have := AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n)
-    Units.isOpen.uniqueDiffOn x x.isUnit
-  exact this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)
-
-variable {𝕜' : Type*} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
-
-theorem contDiffAt_inv {x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.inv x := by
-  simpa only [Ring.inverse_eq_inv'] using contDiffAt_ring_inverse 𝕜 (Units.mk0 x hx)
-
-theorem contDiffOn_inv {n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') {0}ᶜ := fun _ hx =>
-  (contDiffAt_inv 𝕜 hx).contDiffWithinAt
-
-variable {𝕜}
-
-theorem ContDiffWithinAt.inv {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) :
-    ContDiffWithinAt 𝕜 n (fun x => (f x)⁻¹) s x :=
-  (contDiffAt_inv 𝕜 hx).comp_contDiffWithinAt x hf
-
-theorem ContDiffOn.inv {f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) :
-    ContDiffOn 𝕜 n (fun x => (f x)⁻¹) s := fun x hx => (hf.contDiffWithinAt hx).inv (h x hx)
-
-nonrec theorem ContDiffAt.inv {f : E → 𝕜'} (hf : ContDiffAt 𝕜 n f x) (hx : f x ≠ 0) :
-    ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x :=
-  hf.inv hx
-
-theorem ContDiff.inv {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ x, f x ≠ 0) :
-    ContDiff 𝕜 n fun x => (f x)⁻¹ := by
-  rw [contDiff_iff_contDiffAt]; exact fun x => hf.contDiffAt.inv (h x)
-
--- TODO: generalize to `f g : E → 𝕜'`
-theorem ContDiffWithinAt.div {f g : E → 𝕜} {n} (hf : ContDiffWithinAt 𝕜 n f s x)
-    (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) :
-    ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x := by
-  simpa only [div_eq_mul_inv] using hf.mul (hg.inv hx)
-
-theorem ContDiffOn.div {f g : E → 𝕜} {n} (hf : ContDiffOn 𝕜 n f s)
-    (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContDiffOn 𝕜 n (f / g) s := fun x hx =>
-  (hf x hx).div (hg x hx) (h₀ x hx)
-
-nonrec theorem ContDiffAt.div {f g : E → 𝕜} {n} (hf : ContDiffAt 𝕜 n f x)
-    (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) : ContDiffAt 𝕜 n (fun x => f x / g x) x :=
-  hf.div hg hx
-
-theorem ContDiff.div {f g : E → 𝕜} {n} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g)
-    (h0 : ∀ x, g x ≠ 0) : ContDiff 𝕜 n fun x => f x / g x := by
-  simp only [contDiff_iff_contDiffAt] at *
-  exact fun x => (hf x).div (hg x) (h0 x)
-
-end AlgebraInverse
-
-/-! ### Inversion of continuous linear maps between Banach spaces -/
-
-section MapInverse
-
-open ContinuousLinearMap
-
-/-- At a continuous linear equivalence `e : E ≃L[𝕜] F` between Banach spaces, the operation of
-inversion is `C^n`, for all `n`. -/
-theorem contDiffAt_map_inverse [CompleteSpace E] (e : E ≃L[𝕜] F) :
-    ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F) := by
-  nontriviality E
-  -- first, we use the lemma `to_ring_inverse` to rewrite in terms of `Ring.inverse` in the ring
-  -- `E →L[𝕜] E`
-  let O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp (e.symm : F →L[𝕜] E)
-  let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
-  have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (to_ring_inverse e)
-  rw [this]
-  -- `O₁` and `O₂` are `ContDiff`,
-  -- so we reduce to proving that `Ring.inverse` is `ContDiff`
-  have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
-  have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
-  refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)
-  convert contDiffAt_ring_inverse 𝕜 (1 : (E →L[𝕜] E)ˣ)
-  simp [O₂, one_def]
-
-/-- At an invertible map `e : M →L[R] M₂` between Banach spaces, the operation of
-inversion is `C^n`, for all `n`. -/
-theorem ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse [CompleteSpace E] {e : E →L[𝕜] F}
-    (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e := by
-  rcases he with ⟨M, rfl⟩
-  exact _root_.contDiffAt_map_inverse M
-
-end MapInverse
-
-section FunctionInverse
-
-open ContinuousLinearMap
-
-/-- If `f` is a local homeomorphism and the point `a` is in its target,
-and if `f` is `n` times continuously differentiable at `f.symm a`,
-and if the derivative at `f.symm a` is a continuous linear equivalence,
-then `f.symm` is `n` times continuously differentiable at the point `a`.
-
-This is one of the easy parts of the inverse function theorem: it assumes that we already have
-an inverse function. -/
-theorem PartialHomeomorph.contDiffAt_symm [CompleteSpace E] (f : PartialHomeomorph E F)
-    {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
-    (hf₀' : HasFDerivAt f (f₀' : E →L[𝕜] F) (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) :
-    ContDiffAt 𝕜 n f.symm a := by
-  match n with
-  | ω =>
-    apply AnalyticAt.contDiffAt
-    exact f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv
-  | (n : ℕ∞) =>
-    -- We prove this by induction on `n`
-    induction' n using ENat.nat_induction with n IH Itop
-    · apply contDiffAt_zero.2
-      exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
-    · obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
-      apply contDiffAt_succ_iff_hasFDerivAt.2
-      -- For showing `n.succ` times continuous differentiability (the main inductive step), it
-      -- suffices to produce the derivative and show that it is `n` times continuously
-      -- differentiable
-      have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
-      -- This follows by a bootstrapping formula expressing the derivative as a
-      -- function of `f` itself
-      refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
-      · -- We first check that the derivative of `f` is that formula
-        have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
-          have hf₀' := f₀'.nhds
-          rw [← eq_f₀'] at hf₀'
-          exact hf'.continuousAt.preimage_mem_nhds hf₀'
-        obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
-        use f.target ∩ f.symm ⁻¹' t
-        refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
-        · exact f.isOpen_inter_preimage_symm ht
-        · exact mem_inter ha (mem_preimage.mpr htf)
-        intro x hx
-        obtain ⟨hxu, e, he⟩ := htu hx.2
-        have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
-          rw [he]
-          exact hff' (f.symm x) hxu
-        convert f.hasFDerivAt_symm hx.1 h_deriv
-        simp [← he]
-      · -- Then we check that the formula, being a composition of `ContDiff` pieces, is
-        -- itself `ContDiff`
-        have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
-          rw [eq_f₀']
-          exact contDiffAt_map_inverse _
-        have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
-          refine IH (hf.of_le ?_)
-          norm_cast
-          exact Nat.le_succ n
-        exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
-    · refine contDiffAt_infty.mpr ?_
-      intro n
-      exact Itop n (contDiffAt_infty.mp hf n)
-
-/-- If `f` is an `n` times continuously differentiable homeomorphism,
-and if the derivative of `f` at each point is a continuous linear equivalence,
-then `f.symm` is `n` times continuously differentiable.
-
-This is one of the easy parts of the inverse function theorem: it assumes that we already have
-an inverse function. -/
-theorem Homeomorph.contDiff_symm [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F}
-    (hf₀' : ∀ a, HasFDerivAt f (f₀' a : E →L[𝕜] F) a) (hf : ContDiff 𝕜 n (f : E → F)) :
-    ContDiff 𝕜 n (f.symm : F → E) :=
-  contDiff_iff_contDiffAt.2 fun x =>
-    f.toPartialHomeomorph.contDiffAt_symm (mem_univ x) (hf₀' _) hf.contDiffAt
-
-/-- Let `f` be a local homeomorphism of a nontrivially normed field, let `a` be a point in its
-target. if `f` is `n` times continuously differentiable at `f.symm a`, and if the derivative at
-`f.symm a` is nonzero, then `f.symm` is `n` times continuously differentiable at the point `a`.
-
-This is one of the easy parts of the inverse function theorem: it assumes that we already have
-an inverse function. -/
-theorem PartialHomeomorph.contDiffAt_symm_deriv [CompleteSpace 𝕜] (f : PartialHomeomorph 𝕜 𝕜)
-    {f₀' a : 𝕜} (h₀ : f₀' ≠ 0) (ha : a ∈ f.target) (hf₀' : HasDerivAt f f₀' (f.symm a))
-    (hf : ContDiffAt 𝕜 n f (f.symm a)) : ContDiffAt 𝕜 n f.symm a :=
-  f.contDiffAt_symm ha (hf₀'.hasFDerivAt_equiv h₀) hf
-
-/-- Let `f` be an `n` times continuously differentiable homeomorphism of a nontrivially normed
-field.  Suppose that the derivative of `f` is never equal to zero. Then `f.symm` is `n` times
-continuously differentiable.
-
-This is one of the easy parts of the inverse function theorem: it assumes that we already have
-an inverse function. -/
-theorem Homeomorph.contDiff_symm_deriv [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜}
-    (h₀ : ∀ x, f' x ≠ 0) (hf' : ∀ x, HasDerivAt f (f' x) x) (hf : ContDiff 𝕜 n (f : 𝕜 → 𝕜)) :
-    ContDiff 𝕜 n (f.symm : 𝕜 → 𝕜) :=
-  contDiff_iff_contDiffAt.2 fun x =>
-    f.toPartialHomeomorph.contDiffAt_symm_deriv (h₀ _) (mem_univ x) (hf' _) hf.contDiffAt
-
-namespace PartialHomeomorph
-
-variable (𝕜)
-
-/-- Restrict a partial homeomorphism to the subsets of the source and target
-that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
-such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.
-
-Note that `n` is a natural number or `ω`, but not `∞`,
-because the set of points of `C^∞`-smoothness of `f` is not guaranteed to be open. -/
-@[simps! apply symm_apply source target]
-def restrContDiff (f : PartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ∞) :
-    PartialHomeomorph E F :=
-  haveI H : f.IsImage {x | ContDiffAt 𝕜 n f x ∧ ContDiffAt 𝕜 n f.symm (f x)}
-      {y | ContDiffAt 𝕜 n f.symm y ∧ ContDiffAt 𝕜 n f (f.symm y)} := fun x hx ↦ by
-    simp [hx, and_comm]
-  H.restr <| isOpen_iff_mem_nhds.2 fun _ ⟨hxs, hxf, hxf'⟩ ↦
-    inter_mem (f.open_source.mem_nhds hxs) <| (hxf.eventually hn).and <|
-    f.continuousAt hxs (hxf'.eventually hn)
-
-lemma contDiffOn_restrContDiff_source (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
-    ContDiffOn 𝕜 n f (f.restrContDiff 𝕜 n hn).source := fun _x hx ↦ hx.2.1.contDiffWithinAt
-
-lemma contDiffOn_restrContDiff_target (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
-    ContDiffOn 𝕜 n f.symm (f.restrContDiff 𝕜 n hn).target := fun _x hx ↦ hx.2.1.contDiffWithinAt
-
-end PartialHomeomorph
-
-end FunctionInverse
-
 section deriv
 
 /-!
@@ -2084,59 +1333,3 @@ theorem ContDiff.iterate_deriv' (n : ℕ) :
   | k + 1, _, hf => ContDiff.iterate_deriv' _ k (contDiff_succ_iff_deriv.mp hf).2.2
 
 end deriv
-
-section RestrictScalars
-
-/-!
-### Restricting from `ℂ` to `ℝ`, or generally from `𝕜'` to `𝕜`
-
-If a function is `n` times continuously differentiable over `ℂ`, then it is `n` times continuously
-differentiable over `ℝ`. In this paragraph, we give variants of this statement, in the general
-situation where `ℂ` and `ℝ` are replaced respectively by `𝕜'` and `𝕜` where `𝕜'` is a normed algebra
-over `𝕜`.
--/
-
-
-variable (𝕜) {𝕜' : Type*} [NontriviallyNormedField 𝕜']
--- Porting note: this couldn't be on the same line as the binder type update of `𝕜`
-variable [NormedAlgebra 𝕜 𝕜']
-variable [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
-variable [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]
-variable {p' : E → FormalMultilinearSeries 𝕜' E F}
-
-theorem HasFTaylorSeriesUpToOn.restrictScalars {n : WithTop ℕ∞}
-    (h : HasFTaylorSeriesUpToOn n f p' s) :
-    HasFTaylorSeriesUpToOn n f (fun x => (p' x).restrictScalars 𝕜) s where
-  zero_eq x hx := h.zero_eq x hx
-  fderivWithin m hm x hx :=
-    set_option maxSynthPendingDepth 2 in
-    ((ContinuousMultilinearMap.restrictScalarsLinear 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x <|
-        (h.fderivWithin m hm x hx).restrictScalars 𝕜 :)
-  cont m hm := ContinuousMultilinearMap.continuous_restrictScalars.comp_continuousOn (h.cont m hm)
-
-theorem ContDiffWithinAt.restrict_scalars (h : ContDiffWithinAt 𝕜' n f s x) :
-    ContDiffWithinAt 𝕜 n f s x := by
-  match n with
-  | ω =>
-    obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
-    refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
-    change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u
-    apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)
-    exact ContinuousLinearMap.analyticOnNhd _ _
-  | (n : ℕ∞) =>
-    intro m hm
-    rcases h m hm with ⟨u, u_mem, p', hp'⟩
-    exact ⟨u, u_mem, _, hp'.restrictScalars _⟩
-
-theorem ContDiffOn.restrict_scalars (h : ContDiffOn 𝕜' n f s) : ContDiffOn 𝕜 n f s := fun x hx =>
-  (h x hx).restrict_scalars _
-
-theorem ContDiffAt.restrict_scalars (h : ContDiffAt 𝕜' n f x) : ContDiffAt 𝕜 n f x :=
-  contDiffWithinAt_univ.1 <| h.contDiffWithinAt.restrict_scalars _
-
-theorem ContDiff.restrict_scalars (h : ContDiff 𝕜' n f) : ContDiff 𝕜 n f :=
-  contDiff_iff_contDiffAt.2 fun _ => h.contDiffAt.restrict_scalars _
-
-end RestrictScalars
-
-set_option linter.style.longFile 2200
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
index c7ce7d8e91d48..863c507648a29 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Data.Finset.Sym
 import Mathlib.Data.Nat.Choose.Cast
 import Mathlib.Data.Nat.Choose.Multinomial
diff --git a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
index a403a0f90c9d8..4a02669fd7012 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Normed.Module.FiniteDimension
 
 /-!
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
new file mode 100644
index 0000000000000..70d8f5b772a72
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
@@ -0,0 +1,846 @@
+/-
+Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel, Floris van Doorn
+-/
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.Deriv.Inverse
+
+/-!
+# Higher differentiability of usual operations
+
+We prove that the usual operations (addition, multiplication, difference, composition, and
+so on) preserve `C^n` functions.
+
+## Notations
+
+We use the notation `E [×n]→L[𝕜] F` for the space of continuous multilinear maps on `E^n` with
+values in `F`. This is the space in which the `n`-th derivative of a function from `E` to `F` lives.
+
+In this file, we denote `(⊤ : ℕ∞) : WithTop ℕ∞` with `∞` and `⊤ : WithTop ℕ∞` with `ω`.
+
+## Tags
+
+derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor series, formal series
+-/
+
+open scoped NNReal Nat ContDiff
+
+universe u uE uF uG
+
+attribute [local instance 1001]
+  NormedAddCommGroup.toAddCommGroup AddCommGroup.toAddCommMonoid
+
+open Set Fin Filter Function
+
+open scoped Topology
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF}
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+  {X : Type*} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {s t : Set E} {f : E → F}
+  {g : F → G} {x x₀ : E} {b : E × F → G} {m n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F}
+
+/-!
+### Smoothness of functions `f : E → Π i, F' i`
+-/
+
+section Pi
+
+variable {ι ι' : Type*} [Fintype ι] [Fintype ι'] {F' : ι → Type*} [∀ i, NormedAddCommGroup (F' i)]
+  [∀ i, NormedSpace 𝕜 (F' i)] {φ : ∀ i, E → F' i} {p' : ∀ i, E → FormalMultilinearSeries 𝕜 E (F' i)}
+  {Φ : E → ∀ i, F' i} {P' : E → FormalMultilinearSeries 𝕜 E (∀ i, F' i)}
+
+theorem hasFTaylorSeriesUpToOn_pi {n : WithTop ℕ∞} :
+    HasFTaylorSeriesUpToOn n (fun x i => φ i x)
+        (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
+      ∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s := by
+  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
+  set L : ∀ m : ℕ, (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i := fun m =>
+    ContinuousMultilinearMap.piₗᵢ _ _
+  refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
+  · exact h.continuousLinearMap_comp (pr i)
+  · ext1 i
+    exact (h i).zero_eq x hx
+  · intro m hm x hx
+    exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
+      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx
+  · intro m hm
+    exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm
+
+@[simp]
+theorem hasFTaylorSeriesUpToOn_pi' {n : WithTop ℕ∞} :
+    HasFTaylorSeriesUpToOn n Φ P' s ↔
+      ∀ i, HasFTaylorSeriesUpToOn n (fun x => Φ x i)
+        (fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap
+          (P' x m)) s := by
+  convert hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i); ext; rfl
+
+theorem contDiffWithinAt_pi :
+    ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x := by
+  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
+  refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
+  match n with
+  | ω =>
+    choose u hux p hp h'p using h
+    refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
+      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
+    set L : (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i :=
+      ContinuousMultilinearMap.piₗᵢ _ _
+    change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
+    apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
+    exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
+  | (n : ℕ∞) =>
+    intro m hm
+    choose u hux p hp using fun i => h i m hm
+    exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
+      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩
+
+theorem contDiffOn_pi : ContDiffOn 𝕜 n Φ s ↔ ∀ i, ContDiffOn 𝕜 n (fun x => Φ x i) s :=
+  ⟨fun h _ x hx => contDiffWithinAt_pi.1 (h x hx) _, fun h x hx =>
+    contDiffWithinAt_pi.2 fun i => h i x hx⟩
+
+theorem contDiffAt_pi : ContDiffAt 𝕜 n Φ x ↔ ∀ i, ContDiffAt 𝕜 n (fun x => Φ x i) x :=
+  contDiffWithinAt_pi
+
+theorem contDiff_pi : ContDiff 𝕜 n Φ ↔ ∀ i, ContDiff 𝕜 n fun x => Φ x i := by
+  simp only [← contDiffOn_univ, contDiffOn_pi]
+
+theorem contDiff_update [DecidableEq ι] (k : WithTop ℕ∞) (x : ∀ i, F' i) (i : ι) :
+    ContDiff 𝕜 k (update x i) := by
+  rw [contDiff_pi]
+  intro j
+  dsimp [Function.update]
+  split_ifs with h
+  · subst h
+    exact contDiff_id
+  · exact contDiff_const
+
+variable (F') in
+theorem contDiff_single [DecidableEq ι] (k : WithTop ℕ∞) (i : ι) :
+    ContDiff 𝕜 k (Pi.single i : F' i → ∀ i, F' i) :=
+  contDiff_update k 0 i
+
+variable (𝕜 E)
+
+theorem contDiff_apply (i : ι) : ContDiff 𝕜 n fun f : ι → E => f i :=
+  contDiff_pi.mp contDiff_id i
+
+theorem contDiff_apply_apply (i : ι) (j : ι') : ContDiff 𝕜 n fun f : ι → ι' → E => f i j :=
+  contDiff_pi.mp (contDiff_apply 𝕜 (ι' → E) i) j
+
+end Pi
+
+/-! ### Sum of two functions -/
+
+section Add
+
+theorem HasFTaylorSeriesUpToOn.add {n : WithTop ℕ∞} {q g} (hf : HasFTaylorSeriesUpToOn n f p s)
+    (hg : HasFTaylorSeriesUpToOn n g q s) : HasFTaylorSeriesUpToOn n (f + g) (p + q) s := by
+  exact HasFTaylorSeriesUpToOn.continuousLinearMap_comp
+    (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F) (hf.prod hg)
+
+-- The sum is smooth.
+theorem contDiff_add : ContDiff 𝕜 n fun p : F × F => p.1 + p.2 :=
+  (IsBoundedLinearMap.fst.add IsBoundedLinearMap.snd).contDiff
+
+/-- The sum of two `C^n` functions within a set at a point is `C^n` within this set
+at this point. -/
+theorem ContDiffWithinAt.add {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
+    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x :=
+  contDiff_add.contDiffWithinAt.comp x (hf.prod hg) subset_preimage_univ
+
+/-- The sum of two `C^n` functions at a point is `C^n` at this point. -/
+theorem ContDiffAt.add {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
+    ContDiffAt 𝕜 n (fun x => f x + g x) x := by
+  rw [← contDiffWithinAt_univ] at *; exact hf.add hg
+
+/-- The sum of two `C^n`functions is `C^n`. -/
+theorem ContDiff.add {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+    ContDiff 𝕜 n fun x => f x + g x :=
+  contDiff_add.comp (hf.prod hg)
+
+/-- The sum of two `C^n` functions on a domain is `C^n`. -/
+theorem ContDiffOn.add {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
+    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x + g x) s := fun x hx =>
+  (hf x hx).add (hg x hx)
+
+variable {i : ℕ}
+
+/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
+See also `iteratedFDerivWithin_add_apply'`, which uses the spelling `(fun x ↦ f x + g x)`
+instead of `f + g`. -/
+theorem iteratedFDerivWithin_add_apply {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x)
+    (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
+    iteratedFDerivWithin 𝕜 i (f + g) s x =
+      iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x := by
+  have := (hf.eventually (by simp)).and (hg.eventually (by simp))
+  obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
+  have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
+  have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
+  have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
+  have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
+    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
+  rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
+    ← iteratedFDerivWithin_congr_set H]
+  exact .symm (((hft.ftaylorSeriesWithin hut).add
+      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)
+
+/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
+This is the same as `iteratedFDerivWithin_add_apply`, but using the spelling `(fun x ↦ f x + g x)`
+instead of `f + g`, which can be handy for some rewrites.
+TODO: use one form consistently. -/
+theorem iteratedFDerivWithin_add_apply' {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x)
+    (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
+    iteratedFDerivWithin 𝕜 i (fun x => f x + g x) s x =
+      iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x :=
+  iteratedFDerivWithin_add_apply hf hg hu hx
+
+theorem iteratedFDeriv_add_apply {i : ℕ} {f g : E → F}
+    (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
+    iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x := by
+  simp_rw [← iteratedFDerivWithin_univ]
+  exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)
+
+theorem iteratedFDeriv_add_apply' {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 i f x)
+    (hg : ContDiffAt 𝕜 i g x) :
+    iteratedFDeriv 𝕜 i (fun x => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x :=
+  iteratedFDeriv_add_apply hf hg
+
+end Add
+
+/-! ### Negative -/
+
+section Neg
+
+-- The negative is smooth.
+theorem contDiff_neg : ContDiff 𝕜 n fun p : F => -p :=
+  IsBoundedLinearMap.id.neg.contDiff
+
+/-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
+this point. -/
+theorem ContDiffWithinAt.neg {s : Set E} {f : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) :
+    ContDiffWithinAt 𝕜 n (fun x => -f x) s x :=
+  contDiff_neg.contDiffWithinAt.comp x hf subset_preimage_univ
+
+/-- The negative of a `C^n` function at a point is `C^n` at this point. -/
+theorem ContDiffAt.neg {f : E → F} (hf : ContDiffAt 𝕜 n f x) :
+    ContDiffAt 𝕜 n (fun x => -f x) x := by rw [← contDiffWithinAt_univ] at *; exact hf.neg
+
+/-- The negative of a `C^n`function is `C^n`. -/
+theorem ContDiff.neg {f : E → F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => -f x :=
+  contDiff_neg.comp hf
+
+/-- The negative of a `C^n` function on a domain is `C^n`. -/
+theorem ContDiffOn.neg {s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) :
+    ContDiffOn 𝕜 n (fun x => -f x) s := fun x hx => (hf x hx).neg
+
+variable {i : ℕ}
+
+-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: define `Neg` instance on `ContinuousLinearEquiv`,
+-- prove it from `ContinuousLinearEquiv.iteratedFDerivWithin_comp_left`
+theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
+    iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x := by
+  induction' i with i hi generalizing x
+  · ext; simp
+  · ext h
+    calc
+      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
+          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
+        rfl
+      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
+        rw [fderivWithin_congr' (@hi) hx]; rfl
+      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
+        rw [Pi.neg_def, fderivWithin_neg (hu x hx)]; rfl
+      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := rfl
+
+theorem iteratedFDeriv_neg_apply {i : ℕ} {f : E → F} :
+    iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x := by
+  simp_rw [← iteratedFDerivWithin_univ]
+  exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)
+
+end Neg
+
+/-! ### Subtraction -/
+
+/-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
+at this point. -/
+theorem ContDiffWithinAt.sub {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
+    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x := by
+  simpa only [sub_eq_add_neg] using hf.add hg.neg
+
+/-- The difference of two `C^n` functions at a point is `C^n` at this point. -/
+theorem ContDiffAt.sub {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
+    ContDiffAt 𝕜 n (fun x => f x - g x) x := by simpa only [sub_eq_add_neg] using hf.add hg.neg
+
+/-- The difference of two `C^n` functions on a domain is `C^n`. -/
+theorem ContDiffOn.sub {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
+    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x - g x) s := by
+  simpa only [sub_eq_add_neg] using hf.add hg.neg
+
+/-- The difference of two `C^n` functions is `C^n`. -/
+theorem ContDiff.sub {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+    ContDiff 𝕜 n fun x => f x - g x := by simpa only [sub_eq_add_neg] using hf.add hg.neg
+
+/-! ### Sum of finitely many functions -/
+
+theorem ContDiffWithinAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E}
+    (h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x) :
+    ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x := by
+  classical
+    induction' s using Finset.induction_on with i s is IH
+    · simp [contDiffWithinAt_const]
+    · simp only [is, Finset.sum_insert, not_false_iff]
+      exact (h _ (Finset.mem_insert_self i s)).add
+        (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
+
+theorem ContDiffAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {x : E}
+    (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) :
+    ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x := by
+  rw [← contDiffWithinAt_univ] at *; exact ContDiffWithinAt.sum h
+
+theorem ContDiffOn.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E}
+    (h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t) :
+    ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t := fun x hx =>
+  ContDiffWithinAt.sum fun i hi => h i hi x hx
+
+theorem ContDiff.sum {ι : Type*} {f : ι → E → F} {s : Finset ι}
+    (h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) : ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x := by
+  simp only [← contDiffOn_univ] at *; exact ContDiffOn.sum h
+
+theorem iteratedFDerivWithin_sum_apply {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E}
+    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 i (f j) s x) :
+    iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j ·) s x =
+      ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x := by
+  induction u using Finset.cons_induction with
+  | empty => ext; simp [hs, hx]
+  | cons a u ha IH =>
+    simp only [Finset.mem_cons, forall_eq_or_imp] at h
+    simp only [Finset.sum_cons]
+    rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]
+
+theorem iteratedFDeriv_sum {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ}
+    (h : ∀ j ∈ u, ContDiff 𝕜 i (f j)) :
+    iteratedFDeriv 𝕜 i (∑ j ∈ u, f j ·) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j) :=
+  funext fun x ↦ by simpa [iteratedFDerivWithin_univ] using
+    iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (mem_univ x) (h · · |>.contDiffWithinAt)
+
+/-! ### Product of two functions -/
+
+section MulProd
+
+variable {𝔸 𝔸' ι 𝕜' : Type*} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [NormedCommRing 𝔸']
+  [NormedAlgebra 𝕜 𝔸'] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+
+-- The product is smooth.
+theorem contDiff_mul : ContDiff 𝕜 n fun p : 𝔸 × 𝔸 => p.1 * p.2 :=
+  (ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.contDiff
+
+/-- The product of two `C^n` functions within a set at a point is `C^n` within this set
+at this point. -/
+theorem ContDiffWithinAt.mul {s : Set E} {f g : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x)
+    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x :=
+  contDiff_mul.comp_contDiffWithinAt (hf.prod hg)
+
+/-- The product of two `C^n` functions at a point is `C^n` at this point. -/
+nonrec theorem ContDiffAt.mul {f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
+    ContDiffAt 𝕜 n (fun x => f x * g x) x :=
+  hf.mul hg
+
+/-- The product of two `C^n` functions on a domain is `C^n`. -/
+theorem ContDiffOn.mul {f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
+    ContDiffOn 𝕜 n (fun x => f x * g x) s := fun x hx => (hf x hx).mul (hg x hx)
+
+/-- The product of two `C^n`functions is `C^n`. -/
+theorem ContDiff.mul {f g : E → 𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+    ContDiff 𝕜 n fun x => f x * g x :=
+  contDiff_mul.comp (hf.prod hg)
+
+theorem contDiffWithinAt_prod' {t : Finset ι} {f : ι → E → 𝔸'}
+    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x :=
+  Finset.prod_induction f (fun f => ContDiffWithinAt 𝕜 n f s x) (fun _ _ => ContDiffWithinAt.mul)
+    (contDiffWithinAt_const (c := 1)) h
+
+theorem contDiffWithinAt_prod {t : Finset ι} {f : ι → E → 𝔸'}
+    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) :
+    ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x := by
+  simpa only [← Finset.prod_apply] using contDiffWithinAt_prod' h
+
+theorem contDiffAt_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
+    ContDiffAt 𝕜 n (∏ i ∈ t, f i) x :=
+  contDiffWithinAt_prod' h
+
+theorem contDiffAt_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
+    ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x :=
+  contDiffWithinAt_prod h
+
+theorem contDiffOn_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
+    ContDiffOn 𝕜 n (∏ i ∈ t, f i) s := fun x hx => contDiffWithinAt_prod' fun i hi => h i hi x hx
+
+theorem contDiffOn_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
+    ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s := fun x hx =>
+  contDiffWithinAt_prod fun i hi => h i hi x hx
+
+theorem contDiff_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
+    ContDiff 𝕜 n (∏ i ∈ t, f i) :=
+  contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod' fun i hi => (h i hi).contDiffAt
+
+theorem contDiff_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
+    ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y :=
+  contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod fun i hi => (h i hi).contDiffAt
+
+theorem ContDiff.pow {f : E → 𝔸} (hf : ContDiff 𝕜 n f) : ∀ m : ℕ, ContDiff 𝕜 n fun x => f x ^ m
+  | 0 => by simpa using contDiff_const
+  | m + 1 => by simpa [pow_succ] using (hf.pow m).mul hf
+
+theorem ContDiffWithinAt.pow {f : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (m : ℕ) :
+    ContDiffWithinAt 𝕜 n (fun y => f y ^ m) s x :=
+  (contDiff_id.pow m).comp_contDiffWithinAt hf
+
+nonrec theorem ContDiffAt.pow {f : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (m : ℕ) :
+    ContDiffAt 𝕜 n (fun y => f y ^ m) x :=
+  hf.pow m
+
+theorem ContDiffOn.pow {f : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (m : ℕ) :
+    ContDiffOn 𝕜 n (fun y => f y ^ m) s := fun y hy => (hf y hy).pow m
+
+theorem ContDiffWithinAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') :
+    ContDiffWithinAt 𝕜 n (fun x => f x / c) s x := by
+  simpa only [div_eq_mul_inv] using hf.mul contDiffWithinAt_const
+
+nonrec theorem ContDiffAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffAt 𝕜 n f x) (c : 𝕜') :
+    ContDiffAt 𝕜 n (fun x => f x / c) x :=
+  hf.div_const c
+
+theorem ContDiffOn.div_const {f : E → 𝕜'} {n} (hf : ContDiffOn 𝕜 n f s) (c : 𝕜') :
+    ContDiffOn 𝕜 n (fun x => f x / c) s := fun x hx => (hf x hx).div_const c
+
+theorem ContDiff.div_const {f : E → 𝕜'} {n} (hf : ContDiff 𝕜 n f) (c : 𝕜') :
+    ContDiff 𝕜 n fun x => f x / c := by simpa only [div_eq_mul_inv] using hf.mul contDiff_const
+
+end MulProd
+
+/-! ### Scalar multiplication -/
+
+section SMul
+
+-- The scalar multiplication is smooth.
+theorem contDiff_smul : ContDiff 𝕜 n fun p : 𝕜 × F => p.1 • p.2 :=
+  isBoundedBilinearMap_smul.contDiff
+
+/-- The scalar multiplication of two `C^n` functions within a set at a point is `C^n` within this
+set at this point. -/
+theorem ContDiffWithinAt.smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
+    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x • g x) s x :=
+  contDiff_smul.contDiffWithinAt.comp x (hf.prod hg) subset_preimage_univ
+
+/-- The scalar multiplication of two `C^n` functions at a point is `C^n` at this point. -/
+theorem ContDiffAt.smul {f : E → 𝕜} {g : E → F} (hf : ContDiffAt 𝕜 n f x)
+    (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x • g x) x := by
+  rw [← contDiffWithinAt_univ] at *; exact hf.smul hg
+
+/-- The scalar multiplication of two `C^n` functions is `C^n`. -/
+theorem ContDiff.smul {f : E → 𝕜} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+    ContDiff 𝕜 n fun x => f x • g x :=
+  contDiff_smul.comp (hf.prod hg)
+
+/-- The scalar multiplication of two `C^n` functions on a domain is `C^n`. -/
+theorem ContDiffOn.smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffOn 𝕜 n f s)
+    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x • g x) s := fun x hx =>
+  (hf x hx).smul (hg x hx)
+
+end SMul
+
+/-! ### Constant scalar multiplication
+
+Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: generalize results in this section.
+
+1. It should be possible to assume `[Monoid R] [DistribMulAction R F] [SMulCommClass 𝕜 R F]`.
+2. If `c` is a unit (or `R` is a group), then one can drop `ContDiff*` assumptions in some
+  lemmas.
+-/
+
+section ConstSMul
+
+variable {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F]
+variable [ContinuousConstSMul R F]
+
+-- The scalar multiplication with a constant is smooth.
+theorem contDiff_const_smul (c : R) : ContDiff 𝕜 n fun p : F => c • p :=
+  (c • ContinuousLinearMap.id 𝕜 F).contDiff
+
+/-- The scalar multiplication of a constant and a `C^n` function within a set at a point is `C^n`
+within this set at this point. -/
+theorem ContDiffWithinAt.const_smul {s : Set E} {f : E → F} {x : E} (c : R)
+    (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun y => c • f y) s x :=
+  (contDiff_const_smul c).contDiffAt.comp_contDiffWithinAt x hf
+
+/-- The scalar multiplication of a constant and a `C^n` function at a point is `C^n` at this
+point. -/
+theorem ContDiffAt.const_smul {f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) :
+    ContDiffAt 𝕜 n (fun y => c • f y) x := by
+  rw [← contDiffWithinAt_univ] at *; exact hf.const_smul c
+
+/-- The scalar multiplication of a constant and a `C^n` function is `C^n`. -/
+theorem ContDiff.const_smul {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
+    ContDiff 𝕜 n fun y => c • f y :=
+  (contDiff_const_smul c).comp hf
+
+/-- The scalar multiplication of a constant and a `C^n` on a domain is `C^n`. -/
+theorem ContDiffOn.const_smul {s : Set E} {f : E → F} (c : R) (hf : ContDiffOn 𝕜 n f s) :
+    ContDiffOn 𝕜 n (fun y => c • f y) s := fun x hx => (hf x hx).const_smul c
+
+variable {i : ℕ} {a : R}
+
+theorem iteratedFDerivWithin_const_smul_apply (hf : ContDiffWithinAt 𝕜 i f s x)
+    (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
+    iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x :=
+  (a • (1 : F →L[𝕜] F)).iteratedFDerivWithin_comp_left hf hu hx le_rfl
+
+theorem iteratedFDeriv_const_smul_apply (hf : ContDiffAt 𝕜 i f x) :
+    iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x :=
+  (a • (1 : F →L[𝕜] F)).iteratedFDeriv_comp_left hf le_rfl
+
+theorem iteratedFDeriv_const_smul_apply' (hf : ContDiffAt 𝕜 i f x) :
+    iteratedFDeriv 𝕜 i (fun x ↦ a • f x) x = a • iteratedFDeriv 𝕜 i f x :=
+  iteratedFDeriv_const_smul_apply hf
+
+end ConstSMul
+
+/-! ### Cartesian product of two functions -/
+
+section prodMap
+
+variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+variable {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
+
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+theorem ContDiffWithinAt.prod_map' {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {p : E × E'}
+    (hf : ContDiffWithinAt 𝕜 n f s p.1) (hg : ContDiffWithinAt 𝕜 n g t p.2) :
+    ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p :=
+  (hf.comp p contDiffWithinAt_fst (prod_subset_preimage_fst _ _)).prod
+    (hg.comp p contDiffWithinAt_snd (prod_subset_preimage_snd _ _))
+
+theorem ContDiffWithinAt.prod_map {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {x : E}
+    {y : E'} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g t y) :
+    ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y) :=
+  ContDiffWithinAt.prod_map' hf hg
+
+/-- The product map of two `C^n` functions on a set is `C^n` on the product set. -/
+theorem ContDiffOn.prod_map {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type*}
+    [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'}
+    (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g t) : ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t) :=
+  (hf.comp contDiffOn_fst (prod_subset_preimage_fst _ _)).prod
+    (hg.comp contDiffOn_snd (prod_subset_preimage_snd _ _))
+
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+theorem ContDiffAt.prod_map {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffAt 𝕜 n f x)
+    (hg : ContDiffAt 𝕜 n g y) : ContDiffAt 𝕜 n (Prod.map f g) (x, y) := by
+  rw [ContDiffAt] at *
+  convert hf.prod_map hg
+  simp only [univ_prod_univ]
+
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+theorem ContDiffAt.prod_map' {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffAt 𝕜 n f p.1)
+    (hg : ContDiffAt 𝕜 n g p.2) : ContDiffAt 𝕜 n (Prod.map f g) p := by
+  rcases p with ⟨⟩
+  exact ContDiffAt.prod_map hf hg
+
+/-- The product map of two `C^n` functions is `C^n`. -/
+theorem ContDiff.prod_map {f : E → F} {g : E' → F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+    ContDiff 𝕜 n (Prod.map f g) := by
+  rw [contDiff_iff_contDiffAt] at *
+  exact fun ⟨x, y⟩ => (hf x).prod_map (hg y)
+
+theorem contDiff_prod_mk_left (f₀ : F) : ContDiff 𝕜 n fun e : E => (e, f₀) :=
+  contDiff_id.prod contDiff_const
+
+theorem contDiff_prod_mk_right (e₀ : E) : ContDiff 𝕜 n fun f : F => (e₀, f) :=
+  contDiff_const.prod contDiff_id
+
+end prodMap
+
+/-!
+### Inversion in a complete normed algebra (or more generally with summable geometric series)
+-/
+
+section AlgebraInverse
+
+variable (𝕜)
+variable {R : Type*} [NormedRing R] [NormedAlgebra 𝕜 R]
+
+open NormedRing ContinuousLinearMap Ring
+
+/-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
+invertible element, as it is analytic. -/
+theorem contDiffAt_ring_inverse [HasSummableGeomSeries R] (x : Rˣ) :
+    ContDiffAt 𝕜 n Ring.inverse (x : R) := by
+  have := AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n)
+    Units.isOpen.uniqueDiffOn x x.isUnit
+  exact this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)
+
+variable {𝕜' : Type*} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+
+theorem contDiffAt_inv {x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.inv x := by
+  simpa only [Ring.inverse_eq_inv'] using contDiffAt_ring_inverse 𝕜 (Units.mk0 x hx)
+
+theorem contDiffOn_inv {n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') {0}ᶜ := fun _ hx =>
+  (contDiffAt_inv 𝕜 hx).contDiffWithinAt
+
+variable {𝕜}
+
+theorem ContDiffWithinAt.inv {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) :
+    ContDiffWithinAt 𝕜 n (fun x => (f x)⁻¹) s x :=
+  (contDiffAt_inv 𝕜 hx).comp_contDiffWithinAt x hf
+
+theorem ContDiffOn.inv {f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) :
+    ContDiffOn 𝕜 n (fun x => (f x)⁻¹) s := fun x hx => (hf.contDiffWithinAt hx).inv (h x hx)
+
+nonrec theorem ContDiffAt.inv {f : E → 𝕜'} (hf : ContDiffAt 𝕜 n f x) (hx : f x ≠ 0) :
+    ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x :=
+  hf.inv hx
+
+theorem ContDiff.inv {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ x, f x ≠ 0) :
+    ContDiff 𝕜 n fun x => (f x)⁻¹ := by
+  rw [contDiff_iff_contDiffAt]; exact fun x => hf.contDiffAt.inv (h x)
+
+-- TODO: generalize to `f g : E → 𝕜'`
+theorem ContDiffWithinAt.div {f g : E → 𝕜} {n} (hf : ContDiffWithinAt 𝕜 n f s x)
+    (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) :
+    ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x := by
+  simpa only [div_eq_mul_inv] using hf.mul (hg.inv hx)
+
+theorem ContDiffOn.div {f g : E → 𝕜} {n} (hf : ContDiffOn 𝕜 n f s)
+    (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContDiffOn 𝕜 n (f / g) s := fun x hx =>
+  (hf x hx).div (hg x hx) (h₀ x hx)
+
+nonrec theorem ContDiffAt.div {f g : E → 𝕜} {n} (hf : ContDiffAt 𝕜 n f x)
+    (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) : ContDiffAt 𝕜 n (fun x => f x / g x) x :=
+  hf.div hg hx
+
+theorem ContDiff.div {f g : E → 𝕜} {n} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g)
+    (h0 : ∀ x, g x ≠ 0) : ContDiff 𝕜 n fun x => f x / g x := by
+  simp only [contDiff_iff_contDiffAt] at *
+  exact fun x => (hf x).div (hg x) (h0 x)
+
+end AlgebraInverse
+
+/-! ### Inversion of continuous linear maps between Banach spaces -/
+
+section MapInverse
+
+open ContinuousLinearMap
+
+/-- At a continuous linear equivalence `e : E ≃L[𝕜] F` between Banach spaces, the operation of
+inversion is `C^n`, for all `n`. -/
+theorem contDiffAt_map_inverse [CompleteSpace E] (e : E ≃L[𝕜] F) :
+    ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F) := by
+  nontriviality E
+  -- first, we use the lemma `to_ring_inverse` to rewrite in terms of `Ring.inverse` in the ring
+  -- `E →L[𝕜] E`
+  let O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp (e.symm : F →L[𝕜] E)
+  let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
+  have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (to_ring_inverse e)
+  rw [this]
+  -- `O₁` and `O₂` are `ContDiff`,
+  -- so we reduce to proving that `Ring.inverse` is `ContDiff`
+  have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
+  have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
+  refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)
+  convert contDiffAt_ring_inverse 𝕜 (1 : (E →L[𝕜] E)ˣ)
+  simp [O₂, one_def]
+
+/-- At an invertible map `e : M →L[R] M₂` between Banach spaces, the operation of
+inversion is `C^n`, for all `n`. -/
+theorem ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse [CompleteSpace E] {e : E →L[𝕜] F}
+    (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e := by
+  rcases he with ⟨M, rfl⟩
+  exact _root_.contDiffAt_map_inverse M
+
+end MapInverse
+
+section FunctionInverse
+
+open ContinuousLinearMap
+
+/-- If `f` is a local homeomorphism and the point `a` is in its target,
+and if `f` is `n` times continuously differentiable at `f.symm a`,
+and if the derivative at `f.symm a` is a continuous linear equivalence,
+then `f.symm` is `n` times continuously differentiable at the point `a`.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem PartialHomeomorph.contDiffAt_symm [CompleteSpace E] (f : PartialHomeomorph E F)
+    {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
+    (hf₀' : HasFDerivAt f (f₀' : E →L[𝕜] F) (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) :
+    ContDiffAt 𝕜 n f.symm a := by
+  match n with
+  | ω =>
+    apply AnalyticAt.contDiffAt
+    exact f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv
+  | (n : ℕ∞) =>
+    -- We prove this by induction on `n`
+    induction' n using ENat.nat_induction with n IH Itop
+    · apply contDiffAt_zero.2
+      exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
+    · obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
+      apply contDiffAt_succ_iff_hasFDerivAt.2
+      -- For showing `n.succ` times continuous differentiability (the main inductive step), it
+      -- suffices to produce the derivative and show that it is `n` times continuously
+      -- differentiable
+      have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
+      -- This follows by a bootstrapping formula expressing the derivative as a
+      -- function of `f` itself
+      refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
+      · -- We first check that the derivative of `f` is that formula
+        have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
+          have hf₀' := f₀'.nhds
+          rw [← eq_f₀'] at hf₀'
+          exact hf'.continuousAt.preimage_mem_nhds hf₀'
+        obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
+        use f.target ∩ f.symm ⁻¹' t
+        refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
+        · exact f.isOpen_inter_preimage_symm ht
+        · exact mem_inter ha (mem_preimage.mpr htf)
+        intro x hx
+        obtain ⟨hxu, e, he⟩ := htu hx.2
+        have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
+          rw [he]
+          exact hff' (f.symm x) hxu
+        convert f.hasFDerivAt_symm hx.1 h_deriv
+        simp [← he]
+      · -- Then we check that the formula, being a composition of `ContDiff` pieces, is
+        -- itself `ContDiff`
+        have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
+          rw [eq_f₀']
+          exact contDiffAt_map_inverse _
+        have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
+          refine IH (hf.of_le ?_)
+          norm_cast
+          exact Nat.le_succ n
+        exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
+    · refine contDiffAt_infty.mpr ?_
+      intro n
+      exact Itop n (contDiffAt_infty.mp hf n)
+
+/-- If `f` is an `n` times continuously differentiable homeomorphism,
+and if the derivative of `f` at each point is a continuous linear equivalence,
+then `f.symm` is `n` times continuously differentiable.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem Homeomorph.contDiff_symm [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F}
+    (hf₀' : ∀ a, HasFDerivAt f (f₀' a : E →L[𝕜] F) a) (hf : ContDiff 𝕜 n (f : E → F)) :
+    ContDiff 𝕜 n (f.symm : F → E) :=
+  contDiff_iff_contDiffAt.2 fun x =>
+    f.toPartialHomeomorph.contDiffAt_symm (mem_univ x) (hf₀' _) hf.contDiffAt
+
+/-- Let `f` be a local homeomorphism of a nontrivially normed field, let `a` be a point in its
+target. if `f` is `n` times continuously differentiable at `f.symm a`, and if the derivative at
+`f.symm a` is nonzero, then `f.symm` is `n` times continuously differentiable at the point `a`.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem PartialHomeomorph.contDiffAt_symm_deriv [CompleteSpace 𝕜] (f : PartialHomeomorph 𝕜 𝕜)
+    {f₀' a : 𝕜} (h₀ : f₀' ≠ 0) (ha : a ∈ f.target) (hf₀' : HasDerivAt f f₀' (f.symm a))
+    (hf : ContDiffAt 𝕜 n f (f.symm a)) : ContDiffAt 𝕜 n f.symm a :=
+  f.contDiffAt_symm ha (hf₀'.hasFDerivAt_equiv h₀) hf
+
+/-- Let `f` be an `n` times continuously differentiable homeomorphism of a nontrivially normed
+field.  Suppose that the derivative of `f` is never equal to zero. Then `f.symm` is `n` times
+continuously differentiable.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem Homeomorph.contDiff_symm_deriv [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜}
+    (h₀ : ∀ x, f' x ≠ 0) (hf' : ∀ x, HasDerivAt f (f' x) x) (hf : ContDiff 𝕜 n (f : 𝕜 → 𝕜)) :
+    ContDiff 𝕜 n (f.symm : 𝕜 → 𝕜) :=
+  contDiff_iff_contDiffAt.2 fun x =>
+    f.toPartialHomeomorph.contDiffAt_symm_deriv (h₀ _) (mem_univ x) (hf' _) hf.contDiffAt
+
+namespace PartialHomeomorph
+
+variable (𝕜)
+
+/-- Restrict a partial homeomorphism to the subsets of the source and target
+that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
+such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.
+
+Note that `n` is a natural number or `ω`, but not `∞`,
+because the set of points of `C^∞`-smoothness of `f` is not guaranteed to be open. -/
+@[simps! apply symm_apply source target]
+def restrContDiff (f : PartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ∞) :
+    PartialHomeomorph E F :=
+  haveI H : f.IsImage {x | ContDiffAt 𝕜 n f x ∧ ContDiffAt 𝕜 n f.symm (f x)}
+      {y | ContDiffAt 𝕜 n f.symm y ∧ ContDiffAt 𝕜 n f (f.symm y)} := fun x hx ↦ by
+    simp [hx, and_comm]
+  H.restr <| isOpen_iff_mem_nhds.2 fun _ ⟨hxs, hxf, hxf'⟩ ↦
+    inter_mem (f.open_source.mem_nhds hxs) <| (hxf.eventually hn).and <|
+    f.continuousAt hxs (hxf'.eventually hn)
+
+lemma contDiffOn_restrContDiff_source (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
+    ContDiffOn 𝕜 n f (f.restrContDiff 𝕜 n hn).source := fun _x hx ↦ hx.2.1.contDiffWithinAt
+
+lemma contDiffOn_restrContDiff_target (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
+    ContDiffOn 𝕜 n f.symm (f.restrContDiff 𝕜 n hn).target := fun _x hx ↦ hx.2.1.contDiffWithinAt
+
+end PartialHomeomorph
+
+end FunctionInverse
+
+section RestrictScalars
+
+/-!
+### Restricting from `ℂ` to `ℝ`, or generally from `𝕜'` to `𝕜`
+
+If a function is `n` times continuously differentiable over `ℂ`, then it is `n` times continuously
+differentiable over `ℝ`. In this paragraph, we give variants of this statement, in the general
+situation where `ℂ` and `ℝ` are replaced respectively by `𝕜'` and `𝕜` where `𝕜'` is a normed algebra
+over `𝕜`.
+-/
+
+
+variable (𝕜) {𝕜' : Type*} [NontriviallyNormedField 𝕜']
+-- Porting note: this couldn't be on the same line as the binder type update of `𝕜`
+variable [NormedAlgebra 𝕜 𝕜']
+variable [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
+variable [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]
+variable {p' : E → FormalMultilinearSeries 𝕜' E F}
+
+theorem HasFTaylorSeriesUpToOn.restrictScalars {n : WithTop ℕ∞}
+    (h : HasFTaylorSeriesUpToOn n f p' s) :
+    HasFTaylorSeriesUpToOn n f (fun x => (p' x).restrictScalars 𝕜) s where
+  zero_eq x hx := h.zero_eq x hx
+  fderivWithin m hm x hx :=
+    set_option maxSynthPendingDepth 2 in
+    ((ContinuousMultilinearMap.restrictScalarsLinear 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x <|
+        (h.fderivWithin m hm x hx).restrictScalars 𝕜 :)
+  cont m hm := ContinuousMultilinearMap.continuous_restrictScalars.comp_continuousOn (h.cont m hm)
+
+theorem ContDiffWithinAt.restrict_scalars (h : ContDiffWithinAt 𝕜' n f s x) :
+    ContDiffWithinAt 𝕜 n f s x := by
+  match n with
+  | ω =>
+    obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
+    refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
+    change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u
+    apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)
+    exact ContinuousLinearMap.analyticOnNhd _ _
+  | (n : ℕ∞) =>
+    intro m hm
+    rcases h m hm with ⟨u, u_mem, p', hp'⟩
+    exact ⟨u, u_mem, _, hp'.restrictScalars _⟩
+
+theorem ContDiffOn.restrict_scalars (h : ContDiffOn 𝕜' n f s) : ContDiffOn 𝕜 n f s := fun x hx =>
+  (h x hx).restrict_scalars _
+
+theorem ContDiffAt.restrict_scalars (h : ContDiffAt 𝕜' n f x) : ContDiffAt 𝕜 n f x :=
+  contDiffWithinAt_univ.1 <| h.contDiffWithinAt.restrict_scalars _
+
+theorem ContDiff.restrict_scalars (h : ContDiff 𝕜' n f) : ContDiff 𝕜 n f :=
+  contDiff_iff_contDiffAt.2 fun _ => h.contDiffAt.restrict_scalars _
+
+end RestrictScalars
diff --git a/Mathlib/Analysis/Calculus/ContDiff/WithLp.lean b/Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
index 7c1f15c0a1dd3..9e57126bca7ae 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker, Eric Wieser
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Normed.Lp.PiLp
 
 /-!
diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean
index f52e49644ceda..62ca036ff5c2f 100644
--- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean
+++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.ContDiff.RCLike
 import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
 
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
index 5de876630e0b3..190b211d1434c 100644
--- a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
+++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck, Ruben Van de Velde
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Shift
 import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
diff --git a/Mathlib/Analysis/Calculus/SmoothSeries.lean b/Mathlib/Analysis/Calculus/SmoothSeries.lean
index 734dd58db15a3..943712c5e4dd7 100644
--- a/Mathlib/Analysis/Calculus/SmoothSeries.lean
+++ b/Mathlib/Analysis/Calculus/SmoothSeries.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.UniformLimitsDeriv
 import Mathlib.Topology.Algebra.InfiniteSum.Module
 import Mathlib.Analysis.NormedSpace.FunctionSeries
diff --git a/Mathlib/Analysis/Complex/RealDeriv.lean b/Mathlib/Analysis/Complex/RealDeriv.lean
index 3d214cf595f51..51c963c0e4eb7 100644
--- a/Mathlib/Analysis/Complex/RealDeriv.lean
+++ b/Mathlib/Analysis/Complex/RealDeriv.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yourong Zang
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.Deriv.Linear
 import Mathlib.Analysis.Complex.Basic
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Sqrt.lean b/Mathlib/Analysis/SpecialFunctions/Sqrt.lean
index 7ae53108fa536..6ceb3781bd731 100644
--- a/Mathlib/Analysis/SpecialFunctions/Sqrt.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Sqrt.lean
@@ -3,7 +3,7 @@ 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.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Calculus.Deriv.Pow
 
 /-!
diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
index d98fdab776c9a..c54f4e9554b4e 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Operations
 import Mathlib.Analysis.Normed.Module.Convex
 import Mathlib.Data.Bundle
 import Mathlib.Geometry.Manifold.ChartedSpace