From 0f4163c5cb0a5b99b55a74c63bac1c5eab8b6108 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Jun 2023 09:09:56 +0200
Subject: [PATCH 1/6] feat: port Analysis.Analytic.IsolatedZeros


From a79e2d91cafbfe62f107aa6798fe85042c45d123 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Jun 2023 09:09:56 +0200
Subject: [PATCH 2/6] Initial file copy from mathport

---
 Mathlib/Analysis/Analytic/IsolatedZeros.lean | 221 +++++++++++++++++++
 1 file changed, 221 insertions(+)
 create mode 100644 Mathlib/Analysis/Analytic/IsolatedZeros.lean

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
new file mode 100644
index 0000000000000..797091e5caca9
--- /dev/null
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -0,0 +1,221 @@
+/-
+Copyright (c) 2022 Vincent Beffara. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vincent Beffara
+
+! This file was ported from Lean 3 source module analysis.analytic.isolated_zeros
+! leanprover-community/mathlib commit a3209ddf94136d36e5e5c624b10b2a347cc9d090
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Analysis.Analytic.Basic
+import Mathbin.Analysis.Calculus.Dslope
+import Mathbin.Analysis.Calculus.FderivAnalytic
+import Mathbin.Analysis.Calculus.FormalMultilinearSeries
+import Mathbin.Analysis.Analytic.Uniqueness
+
+/-!
+# Principle of isolated zeros
+
+This file proves the fact that the zeros of a non-constant analytic function of one variable are
+isolated. It also introduces a little bit of API in the `has_fpower_series_at` namespace that is
+useful in this setup.
+
+## Main results
+
+* `analytic_at.eventually_eq_zero_or_eventually_ne_zero` is the main statement that if a function is
+  analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
+  vanish in a punctured neighborhood of `z₀`.
+* `analytic_on.eq_on_of_preconnected_of_frequently_eq` is the identity theorem for analytic
+  functions: if a function `f` is analytic on a connected set `U` and is zero on a set with an
+  accumulation point in `U` then `f` is identically `0` on `U`.
+-/
+
+
+open scoped Classical
+
+open Filter Function Nat FormalMultilinearSeries Emetric Set
+
+open scoped Topology BigOperators
+
+variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddCommGroup E]
+  [NormedSpace 𝕜 E] {s : E} {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {n : ℕ} {z z₀ : 𝕜}
+  {y : Fin n → 𝕜}
+
+namespace HasSum
+
+variable {a : ℕ → E}
+
+theorem hasSum_at_zero (a : ℕ → E) : HasSum (fun n => (0 : 𝕜) ^ n • a n) (a 0) := by
+  convert hasSum_single 0 fun b h => _ <;>
+    first
+    | simp [Nat.pos_of_ne_zero h]
+    | simp
+#align has_sum.has_sum_at_zero HasSum.hasSum_at_zero
+
+theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m) s)
+    (ha : ∀ k < n, a k = 0) : ∃ t : E, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t :=
+  by
+  obtain rfl | hn := n.eq_zero_or_pos
+  · simpa
+  by_cases h : z = 0
+  · have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using has_sum_at_zero a)
+    exact ⟨a n, by simp [h, hn, this], by simpa [h] using has_sum_at_zero fun m => a (m + n)⟩
+  · refine' ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], _⟩
+    have h1 : ∑ i in Finset.range n, z ^ i • a i = 0 :=
+      Finset.sum_eq_zero fun k hk => by simp [ha k (finset.mem_range.mp hk)]
+    have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by
+      simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
+    convert h2.const_smul (z⁻¹ ^ n)
+    · field_simp [pow_add, smul_smul]
+    · simp only [inv_pow]
+#align has_sum.exists_has_sum_smul_of_apply_eq_zero HasSum.exists_hasSum_smul_of_apply_eq_zero
+
+end HasSum
+
+namespace HasFPowerSeriesAt
+
+theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
+    HasFPowerSeriesAt (dslope f z₀) p.fslope z₀ :=
+  by
+  have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
+  have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
+  simp only [hasFPowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
+  refine' hp.mono fun x hx => _
+  by_cases h : x = 0
+  · convert hasSum_single 0 _ <;> intros <;> simp [*]
+  · have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, pow_succ']
+    suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
+      simpa [dslope, slope, h, smul_smul, hxx] using this
+    · simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
+#align has_fpower_series_at.has_fpower_series_dslope_fslope HasFPowerSeriesAt.has_fpower_series_dslope_fslope
+
+theorem has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) :
+    HasFPowerSeriesAt ((swap dslope z₀^[n]) f) ((fslope^[n]) p) z₀ :=
+  by
+  induction' n with n ih generalizing f p
+  · exact hp
+  · simpa using ih (has_fpower_series_dslope_fslope hp)
+#align has_fpower_series_at.has_fpower_series_iterate_dslope_fslope HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope
+
+theorem iterate_dslope_fslope_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) :
+    (swap dslope z₀^[p.order]) f z₀ ≠ 0 :=
+  by
+  rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]
+  simpa [coeff_eq_zero] using apply_order_ne_zero h
+#align has_fpower_series_at.iterate_dslope_fslope_ne_zero HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero
+
+theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
+    ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀^[p.order]) f z :=
+  by
+  have hq := has_fpower_series_at_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
+  filter_upwards [hq, has_fpower_series_at_iff'.mp hp] with x hx1 hx2
+  have : ∀ k < p.order, p.coeff k = 0 := fun k hk => by
+    simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
+  obtain ⟨s, hs1, hs2⟩ := HasSum.exists_hasSum_smul_of_apply_eq_zero hx2 this
+  convert hs1.symm
+  simp only [coeff_iterate_fslope] at hx1 
+  exact hx1.unique hs2
+#align has_fpower_series_at.eq_pow_order_mul_iterate_dslope HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope
+
+theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
+  by
+  rw [eventually_nhdsWithin_iff]
+  have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).ContinuousAt
+  have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
+  filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3] with z e1 e2 e3
+  simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3)
+#align has_fpower_series_at.locally_ne_zero HasFPowerSeriesAt.locally_ne_zero
+
+theorem locally_zero_iff (hp : HasFPowerSeriesAt f p z₀) : (∀ᶠ z in 𝓝 z₀, f z = 0) ↔ p = 0 :=
+  ⟨fun hf => hp.eq_zero_of_eventually hf, fun h => eventually_eq_zero (by rwa [h] at hp )⟩
+#align has_fpower_series_at.locally_zero_iff HasFPowerSeriesAt.locally_zero_iff
+
+end HasFPowerSeriesAt
+
+namespace AnalyticAt
+
+/-- The *principle of isolated zeros* for an analytic function, local version: if a function is
+analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
+vanish in a punctured neighborhood of `z₀`. -/
+theorem eventually_eq_zero_or_eventually_ne_zero (hf : AnalyticAt 𝕜 f z₀) :
+    (∀ᶠ z in 𝓝 z₀, f z = 0) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
+  by
+  rcases hf with ⟨p, hp⟩
+  by_cases h : p = 0
+  · exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp ))
+  · exact Or.inr (hp.locally_ne_zero h)
+#align analytic_at.eventually_eq_zero_or_eventually_ne_zero AnalyticAt.eventually_eq_zero_or_eventually_ne_zero
+
+theorem eventually_eq_or_eventually_ne (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
+    (∀ᶠ z in 𝓝 z₀, f z = g z) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ g z := by
+  simpa [sub_eq_zero] using (hf.sub hg).eventually_eq_zero_or_eventually_ne_zero
+#align analytic_at.eventually_eq_or_eventually_ne AnalyticAt.eventually_eq_or_eventually_ne
+
+theorem frequently_zero_iff_eventually_zero {f : 𝕜 → E} {w : 𝕜} (hf : AnalyticAt 𝕜 f w) :
+    (∃ᶠ z in 𝓝[≠] w, f z = 0) ↔ ∀ᶠ z in 𝓝 w, f z = 0 :=
+  ⟨hf.eventually_eq_zero_or_eventually_ne_zero.resolve_right, fun h =>
+    (h.filter_mono nhdsWithin_le_nhds).Frequently⟩
+#align analytic_at.frequently_zero_iff_eventually_zero AnalyticAt.frequently_zero_iff_eventually_zero
+
+theorem frequently_eq_iff_eventually_eq (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
+    (∃ᶠ z in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ z in 𝓝 z₀, f z = g z := by
+  simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)
+#align analytic_at.frequently_eq_iff_eventually_eq AnalyticAt.frequently_eq_iff_eventually_eq
+
+end AnalyticAt
+
+namespace AnalyticOn
+
+variable {U : Set 𝕜}
+
+/-- The *principle of isolated zeros* for an analytic function, global version: if a function is
+analytic on a connected set `U` and vanishes in arbitrary neighborhoods of a point `z₀ ∈ U`, then
+it is identically zero in `U`.
+For higher-dimensional versions requiring that the function vanishes in a neighborhood of `z₀`,
+see `eq_on_zero_of_preconnected_of_eventually_eq_zero`. -/
+theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOn 𝕜 f U)
+    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfw : ∃ᶠ z in 𝓝[≠] z₀, f z = 0) : EqOn f 0 U :=
+  hf.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀
+    ((hf z₀ h₀).frequently_zero_iff_eventually_zero.1 hfw)
+#align analytic_on.eq_on_zero_of_preconnected_of_frequently_eq_zero AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero
+
+theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U)
+    (h₀ : z₀ ∈ U) (hfz₀ : z₀ ∈ closure ({z | f z = 0} \ {z₀})) : EqOn f 0 U :=
+  hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀
+    (mem_closure_ne_iff_frequently_within.mp hfz₀)
+#align analytic_on.eq_on_zero_of_preconnected_of_mem_closure AnalyticOn.eqOn_zero_of_preconnected_of_mem_closure
+
+/-- The *identity principle* for analytic functions, global version: if two functions are
+analytic on a connected set `U` and coincide at points which accumulate to a point `z₀ ∈ U`, then
+they coincide globally in `U`.
+For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
+see `eq_on_of_preconnected_of_eventually_eq`. -/
+theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U)
+    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U :=
+  by
+  have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
+    hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
+  simpa [sub_eq_zero] using fun z hz =>
+    (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz
+#align analytic_on.eq_on_of_preconnected_of_frequently_eq AnalyticOn.eqOn_of_preconnected_of_frequently_eq
+
+theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U)
+    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z | f z = g z} \ {z₀})) :
+    EqOn f g U :=
+  hf.eqOn_of_preconnected_of_frequently_eq hg hU h₀ (mem_closure_ne_iff_frequently_within.mp hfg)
+#align analytic_on.eq_on_of_preconnected_of_mem_closure AnalyticOn.eqOn_of_preconnected_of_mem_closure
+
+/-- The *identity principle* for analytic functions, global version: if two functions on a normed
+field `𝕜` are analytic everywhere and coincide at points which accumulate to a point `z₀`, then
+they coincide globally.
+For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
+see `eq_of_eventually_eq`. -/
+theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOn 𝕜 f univ) (hg : AnalyticOn 𝕜 g univ)
+    (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g :=
+  funext fun x =>
+    eqOn_of_preconnected_of_frequently_eq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)
+#align analytic_on.eq_of_frequently_eq AnalyticOn.eq_of_frequently_eq
+
+end AnalyticOn
+

