diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean
index 8e4a7cb6769404..b0d3cf783d3c00 100644
--- a/Mathlib/Analysis/Analytic/Constructions.lean
+++ b/Mathlib/Analysis/Analytic/Constructions.lean
@@ -972,20 +972,14 @@ theorem analyticAt_iff_analytic_smul [Module 𝕝 F] [IsBoundedSMul 𝕝 F] [IsS
   analyticAt_iff_analytic_fun_smul h₁f h₂f
 
 /- A function is analytic at a point iff it is analytic after multiplication
-  with a non-vanishing analytic function. -/
-theorem analyticAt_iff_analytic_fun_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z)
+with a non-vanishing analytic function. -/
+@[to_fun analyticAt_iff_analytic_fun_mul]
+theorem analyticAt_iff_analytic_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z)
     (h₂f : f z ≠ 0) :
-    AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z * g z) z := by
+    AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z := by
   simp_rw [← smul_eq_mul]
   exact analyticAt_iff_analytic_smul h₁f h₂f
 
-/- A function is analytic at a point iff it is analytic after multiplication
-  with a non-vanishing analytic function. -/
-theorem analyticAt_iff_analytic_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z)
-    (h₂f : f z ≠ 0) :
-    AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z :=
-  analyticAt_iff_analytic_fun_mul h₁f h₂f
-
 /-- `f x / g x` is analytic away from `g x = 0` -/
 theorem AnalyticWithinAt.div {f g : E → 𝕝} {s : Set E} {x : E}
     (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) (g0 : g x ≠ 0) :
@@ -1016,9 +1010,10 @@ theorem AnalyticOnNhd.div {f g : E → 𝕝} {s : Set E}
 -/
 
 /-- Finite sums of analytic functions are analytic -/
-theorem Finset.analyticWithinAt_fun_sum {f : α → E → F} {c : E} {s : Set E}
+@[to_fun Finset.analyticWithinAt_fun_sum]
+theorem Finset.analyticWithinAt_sum {f : α → E → F} {c : E} {s : Set E}
     (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) :
-    AnalyticWithinAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s c := by
+    AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c := by
   classical
   induction N using Finset.induction with
   | empty =>
@@ -1030,47 +1025,22 @@ theorem Finset.analyticWithinAt_fun_sum {f : α → E → F} {c : E} {s : Set E}
     exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))
 
 /-- Finite sums of analytic functions are analytic -/
