chore: use the to_fun attribute (leanprover-community#32231)

Reduce code duplication using the to_fun attribute.

This is not exhaustive, neither does it constitute an endorsement "we always want to generate the applied form of a lemma".

Author: grunweg

Mathlib/Analysis/Analytic/Constructions.lean

@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Analytic.Linear
 public import Mathlib.Analysis.Normed.Operator.Mul
 public import Mathlib.Analysis.Normed.Ring.Units
 public import Mathlib.Analysis.Analytic.OfScalars
+import Mathlib.Tactic.ToFun
 
 /-!
 # Various ways to combine analytic functions
@@ -102,17 +103,13 @@ theorem AnalyticWithinAt.add (hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWi
   let ⟨_, hqf⟩ := hg
   (hpf.add hqf).analyticWithinAt
 
-@[fun_prop]
-theorem AnalyticAt.fun_add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
-    AnalyticAt 𝕜 (fun z ↦ f z + g z) x :=
+@[to_fun (attr := fun_prop)]
+theorem AnalyticAt.add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
+    AnalyticAt 𝕜 (f + g) x :=
   let ⟨_, hpf⟩ := hf
   let ⟨_, hqf⟩ := hg
   (hpf.add hqf).analyticAt
 
-@[fun_prop]
-theorem AnalyticAt.add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f + g) x :=
-  hf.fun_add hg
-
 theorem HasFPowerSeriesWithinOnBall.neg (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
     HasFPowerSeriesWithinOnBall (-f) (-pf) s x r :=
   { r_le := by
@@ -142,15 +139,11 @@ theorem AnalyticWithinAt.neg (hf : AnalyticWithinAt 𝕜 f s x) : AnalyticWithin
   let ⟨_, hpf⟩ := hf
   hpf.neg.analyticWithinAt
 
-@[fun_prop]
-theorem AnalyticAt.fun_neg (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ -f z) x :=
+@[to_fun (attr := fun_prop)]
+theorem AnalyticAt.neg (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (-f) x :=
   let ⟨_, hpf⟩ := hf
   hpf.neg.analyticAt
 
-@[fun_prop]
-theorem AnalyticAt.neg (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (-f) x :=
-  hf.fun_neg
-
 @[simp] lemma analyticAt_neg : AnalyticAt 𝕜 (-f) x ↔ AnalyticAt 𝕜 f x where
   mp hf := by simpa using hf.neg
   mpr := .neg
@@ -177,15 +170,10 @@ theorem AnalyticWithinAt.sub (hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWi
     AnalyticWithinAt 𝕜 (f - g) s x := by
   simpa only [sub_eq_add_neg] using hf.add hg.neg
 
-@[fun_prop]
-theorem AnalyticAt.fun_sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
-    AnalyticAt 𝕜 (fun z ↦ f z - g z) x := by
-  simpa only [sub_eq_add_neg] using hf.add hg.neg
-
-@[fun_prop]
+@[to_fun (attr := fun_prop)]
 theorem AnalyticAt.sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
-    AnalyticAt 𝕜 (f - g) x :=
-  hf.fun_sub hg
+    AnalyticAt 𝕜 (f - g) x := by
+  simpa only [sub_eq_add_neg] using hf.add hg.neg
 
 theorem HasFPowerSeriesWithinOnBall.const_smul (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
     HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r where
@@ -214,15 +202,11 @@ theorem AnalyticWithinAt.const_smul (hf : AnalyticWithinAt 𝕜 f s x) :
   let ⟨_, hpf⟩ := hf
   hpf.const_smul.analyticWithinAt
 
-@[fun_prop]
-theorem AnalyticAt.fun_const_smul (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ c • f z) x :=
+@[to_fun (attr := fun_prop)]
+theorem AnalyticAt.const_smul (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (c • f) x :=
   let ⟨_, hpf⟩ := hf
   hpf.const_smul.analyticAt
 
-@[fun_prop]
-theorem AnalyticAt.const_smul (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (c • f) x :=
-  hf.fun_const_smul
-
 theorem AnalyticOn.add (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
     AnalyticOn 𝕜 (f + g) s :=
   fun z hz => (hf z hz).add (hg z hz)
@@ -604,18 +588,11 @@ lemma AnalyticWithinAt.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F]
   (analyticAt_smul _).comp₂_analyticWithinAt hf hg
 
 /-- Scalar multiplication of one analytic function by another. -/
-@[fun_prop]
-lemma AnalyticAt.fun_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}
-    (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
-    AnalyticAt 𝕜 (fun x ↦ f x • g x) z :=
-  (analyticAt_smul _).comp₂ hf hg
-
-/-- Scalar multiplication of one analytic function by another. -/
-@[fun_prop]
+@[to_fun]
 lemma AnalyticAt.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}
     (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
     AnalyticAt 𝕜 (f • g) z :=
-  hf.fun_smul hg
+  (analyticAt_smul _).comp₂ hf hg
 
 /-- Scalar multiplication of one analytic function by another. -/
 lemma AnalyticOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F]
@@ -637,16 +614,10 @@ lemma AnalyticWithinAt.mul {f g : E → A} {s : Set E} {z : E}
   (analyticAt_mul _).comp₂_analyticWithinAt hf hg
 
 /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
-@[fun_prop]
-lemma AnalyticAt.fun_mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
-    AnalyticAt 𝕜 (fun x ↦ f x * g x) z :=
-  (analyticAt_mul _).comp₂ hf hg
-
-/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
-@[fun_prop]
+@[to_fun (attr := fun_prop)]
 lemma AnalyticAt.mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
     AnalyticAt 𝕜 (f * g) z :=
-  hf.fun_mul hg
+  (analyticAt_mul _).comp₂ hf hg
 
 /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
 lemma AnalyticOn.mul {f g : E → A} {s : Set E}
@@ -661,9 +632,10 @@ lemma AnalyticOnNhd.mul {f g : E → A} {s : Set E}
   fun _ m ↦ (hf _ m).mul (hg _ m)
 
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-lemma AnalyticWithinAt.fun_pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z)
+@[to_fun]
+lemma AnalyticWithinAt.pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z)
     (n : ℕ) :
-    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
+    AnalyticWithinAt 𝕜 (f ^ n) s z := by
   induction n with
   | zero =>
     simp only [pow_zero]
@@ -673,99 +645,56 @@ lemma AnalyticWithinAt.fun_pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticW
     exact hm.mul hf
 
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-lemma AnalyticWithinAt.pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z)
-    (n : ℕ) :
-    AnalyticWithinAt 𝕜 (f ^ n) s z :=
-  AnalyticWithinAt.fun_pow hf n
-
-/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-@[fun_prop]
-lemma AnalyticAt.fun_pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) :
-    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
+@[to_fun (attr := fun_prop)]
+lemma AnalyticAt.pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) :
+    AnalyticAt 𝕜 (f ^ n) z := by
   rw [← analyticWithinAt_univ] at hf ⊢
   exact hf.pow n
 
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-@[fun_prop]
-lemma AnalyticAt.pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) :
-    AnalyticAt 𝕜 (f ^ n) z :=
-  AnalyticAt.fun_pow hf n
-
-/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-lemma AnalyticOn.fun_pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) :
-    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s :=
-  fun _ m ↦ (hf _ m).pow n
-
-/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
+@[to_fun]
 lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) :
     AnalyticOn 𝕜 (f ^ n) s :=
   fun _ m ↦ (hf _ m).pow n
 
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-lemma AnalyticOnNhd.fun_pow {f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
-    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s :=
-  fun _ m ↦ (hf _ m).pow n
-
-/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
+@[to_fun]
 lemma AnalyticOnNhd.pow {f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
     AnalyticOnNhd 𝕜 (f ^ n) s :=
-  AnalyticOnNhd.fun_pow hf n
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
-nonnegative. -/
-lemma AnalyticWithinAt.fun_zpow_nonneg {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
-    (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) :
-    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
-  simpa [← zpow_natCast, hn] using hf.pow n.toNat
+  fun _ m ↦ (hf _ m).pow n
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
 nonnegative. -/
+@[to_fun]
 lemma AnalyticWithinAt.zpow_nonneg {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
     (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) :
-    AnalyticWithinAt 𝕜 (f ^ n) s z :=
-  fun_zpow_nonneg hf hn
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
-nonnegative. -/
-lemma AnalyticAt.fun_zpow_nonneg {f : E → 𝕝} {z : E} {n : ℤ} (hf : AnalyticAt 𝕜 f z) (hn : 0 ≤ n) :
-    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
+    AnalyticWithinAt 𝕜 (f ^ n) s z := by
   simpa [← zpow_natCast, hn] using hf.pow n.toNat
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
 nonnegative. -/
+@[to_fun]
 lemma AnalyticAt.zpow_nonneg {f : E → 𝕝} {z : E} {n : ℤ} (hf : AnalyticAt 𝕜 f z) (hn : 0 ≤ n) :
-    AnalyticAt 𝕜 (f ^ n) z :=
-  fun_zpow_nonneg hf hn
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
-nonnegative. -/
-lemma AnalyticOn.fun_zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOn 𝕜 f s)
-    (hn : 0 ≤ n) :
-    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s := by
+    AnalyticAt 𝕜 (f ^ n) z := by
   simpa [← zpow_natCast, hn] using hf.pow n.toNat
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
 nonnegative. -/
+@[to_fun]
 lemma AnalyticOn.zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOn 𝕜 f s)
     (hn : 0 ≤ n) :
-    AnalyticOn 𝕜 (f ^ n) s :=
-  fun_zpow_nonneg hf hn
+    AnalyticOn 𝕜 (f ^ n) s := by
+  simpa [← zpow_natCast, hn] using hf.pow n.toNat
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
 nonnegative. -/
-lemma AnalyticOnNhd.fun_zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s)
+@[to_fun]
+lemma AnalyticOnNhd.zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s)
     (hn : 0 ≤ n) :