From 9959506990c1c328cbc572dfc4ae7a6b4b6df6ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Jun 2023 09:09:57 +0200
Subject: [PATCH 3/6] automated fixes

Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
---
 Mathlib.lean                                 |  1 +
 Mathlib/Analysis/Analytic/IsolatedZeros.lean | 34 ++++++++------------
 2 files changed, 14 insertions(+), 21 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 5cba6d5ca28f8..b35db922c0b5d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -447,6 +447,7 @@ import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.Analysis.Analytic.Basic
 import Mathlib.Analysis.Analytic.Composition
+import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Analytic.Linear
 import Mathlib.Analysis.Analytic.RadiusLiminf
 import Mathlib.Analysis.Analytic.Uniqueness
diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 797091e5caca9..02614e0d0ea05 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -8,11 +8,11 @@ Authors: Vincent Beffara
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Analysis.Analytic.Basic
-import Mathbin.Analysis.Calculus.Dslope
-import Mathbin.Analysis.Calculus.FderivAnalytic
-import Mathbin.Analysis.Calculus.FormalMultilinearSeries
-import Mathbin.Analysis.Analytic.Uniqueness
+import Mathlib.Analysis.Analytic.Basic
+import Mathlib.Analysis.Calculus.Dslope
+import Mathlib.Analysis.Calculus.FderivAnalytic
+import Mathlib.Analysis.Calculus.FormalMultilinearSeries
+import Mathlib.Analysis.Analytic.Uniqueness
 
 /-!
 # Principle of isolated zeros