-theorem Finset.analyticWithinAt_sum {f : α → E → F} {c : E} {s : Set E}
-    (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) :
-    AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c := by
-  convert N.analyticWithinAt_fun_sum h
-  simp
-
-/-- Finite sums of analytic functions are analytic -/
-@[fun_prop]
-theorem Finset.analyticAt_fun_sum {f : α → E → F} {c : E}
-    (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
-    AnalyticAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) c := by
-  simp_rw [← analyticWithinAt_univ] at h ⊢
-  exact N.analyticWithinAt_fun_sum h
-
-/-- Finite sums of analytic functions are analytic -/
-@[fun_prop]
+@[to_fun (attr := fun_prop) Finset.analyticAt_fun_sum]
 theorem Finset.analyticAt_sum {f : α → E → F} {c : E}
     (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
     AnalyticAt 𝕜 (∑ n ∈ N, f n) c := by
-  convert N.analyticAt_fun_sum h
-  simp
-
-/-- Finite sums of analytic functions are analytic -/
-theorem Finset.analyticOn_fun_sum {f : α → E → F} {s : Set E}
-    (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
-    AnalyticOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
-  fun z zs ↦ N.analyticWithinAt_fun_sum (fun n m ↦ h n m z zs)
+  simp_rw [← analyticWithinAt_univ] at h ⊢
+  exact N.analyticWithinAt_sum h
 
 /-- Finite sums of analytic functions are analytic -/
+@[to_fun Finset.analyticOn_fun_sum]
 theorem Finset.analyticOn_sum {f : α → E → F} {s : Set E}
     (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
     AnalyticOn 𝕜 (∑ n ∈ N, f n) s :=
   fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs)
 
 /-- Finite sums of analytic functions are analytic -/
-theorem Finset.analyticOnNhd_fun_sum {f : α → E → F} {s : Set E}
-    (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
-    AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
-  fun z zs ↦ N.analyticAt_fun_sum (fun n m ↦ h n m z zs)
-
-/-- Finite sums of analytic functions are analytic -/
+@[to_fun Finset.analyticOnNhd_fun_sum]
 theorem Finset.analyticOnNhd_sum {f : α → E → F} {s : Set E}
     (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
     AnalyticOnNhd 𝕜 (∑ n ∈ N, f n) s :=
diff --git a/Mathlib/Analysis/Calculus/Deriv/Pow.lean b/Mathlib/Analysis/Calculus/Deriv/Pow.lean
index baaaa3d6c3c8ca..6978c360e8b7b4 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Pow.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Pow.lean
@@ -105,33 +105,21 @@ theorem HasDerivWithinAt.fun_pow (h : HasDerivWithinAt f f' s x) (n : ℕ) :
 theorem HasDerivWithinAt.pow (h : HasDerivWithinAt f f' s x) (n : ℕ) :
     HasDerivWithinAt (f ^ n) (n * f x ^ (n - 1) * f') s x := h.fun_pow n
 
-theorem HasDerivAt.fun_pow (h : HasDerivAt f f' x) (n : ℕ) :
-    HasDerivAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') x := by
-  simpa using h.hasFDerivAt.pow n |>.hasDerivAt
-
+@[to_fun]
 theorem HasDerivAt.pow (h : HasDerivAt f f' x) (n : ℕ) :
-    HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := h.fun_pow n
+    HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := by
+  simpa using h.hasFDerivAt.pow n |>.hasDerivAt
 
-@[simp]
-theorem derivWithin_fun_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
-    derivWithin (fun x => f x ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x := by
+@[to_fun (attr := simp) derivWithin_fun_pow]
+theorem derivWithin_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
+    derivWithin (f ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x := by
   by_cases hsx : UniqueDiffWithinAt 𝕜 s x
   · exact (h.hasDerivWithinAt.pow n).derivWithin hsx
   · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
 
-@[simp]
-theorem derivWithin_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
-    derivWithin (f ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x :=
-  derivWithin_fun_pow h n
-
-@[simp]
-theorem deriv_fun_pow (h : DifferentiableAt 𝕜 f x) (n : ℕ) :
-    deriv (fun x => f x ^ n) x = n * f x ^ (n - 1) * deriv f x :=
-  (h.hasDerivAt.pow n).deriv
-
-@[simp]
+@[to_fun (attr := simp) deriv_fun_pow]
 theorem deriv_pow (h : DifferentiableAt 𝕜 f x) (n : ℕ) :
-    deriv (f ^ n) x = n * f x ^ (n - 1) * deriv f x := deriv_fun_pow h n
+    deriv (f ^ n) x = n * f x ^ (n - 1) * deriv f x := (h.hasDerivAt.pow n).deriv
 
 end NormedCommRing
 
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Pow.lean b/Mathlib/Analysis/Calculus/FDeriv/Pow.lean
index 89baf5759dbd1d..f8c00125370854 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Pow.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Pow.lean
@@ -45,60 +45,51 @@ private theorem aux (f : E → 𝔸) (f' : E →L[𝕜] 𝔸) (x : E) (n : ℕ)
   simp only [Finset.mem_range, Nat.lt_succ_iff] at hx
   rw [tsub_add_eq_add_tsub hx]
 
-theorem HasStrictFDerivAt.fun_pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) :
-    HasStrictFDerivAt (fun x ↦ f x ^ n)
+@[to_fun]
+theorem HasStrictFDerivAt.pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) :
+    HasStrictFDerivAt (f ^ n)
       (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
   match n with
   | 0 => by simpa using hasStrictFDerivAt_const 1 x
   | 1 => by simpa using h
   | n + 1 + 1 => by
-    have := h.mul' (h.fun_pow' (n + 1))
+    have := h.mul' (h.pow' (n + 1))
     simp_rw [pow_succ' _ (n + 1)]
     refine this.congr_fderiv <| aux _ _ _ _
 
-theorem HasStrictFDerivAt.pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) :
-    HasStrictFDerivAt (f ^ n)
-      (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x := h.fun_pow' n
-
 theorem hasStrictFDerivAt_pow' (n : ℕ) {x : 𝔸} :
     HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ x ^ n)
       (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) x :=
   hasStrictFDerivAt_id _ |>.pow' n
 
-theorem HasFDerivWithinAt.fun_pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) :
-    HasFDerivWithinAt (fun x ↦ f x ^ n)
+@[to_fun]
+theorem HasFDerivWithinAt.pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) :
+    HasFDerivWithinAt (f ^ n)
       (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) s x :=
   match n with
   | 0 => by simpa using hasFDerivWithinAt_const 1 x s
   | 1 => by simpa using h
   | n + 1 + 1 => by
-    have := h.mul' (h.fun_pow' (n + 1))
+    have := h.mul' (h.pow' (n + 1))
     simp_rw [pow_succ' _ (n + 1)]
     exact this.congr_fderiv <| aux _ _ _ _
 
-theorem HasFDerivWithinAt.pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) :
-    HasFDerivWithinAt (f ^ n)
-      (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) s x := h.fun_pow' n
-
 theorem hasFDerivWithinAt_pow' (n : ℕ) {x : 𝔸} {s : Set 𝔸} :
     HasFDerivWithinAt (𝕜 := 𝕜) (fun x ↦ x ^ n)
       (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) s x :=
   hasFDerivWithinAt_id _ _ |>.pow' n
 
-theorem HasFDerivAt.fun_pow' (h : HasFDerivAt f f' x) (n : ℕ) :
-    HasFDerivAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
+@[to_fun]
+theorem HasFDerivAt.pow' (h : HasFDerivAt f f' x) (n : ℕ) :
+    HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
   match n with
   | 0 => by simpa using hasFDerivAt_const 1 x
   | 1 => by simpa using h
   | n + 1 + 1 => by
-    have := h.mul' (h.fun_pow' (n + 1))
+    have := h.mul' (h.pow' (n + 1))
     simp_rw [pow_succ' _ (n + 1)]
     exact this.congr_fderiv <| aux _ _ _ _
 
-theorem HasFDerivAt.pow' (h : HasFDerivAt f f' x) (n : ℕ) :
-    HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
-  h.fun_pow' n
-
 theorem hasFDerivAt_pow' (n : ℕ) {x : 𝔸} :
     HasFDerivAt (𝕜 := 𝕜) (fun x ↦ x ^ n)
       (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) x :=
@@ -118,67 +109,45 @@ theorem differentiableWithinAt_pow (n : ℕ) {x : 𝔸} {s : Set 𝔸} :
     DifferentiableWithinAt 𝕜 (fun x : 𝔸 => x ^ n) s x :=
   differentiableWithinAt_id.pow _
 
-@[simp, fun_prop]
-theorem DifferentiableAt.fun_pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ) :
-    DifferentiableAt 𝕜 (fun x => f x ^ n) x :=
-  differentiableWithinAt_univ.mp <| hf.differentiableWithinAt.pow n
-
-@[simp, fun_prop]
+@[to_fun (attr := simp, fun_prop)]
 theorem DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ) :
