From bbc2d076bb8ee7d1ad83cc55a10b741a6fba9b03 Mon Sep 17 00:00:00 2001
From: e-271828 <f_s@har.bbiq.jp>
Date: Sat, 11 Apr 2026 18:52:45 +0900
Subject: [PATCH 1/3] feat(Analysis/Analytic): add `AnalyticAt` properties for
 iterated `dslope`

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

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 47acf6695e6992..d290cc05bd365b 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -374,3 +374,36 @@ theorem AnalyticOnNhd.map_codiscreteWithin {U : Set 𝕜} {f : 𝕜 → E}
   fun _ hs ↦ mem_map.1 (preimage_mem_codiscreteWithin hfU h₂f hs)
 
 end PreimgCodiscrete
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- If `f` is analytic at `s` and `s ≠ z₀`, then `dslope f z₀` is analytic at `s`. -/
+lemma AnalyticAt.dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (hs : s ≠ z₀) :
+    AnalyticAt 𝕜 (dslope f z₀) s := by
+  have h_inv : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹) s :=
+    (analyticAt_id.sub analyticAt_const).inv (sub_ne_zero.mpr hs)
+  have h_quot : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹ • (f z - f z₀)) s :=
+    h_inv.smul (hf.sub analyticAt_const)
+  have h_eq : (fun z => (z - z₀)⁻¹ • (f z - f z₀)) =ᶠ[𝓝 s] dslope f z₀ := by
+    filter_upwards [isOpen_ne.mem_nhds hs] with z hz
+    exact (_root_.dslope_of_ne f hz).symm
+  exact h_quot.congr h_eq
+
+/-- If `f` is analytic at `s` and `s ≠ z₀`, then the `n`-th iterated `dslope` of `f` at `z₀`
+is analytic at `s`. -/
+lemma AnalyticAt.iterate_dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s)
+    (hs : s ≠ z₀) (n : ℕ) :
+    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) s := by
+  induction n with
+  | zero => exact hf
+  | succ n ih =>
+    rw [Function.iterate_succ_apply']
+    exact AnalyticAt.dslope_of_ne ih hs
+
+/-- If `f` is analytic at `z₀`, then the `n`-th iterated `dslope` of `f` at `z₀`
+is analytic at `z₀`. -/
+lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) :
+    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) z₀ := by
+  obtain ⟨p, hp⟩ := hf
+  exact ⟨_, hp.has_fpower_series_iterate_dslope_fslope n⟩

From 14055977e7840ca2da3f22f1f08ab3d83e6fefda Mon Sep 17 00:00:00 2001
From: e-271828 <f_s@har.bbiq.jp>
Date: Sun, 12 Apr 2026 00:45:15 +0900
Subject: [PATCH 2/3] refactor(Analysis/Analytic): unify
 AnalyticAt.iterate_dslope per reviewer suggestion

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

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index d290cc05bd365b..3447ececea846c 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -378,32 +378,40 @@ end PreimgCodiscrete
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 
-/-- If `f` is analytic at `s` and `s ≠ z₀`, then `dslope f z₀` is analytic at `s`. -/
-lemma AnalyticAt.dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (hs : s ≠ z₀) :
-    AnalyticAt 𝕜 (dslope f z₀) s := by
+private lemma AnalyticAt.dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s)
+    (hs : s ≠ z₀) : AnalyticAt 𝕜 (_root_.dslope f z₀) s := by
   have h_inv : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹) s :=
     (analyticAt_id.sub analyticAt_const).inv (sub_ne_zero.mpr hs)
   have h_quot : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹ • (f z - f z₀)) s :=
     h_inv.smul (hf.sub analyticAt_const)
-  have h_eq : (fun z => (z - z₀)⁻¹ • (f z - f z₀)) =ᶠ[𝓝 s] dslope f z₀ := by
+  have h_eq : (fun z => (z - z₀)⁻¹ • (f z - f z₀)) =ᶠ[𝓝 s] _root_.dslope f z₀ := by
     filter_upwards [isOpen_ne.mem_nhds hs] with z hz
     exact (_root_.dslope_of_ne f hz).symm
   exact h_quot.congr h_eq
 
-/-- If `f` is analytic at `s` and `s ≠ z₀`, then the `n`-th iterated `dslope` of `f` at `z₀`
-is analytic at `s`. -/
-lemma AnalyticAt.iterate_dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s)
-    (hs : s ≠ z₀) (n : ℕ) :
-    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) s := by
+/-- If `f` is analytic at `s`, then `dslope f z₀` is analytic at `s`. -/
+lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) :
+    AnalyticAt 𝕜 (_root_.dslope f z₀) s := by
+  by_cases hs : s = z₀
+  · subst hs
+    obtain ⟨p, hp⟩ := hf
+    exact ⟨_, hp.has_fpower_series_dslope_fslope⟩
+  · exact hf.dslope_of_ne hs
+
+private lemma AnalyticAt.iterate_dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s)
+    (hs : s ≠ z₀) (n : ℕ) : AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s := by
   induction n with
   | zero => exact hf
   | succ n ih =>
     rw [Function.iterate_succ_apply']
-    exact AnalyticAt.dslope_of_ne ih hs
-
-/-- If `f` is analytic at `z₀`, then the `n`-th iterated `dslope` of `f` at `z₀`
-is analytic at `z₀`. -/
-lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) :
-    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) z₀ := by
-  obtain ⟨p, hp⟩ := hf
-  exact ⟨_, hp.has_fpower_series_iterate_dslope_fslope n⟩
+    exact ih.dslope_of_ne hs
+
+/-- If `f` is analytic at `s`, then the `n`-th iterated `dslope` of `f` at `z₀`
+is analytic at `s`. -/
+lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) :
+    AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s := by
+  by_cases hs : s = z₀
+  · subst hs
+    obtain ⟨p, hp⟩ := hf
+    exact ⟨_, hp.has_fpower_series_iterate_dslope_fslope n⟩
+  · exact hf.iterate_dslope_of_ne hs n

From f8e92f2b5264f35e1788c7171dfc33a1f5b99633 Mon Sep 17 00:00:00 2001
From: e-271828 <39018690+e-271828@users.noreply.github.com>
Date: Sun, 12 Apr 2026 01:23:36 +0900
Subject: [PATCH 3/3] refactor(Analysis/Analytic): simplify
 AnalyticAt.iterate_dslope using Function.Iterate.rec

Apply an elegant simplification suggested by @wwylele.

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
---
 Mathlib/Analysis/Analytic/IsolatedZeros.lean | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 3447ececea846c..265234692b763b 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -398,20 +398,8 @@ lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f
     exact ⟨_, hp.has_fpower_series_dslope_fslope⟩
   · exact hf.dslope_of_ne hs
 
-private lemma AnalyticAt.iterate_dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s)
-    (hs : s ≠ z₀) (n : ℕ) : AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s := by
-  induction n with
-  | zero => exact hf
-  | succ n ih =>
-    rw [Function.iterate_succ_apply']
-    exact ih.dslope_of_ne hs
-
 /-- If `f` is analytic at `s`, then the `n`-th iterated `dslope` of `f` at `z₀`
 is analytic at `s`. -/
 lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) :
-    AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s := by
-  by_cases hs : s = z₀
-  · subst hs
-    obtain ⟨p, hp⟩ := hf
-    exact ⟨_, hp.has_fpower_series_iterate_dslope_fslope n⟩
-  · exact hf.iterate_dslope_of_ne hs n
+    AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s :=
+  Function.Iterate.rec _ hf (fun _ hf ↦ hf.dslope) n