@@ -54,8 +54,7 @@ theorem hasSum_at_zero (a : ℕ → E) : HasSum (fun n => (0 : 𝕜) ^ n • a n
 #align has_sum.has_sum_at_zero HasSum.hasSum_at_zero
 
 theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m) s)
-    (ha : ∀ k < n, a k = 0) : ∃ t : E, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t :=
-  by
+    (ha : ∀ k < n, a k = 0) : ∃ t : E, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t := by
   obtain rfl | hn := n.eq_zero_or_pos
   · simpa
   by_cases h : z = 0
@@ -76,8 +75,7 @@ end HasSum
 namespace HasFPowerSeriesAt
 
 theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
-    HasFPowerSeriesAt (dslope f z₀) p.fslope z₀ :=
-  by
+    HasFPowerSeriesAt (dslope f z₀) p.fslope z₀ := by
   have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
   have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
   simp only [hasFPowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
@@ -91,23 +89,20 @@ theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
 #align has_fpower_series_at.has_fpower_series_dslope_fslope HasFPowerSeriesAt.has_fpower_series_dslope_fslope
 
 theorem has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) :
-    HasFPowerSeriesAt ((swap dslope z₀^[n]) f) ((fslope^[n]) p) z₀ :=
-  by
+    HasFPowerSeriesAt ((swap dslope z₀^[n]) f) ((fslope^[n]) p) z₀ := by
   induction' n with n ih generalizing f p
   · exact hp
   · simpa using ih (has_fpower_series_dslope_fslope hp)
 #align has_fpower_series_at.has_fpower_series_iterate_dslope_fslope HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope
 
 theorem iterate_dslope_fslope_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) :