-    DifferentiableAt 𝕜 (f ^ n) x := hf.fun_pow n
+    DifferentiableAt 𝕜 (f ^ n) x :=
+    differentiableWithinAt_univ.mp <| hf.differentiableWithinAt.pow n
 
 theorem differentiableAt_pow (n : ℕ) {x : 𝔸} : DifferentiableAt 𝕜 (fun x : 𝔸 => x ^ n) x :=
   differentiableAt_id.pow _
 
-@[fun_prop]
-theorem DifferentiableOn.fun_pow (hf : DifferentiableOn 𝕜 f s) (n : ℕ) :
-    DifferentiableOn 𝕜 (fun x => f x ^ n) s := fun x h => (hf x h).pow n
-
-@[fun_prop]
+@[to_fun (attr := fun_prop)]
 theorem DifferentiableOn.pow (hf : DifferentiableOn 𝕜 f s) (n : ℕ) :
-    DifferentiableOn 𝕜 (f ^ n) s := hf.fun_pow n
+    DifferentiableOn 𝕜 (f ^ n) s := fun x h => (hf x h).pow n
 
 theorem differentiableOn_pow (n : ℕ) {s : Set 𝔸} : DifferentiableOn 𝕜 (fun x : 𝔸 => x ^ n) s :=
   differentiableOn_id.pow n
 