-    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s := by
+    AnalyticOnNhd 𝕜 (f ^ n) s := by
   simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
   apply pow hf
 
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
-nonnegative. -/
-lemma AnalyticOnNhd.zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s)
-    (hn : 0 ≤ n) :
-    AnalyticOnNhd 𝕜 (f ^ n) s :=
-  fun_zpow_nonneg hf hn
-
 /-!
 ### Restriction of scalars
 -/
@@ -943,56 +872,37 @@ lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} :
   analyticOnNhd_inv.analyticOn
 
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-theorem AnalyticWithinAt.fun_inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x)
-    (f0 : f x ≠ 0) :
-    AnalyticWithinAt 𝕜 (fun x ↦ (f x)⁻¹) s x :=
-  (analyticAt_inv f0).comp_analyticWithinAt fa
-
-/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
+@[to_fun]
 theorem AnalyticWithinAt.inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x)
     (f0 : f x ≠ 0) :
     AnalyticWithinAt 𝕜 f⁻¹ s x :=
-  fun_inv fa f0
-
-/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-@[fun_prop]
-theorem AnalyticAt.fun_inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) :
-    AnalyticAt 𝕜 (fun x ↦ (f x)⁻¹) x :=
-  (analyticAt_inv f0).comp fa
+  (analyticAt_inv f0).comp_analyticWithinAt fa
 
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-@[fun_prop]
+@[to_fun (attr := fun_prop)]
 theorem AnalyticAt.inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : f x ≠ 0) :
     AnalyticAt 𝕜 f⁻¹ x :=