-    (swap dslope z₀^[p.order]) f z₀ ≠ 0 :=
-  by
+    (swap dslope z₀^[p.order]) f z₀ ≠ 0 := by
   rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]
   simpa [coeff_eq_zero] using apply_order_ne_zero h
 #align has_fpower_series_at.iterate_dslope_fslope_ne_zero HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero
 
 theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
-    ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀^[p.order]) f z :=
-  by
+    ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀^[p.order]) f z := by
   have hq := has_fpower_series_at_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
   filter_upwards [hq, has_fpower_series_at_iff'.mp hp] with x hx1 hx2
   have : ∀ k < p.order, p.coeff k = 0 := fun k hk => by
@@ -118,8 +113,7 @@ theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
   exact hx1.unique hs2
 #align has_fpower_series_at.eq_pow_order_mul_iterate_dslope HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope
 
-theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
-  by
+theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 := by
   rw [eventually_nhdsWithin_iff]
   have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).ContinuousAt
   have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
@@ -139,8 +133,7 @@ namespace AnalyticAt
 analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
 vanish in a punctured neighborhood of `z₀`. -/
 theorem eventually_eq_zero_or_eventually_ne_zero (hf : AnalyticAt 𝕜 f z₀) :
-    (∀ᶠ z in 𝓝 z₀, f z = 0) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
-  by
+    (∀ᶠ z in 𝓝 z₀, f z = 0) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 := by
   rcases hf with ⟨p, hp⟩
   by_cases h : p = 0
   · exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp ))