-@[simp, fun_prop]
-theorem Differentiable.fun_pow (hf : Differentiable 𝕜 f) (n : ℕ) :
-    Differentiable 𝕜 fun x => f x ^ n :=
-  fun x => (hf x).pow n
-
-@[simp, fun_prop]
+@[to_fun (attr := simp, fun_prop)]
 theorem Differentiable.pow (hf : Differentiable 𝕜 f) (n : ℕ) : Differentiable 𝕜 (f ^ n) :=
-  hf.fun_pow n
+  fun x => (hf x).pow n
 
 theorem differentiable_pow (n : ℕ) : Differentiable 𝕜 fun x : 𝔸 => x ^ n :=
   differentiable_id.pow _
 
-theorem fderiv_fun_pow' (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
-    fderiv 𝕜 (fun x ↦ f x ^ n) x
-      = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderiv 𝕜 f x <• f x ^ i) :=
-  hf.hasFDerivAt.pow' n |>.fderiv
-
+@[to_fun fderiv_fun_pow']
 theorem fderiv_pow' (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
     fderiv 𝕜 (f ^ n) x
       = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderiv 𝕜 f x <• f x ^ i) :=
-  fderiv_fun_pow' n hf
+  hf.hasFDerivAt.pow' n |>.fderiv
 
 theorem fderiv_pow_ring' {x : 𝔸} (n : ℕ) :
     fderiv 𝕜 (fun x : 𝔸 ↦ x ^ n) x
       = (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> .id _ _ <• x ^ i) := by
   rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_fun_id]
 