-  fa.fun_inv f0
-
-/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-theorem AnalyticOn.fun_inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
-    AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s :=
-  fun x m ↦ (fa x m).inv (f0 x m)
+  (analyticAt_inv f0).comp fa
 
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
+@[to_fun]
 theorem AnalyticOn.inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
     AnalyticOn 𝕜 f⁻¹ s :=
-  fun_inv fa f0
-
-/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-theorem AnalyticOnNhd.fun_inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s)
-    (f0 : ∀ x ∈ s, f x ≠ 0) :
-    AnalyticOnNhd 𝕜 (fun x ↦ (f x)⁻¹) s :=
   fun x m ↦ (fa x m).inv (f0 x m)
 
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
+@[to_fun]
 theorem AnalyticOnNhd.inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s)
     (f0 : ∀ x ∈ s, f x ≠ 0) :
     AnalyticOnNhd 𝕜 f⁻¹ s :=
-  fun_inv fa f0
+  fun x m ↦ (fa x m).inv (f0 x m)
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
-lemma AnalyticWithinAt.fun_zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
+@[to_fun]
+lemma AnalyticWithinAt.zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
     (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
-    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
+    AnalyticWithinAt 𝕜 (f ^ n) s z := by
   by_cases hn : 0 ≤ n
   · exact zpow_nonneg h₁f hn
   · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
@@ -1001,15 +911,9 @@ lemma AnalyticWithinAt.fun_zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
-lemma AnalyticWithinAt.zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
-    (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
-    AnalyticWithinAt 𝕜 (f ^ n) s z :=
-  fun_zpow h₁f h₂f
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
--/
-lemma AnalyticAt.fun_zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
-    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
+@[to_fun]
+lemma AnalyticAt.zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
+    AnalyticAt 𝕜 (f ^ n) z := by
   by_cases hn : 0 ≤ n
   · exact zpow_nonneg h₁f hn
   · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
@@ -1018,37 +922,19 @@ lemma AnalyticAt.fun_zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
-lemma AnalyticAt.zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
-    AnalyticAt 𝕜 (f ^ n) z := by
-  exact fun_zpow h₁f h₂f
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
--/
-lemma AnalyticOn.fun_zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOn 𝕜 f s)
-    (h₂f : ∀ z ∈ s, f z ≠ 0) :
-    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s :=
-  fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
--/
+@[to_fun]
 lemma AnalyticOn.zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOn 𝕜 f s)
     (h₂f : ∀ z ∈ s, f z ≠ 0) :
-    AnalyticOn 𝕜 (f ^ n) s := by
-  exact fun_zpow h₁f h₂f
-
-/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
--/
-lemma AnalyticOnNhd.fun_zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s)
-    (h₂f : ∀ z ∈ s, f z ≠ 0) :
-    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s :=
+    AnalyticOn 𝕜 (f ^ n) s :=
   fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
+@[to_fun]
 lemma AnalyticOnNhd.zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s)
     (h₂f : ∀ z ∈ s, f z ≠ 0) :
     AnalyticOnNhd 𝕜 (f ^ n) s :=
-  fun_zpow h₁f h₂f
+  fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)
 
 /- A function is analytic at a point iff it is analytic after scalar
   multiplication with a non-vanishing analytic function. -/