@@ -192,8 +185,7 @@ they coincide globally in `U`.
 For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
 see `eq_on_of_preconnected_of_eventually_eq`. -/
 theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U)
-    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U :=
-  by
+    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U := by
   have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
     hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
   simpa [sub_eq_zero] using fun z hz =>

From 292128c137e8aa0648c721b94c06b8740c0bc27f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Jun 2023 11:17:03 +0200
Subject: [PATCH 4/6] Green

---
 Mathlib/Analysis/Analytic/IsolatedZeros.lean | 33 ++++++++++----------
 1 file changed, 16 insertions(+), 17 deletions(-)

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 02614e0d0ea05..3a1d03c8e2d2e 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -34,20 +34,20 @@ useful in this setup.
 
 open scoped Classical
 
-open Filter Function Nat FormalMultilinearSeries Emetric Set
+open Filter Function Nat FormalMultilinearSeries EMetric Set
 
 open scoped Topology BigOperators
 
 variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] {s : E} {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {n : ℕ} {z z₀ : 𝕜}
-  {y : Fin n → 𝕜}
+--  {y : Fin n → 𝕜} -- Porting note: TODO
 
 namespace HasSum
 
 variable {a : ℕ → E}
 
 theorem hasSum_at_zero (a : ℕ → E) : HasSum (fun n => (0 : 𝕜) ^ n • a n) (a 0) := by
-  convert hasSum_single 0 fun b h => _ <;>
+  convert hasSum_single (α := E) 0 fun b h => _ <;>
     first
     | simp [Nat.pos_of_ne_zero h]
     | simp
@@ -58,14 +58,14 @@ theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m
   obtain rfl | hn := n.eq_zero_or_pos
   · simpa
   by_cases h : z = 0
-  · have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using has_sum_at_zero a)
-    exact ⟨a n, by simp [h, hn, this], by simpa [h] using has_sum_at_zero fun m => a (m + n)⟩
-  · refine' ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], _⟩
+  · have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
+    exact ⟨a n, by simp [h, hn, this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩
+  · refine ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], ?_⟩
     have h1 : ∑ i in Finset.range n, z ^ i • a i = 0 :=
-      Finset.sum_eq_zero fun k hk => by simp [ha k (finset.mem_range.mp hk)]
+      Finset.sum_eq_zero fun k hk => by simp [ha k (Finset.mem_range.mp hk)]
     have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by
       simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
-    convert h2.const_smul (z⁻¹ ^ n)
+    convert h2.const_smul (z⁻¹ ^ n) using 1
     · field_simp [pow_add, smul_smul]
     · simp only [inv_pow]
 #align has_sum.exists_has_sum_smul_of_apply_eq_zero HasSum.exists_hasSum_smul_of_apply_eq_zero
@@ -79,10 +79,10 @@ theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
   have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
   have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
   simp only [hasFPowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
-  refine' hp.mono fun x hx => _
+  refine hp.mono fun x hx => ?_
   by_cases h : x = 0
-  · convert hasSum_single 0 _ <;> intros <;> simp [*]
-  · have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, pow_succ']
+  · convert hasSum_single (α := E) 0 _ <;> intros <;> simp [*]
+  · have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, _root_.pow_succ']
     suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
       simpa [dslope, slope, h, smul_smul, hxx] using this
     · simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
@@ -103,19 +103,19 @@ theorem iterate_dslope_fslope_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p 
 
 theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
     ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀^[p.order]) f z := by
-  have hq := has_fpower_series_at_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
-  filter_upwards [hq, has_fpower_series_at_iff'.mp hp] with x hx1 hx2
+  have hq := hasFPowerSeriesAt_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
+  filter_upwards [hq, hasFPowerSeriesAt_iff'.mp hp] with x hx1 hx2
   have : ∀ k < p.order, p.coeff k = 0 := fun k hk => by
     simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
   obtain ⟨s, hs1, hs2⟩ := HasSum.exists_hasSum_smul_of_apply_eq_zero hx2 this
   convert hs1.symm
-  simp only [coeff_iterate_fslope] at hx1 
+  simp only [coeff_iterate_fslope] at hx1
   exact hx1.unique hs2
 #align has_fpower_series_at.eq_pow_order_mul_iterate_dslope HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope
 
 theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 := by
   rw [eventually_nhdsWithin_iff]
-  have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).ContinuousAt
+  have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).continuousAt
   have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
   filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3] with z e1 e2 e3
   simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3)
