[Merged by Bors] - chore: use to_fun to auto-generate more duplicate lemmas

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 :=

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
 

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