-theorem fderivWithin_fun_pow' (hxs : UniqueDiffWithinAt 𝕜 s x)
-    (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
-    fderivWithin 𝕜 (fun x ↦ f x ^ n) s x
-      = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderivWithin 𝕜 f s x <• f x ^ i) :=
-  hf.hasFDerivWithinAt.pow' n |>.fderivWithin hxs
-
+@[to_fun fderivWithin_fun_pow']
 theorem fderivWithin_pow' (hxs : UniqueDiffWithinAt 𝕜 s x)
     (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
     fderivWithin 𝕜 (f ^ n) s x
       = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderivWithin 𝕜 f s x <• f x ^ i) :=
-  fderivWithin_fun_pow' hxs n hf
+  hf.hasFDerivWithinAt.pow' n |>.fderivWithin hxs
 
 theorem fderivWithin_pow_ring' {s : Set 𝔸} {x : 𝔸} (n : ℕ) (hxs : UniqueDiffWithinAt 𝕜 s x) :
     fderivWithin 𝕜 (fun x : 𝔸 ↦ x ^ n) s x
@@ -228,27 +197,20 @@ theorem hasFDerivAt_pow (n : ℕ) {x : 𝔸} :
       (fun x : 𝔸 ↦ x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x :=
   hasFDerivAt_id _ |>.pow n
 
-theorem fderiv_fun_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
-    fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x :=
-  hf.hasFDerivAt.pow n |>.fderiv
-
+@[to_fun fderiv_fun_pow]
 theorem fderiv_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
-    fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x :=
-  fderiv_fun_pow n hf
+    fderiv 𝕜 (f ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x :=
+  hf.hasFDerivAt.pow n |>.fderiv
 
 theorem fderiv_pow_ring {x : 𝔸} (n : ℕ) :
     fderiv 𝕜 (fun x : 𝔸 ↦ x ^ n) x = (n • x ^ (n - 1)) • .id _ _ := by
   rw [fderiv_fun_pow n differentiableAt_fun_id, fderiv_fun_id]
 
-theorem fderivWithin_fun_pow (hxs : UniqueDiffWithinAt 𝕜 s x)
-    (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
-    fderivWithin 𝕜 (fun x ↦ f x ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x :=
-  hf.hasFDerivWithinAt.pow n |>.fderivWithin hxs
-
+@[to_fun fderivWithin_fun_pow]
 theorem fderivWithin_pow (hxs : UniqueDiffWithinAt 𝕜 s x)
     (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
     fderivWithin 𝕜 (f ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x :=
-  fderivWithin_fun_pow hxs n hf
+  hf.hasFDerivWithinAt.pow n |>.fderivWithin hxs
 
 theorem fderivWithin_pow_ring {s : Set 𝔸} {x : 𝔸} (n : ℕ) (hxs : UniqueDiffWithinAt 𝕜 s x) :
     fderivWithin 𝕜 (fun x : 𝔸 ↦ x ^ n) s x = (n • x ^ (n - 1)) • .id _ _ := by
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
index b6222afdfc6fd8..76933237667dd5 100644
--- a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
+++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
@@ -245,6 +245,7 @@ theorem iteratedDerivWithin_comp_const_sub (c : 𝕜) :
   ext a
   simp [iteratedDerivWithin, iteratedFDerivWithin_comp_const_sub]
 
+@[to_fun iteratedDerivWithin_fun_id]
 lemma iteratedDerivWithin_id :
     iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0 := by
   obtain (_ | n) := n
@@ -253,10 +254,6 @@ lemma iteratedDerivWithin_id :
     · simp [iteratedDerivWithin_const]
     · exact fun y hy ↦ derivWithin_id _ _ (h.uniqueDiffWithinAt hy)
 
-lemma iteratedDerivWithin_fun_id :
-    iteratedDerivWithin n (·) s x = if n = 0 then x else if n = 1 then 1 else 0 :=
-  iteratedDerivWithin_id hx h
-
 lemma iteratedDerivWithin_smul {f : 𝕜 → 𝔸} {g : 𝕜 → F}
     (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) :
     iteratedDerivWithin n (f • g) s x = ∑ i ∈ .range (n + 1),
@@ -313,16 +310,12 @@ protected lemma Filter.EventuallyEq.iteratedDeriv
     iteratedDeriv n f₁ =ᶠ[𝓝 x] iteratedDeriv n f₂ := by
   simp_all [← nhdsWithin_univ, ← iteratedDerivWithin_univ, EventuallyEq.iteratedDerivWithin]
 
+@[to_fun iteratedDeriv_fun_add]
 lemma iteratedDeriv_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
     iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x := by
   simpa only [iteratedDerivWithin_univ] using
     iteratedDerivWithin_add (Set.mem_univ _) uniqueDiffOn_univ hf hg
 
--- TODO: `@[to_fun]` generates the wrong name. Same for the various lemmas below.
-lemma iteratedDeriv_fun_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
-    iteratedDeriv n (fun z ↦ f z + g z) x = iteratedDeriv n f x + iteratedDeriv n g x :=
-  iteratedDeriv_add hf hg
-
 theorem iteratedDeriv_const_add (hn : 0 < n) (c : F) :
     iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x := by
   simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_add hn c
@@ -331,35 +324,25 @@ theorem iteratedDeriv_const_sub (hn : 0 < n) (c : F) :
     iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x := by
   simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_sub hn c
 
-@[simp]
-lemma iteratedDeriv_fun_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
-    iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a) := by
-  simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f
-
-@[simp]
+@[simp, to_fun iteratedDeriv_fun_neg]
 lemma iteratedDeriv_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
     iteratedDeriv n (-f) a = -(iteratedDeriv n f a) := by
   simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f
+attribute [simp] iteratedDeriv_fun_neg
 
+@[to_fun iteratedDeriv_fun_sub]
 lemma iteratedDeriv_sub (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
     iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x := by
   simpa only [iteratedDerivWithin_univ] using
     iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ hf hg
 
-lemma iteratedDeriv_fun_sub (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
-    iteratedDeriv n (fun z ↦ f z - g z) x = iteratedDeriv n f x - iteratedDeriv n g x :=
-  iteratedDeriv_sub hf hg
-
+@[to_fun iteratedDeriv_fun_const_smul]
 theorem iteratedDeriv_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 n f x) (c : R) :
     iteratedDeriv n (c • f) x = c • iteratedDeriv n f x := by
   simpa only [iteratedDerivWithin_univ] using
     iteratedDerivWithin_const_smul (Set.mem_univ x) uniqueDiffOn_univ
       c (contDiffWithinAt_univ.mpr h)
 
-theorem iteratedDeriv_fun_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 n f x) (c : R) :
-    iteratedDeriv n (c • f ·) x = c • iteratedDeriv n f x :=
-  iteratedDeriv_const_smul h c
-
 /-- A variant of `iteratedDeriv_const_smul` without differentiability assumption when
 the scalar multiplication is by division ring elements. -/
 @[simp]
@@ -421,19 +404,17 @@ lemma iteratedDeriv_comp_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
     iteratedDeriv n (fun x ↦ f (-x)) a = (-1 : 𝕜) ^ n • iteratedDeriv n f (-a) := by
   simp [iteratedDeriv, ← iteratedFDerivWithin_univ, iteratedFDerivWithin_comp_neg]
 
+@[to_fun iteratedDeriv_fun_id]
 lemma iteratedDeriv_id {n : ℕ} {x : 𝕜} :
     iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0 := by
   obtain (_ | _ | n) := n <;>
     simp [iteratedDeriv_succ', iteratedDeriv_const]
 
-lemma iteratedDeriv_fun_id {n : ℕ} {x : 𝕜} :
-    iteratedDeriv n (fun a ↦ a) x = if n = 0 then x else if n = 1 then 1 else 0 :=
-  iteratedDeriv_id
-
 lemma iteratedDeriv_fun_id_zero :
     iteratedDeriv n (fun a ↦ a) (0 : 𝕜) = if n = 1 then 1 else 0 := by
   simp +contextual [iteratedDeriv_fun_id]
 
+@[to_fun iteratedDeriv_fun_mul]
 lemma iteratedDeriv_mul {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
     iteratedDeriv n (f * g) x = ∑ i ∈ .range (n + 1),
       n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x := by
@@ -445,11 +426,6 @@ theorem iteratedDeriv_pow (m : ℕ) (k : ℕ) :
     iteratedDeriv k (· ^ m) x = m.descFactorial k * x ^ (m - k) := by
   simpa using iteratedDerivWithin_pow (Set.mem_univ x) uniqueDiffOn_univ m k
 
-lemma iteratedDeriv_fun_mul {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
-    iteratedDeriv n (fun x ↦ f x * g x) x = ∑ i ∈ .range (n + 1),
-      n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x :=
-  iteratedDeriv_mul hf hg
-
 lemma iteratedDeriv_fun_pow_zero {n m : ℕ} :
     iteratedDeriv n (· ^ m) (0 : 𝕜) = if n = m then m.factorial else 0 := by
   obtain h | h | h := lt_trichotomy n m <;>