@@ -148,7 +148,7 @@ theorem eventually_eq_or_eventually_ne (hf : AnalyticAt 𝕜 f z₀) (hg : Analy
 theorem frequently_zero_iff_eventually_zero {f : 𝕜 → E} {w : 𝕜} (hf : AnalyticAt 𝕜 f w) :
     (∃ᶠ z in 𝓝[≠] w, f z = 0) ↔ ∀ᶠ z in 𝓝 w, f z = 0 :=
   ⟨hf.eventually_eq_zero_or_eventually_ne_zero.resolve_right, fun h =>
-    (h.filter_mono nhdsWithin_le_nhds).Frequently⟩
+    (h.filter_mono nhdsWithin_le_nhds).frequently⟩
 #align analytic_at.frequently_zero_iff_eventually_zero AnalyticAt.frequently_zero_iff_eventually_zero
 
 theorem frequently_eq_iff_eventually_eq (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
@@ -210,4 +210,3 @@ theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOn 𝕜 f univ)
 #align analytic_on.eq_of_frequently_eq AnalyticOn.eq_of_frequently_eq
 
 end AnalyticOn
-

From 95a62c3292b16abde41ae4c9b258822967b12e97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Jun 2023 11:19:32 +0200
Subject: [PATCH 5/6] Porting notes

---
 Mathlib/Analysis/Analytic/IsolatedZeros.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 3a1d03c8e2d2e..1b985089687bb 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -18,15 +18,15 @@ import Mathlib.Analysis.Analytic.Uniqueness
 # Principle of isolated zeros
 
 This file proves the fact that the zeros of a non-constant analytic function of one variable are
-isolated. It also introduces a little bit of API in the `has_fpower_series_at` namespace that is
+isolated. It also introduces a little bit of API in the `HasFPowerSeriesAt` namespace that is
 useful in this setup.
 
 ## Main results
 
-* `analytic_at.eventually_eq_zero_or_eventually_ne_zero` is the main statement that if a function is
+* `AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` is the main statement that if a function is
   analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
   vanish in a punctured neighborhood of `z₀`.
-* `analytic_on.eq_on_of_preconnected_of_frequently_eq` is the identity theorem for analytic
+* `AnalyticOn.eqOn_of_preconnected_of_frequently_eq` is the identity theorem for analytic
   functions: if a function `f` is analytic on a connected set `U` and is zero on a set with an
   accumulation point in `U` then `f` is identically `0` on `U`.
 -/
@@ -40,7 +40,8 @@ open scoped Topology BigOperators
 
 variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] {s : E} {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {n : ℕ} {z z₀ : 𝕜}
---  {y : Fin n → 𝕜} -- Porting note: TODO
+--  {y : Fin n → 𝕜} -- Porting note: This is used nowhere and creates problem since it is sometimes
+-- automatically included as an hypothesis
 
 namespace HasSum
 

From dca0badcd80c6f228c18359311f7b940b3cc0192 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Jun 2023 11:22:53 +0200
Subject: [PATCH 6/6] Fix import

---
 Mathlib/Analysis/Analytic/IsolatedZeros.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 1b985089687bb..e6a52ebeffda9 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -10,7 +10,7 @@ Authors: Vincent Beffara
 -/
 import Mathlib.Analysis.Analytic.Basic
 import Mathlib.Analysis.Calculus.Dslope
-import Mathlib.Analysis.Calculus.FderivAnalytic
+import Mathlib.Analysis.Calculus.FDerivAnalytic
 import Mathlib.Analysis.Calculus.FormalMultilinearSeries
 import Mathlib.Analysis.Analytic.Uniqueness