diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
index 26093e42f5ff8..e321567bede4c 100644
--- a/Mathlib/Analysis/Analytic/Basic.lean
+++ b/Mathlib/Analysis/Analytic/Basic.lean
@@ -54,8 +54,7 @@ Additionally, let `f` be a function from `E` to `F`.
 We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOn` restricted to a
 set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties.
 
-* `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[s] x`, and
-  `f` is continuous within `s` at `x`.
+* `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[s ∪ {x}] x`.
 * `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
 
 We develop the basic properties of these notions, notably:
@@ -340,7 +339,7 @@ end FormalMultilinearSeries
 
 section
 
-variable {f g : E → F} {p pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ℝ≥0∞}
+variable {f g : E → F} {p pf pg : FormalMultilinearSeries 𝕜 E F} {s t : Set E} {x : E} {r r' : ℝ≥0∞}
 
 /-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as
 a power series on the ball of radius `r > 0` around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `‖y‖ < r`.
@@ -352,7 +351,8 @@ structure HasFPowerSeriesOnBall (f : E → F) (p : FormalMultilinearSeries 𝕜
   hasSum :
     ∀ {y}, y ∈ EMetric.ball (0 : E) r → HasSum (fun n : ℕ => p n fun _ : Fin n => y) (f (x + y))
 
-/-- Analogue of `HasFPowerSeriesOnBall` where convergence is required only on a set `s`. -/
+/-- Analogue of `HasFPowerSeriesOnBall` where convergence is required only on a set `s`. We also
+require convergence at `x` as the behavior of this notion is very bad otherwise. -/
 structure HasFPowerSeriesWithinOnBall (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (s : Set E)
     (x : E) (r : ℝ≥0∞) : Prop where
   /-- `p` converges on `ball 0 r` -/
@@ -360,10 +360,8 @@ structure HasFPowerSeriesWithinOnBall (f : E → F) (p : FormalMultilinearSeries
   /-- The radius of convergence is positive -/
   r_pos : 0 < r
   /-- `p converges to f` within `s` -/
-  hasSum : ∀ {y}, x + y ∈ s → y ∈ EMetric.ball (0 : E) r →
+  hasSum : ∀ {y}, x + y ∈ insert x s → y ∈ EMetric.ball (0 : E) r →
     HasSum (fun n : ℕ => p n fun _ : Fin n => y) (f (x + y))
-  /-- We require `ContinuousWithinAt f s x` to ensure `f x` is nice -/
-  continuousWithinAt : ContinuousWithinAt f s x
 
 /-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as
 a power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a neighborhood of `0`. -/
@@ -410,6 +408,17 @@ theorem HasFPowerSeriesAt.analyticAt (hf : HasFPowerSeriesAt f p x) : AnalyticAt
 theorem HasFPowerSeriesOnBall.analyticAt (hf : HasFPowerSeriesOnBall f p x r) : AnalyticAt 𝕜 f x :=
   hf.hasFPowerSeriesAt.analyticAt
 
+theorem HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) : HasFPowerSeriesWithinAt f p s x :=
+  ⟨r, hf⟩
+
+theorem HasFPowerSeriesWithinAt.analyticWithinAt (hf : HasFPowerSeriesWithinAt f p s x) :
+    AnalyticWithinAt 𝕜 f s x := ⟨p, hf⟩
+
+theorem HasFPowerSeriesWithinOnBall.analyticWithinAt (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    AnalyticWithinAt 𝕜 f s x :=
+  hf.hasFPowerSeriesWithinAt.analyticWithinAt
+
 theorem HasFPowerSeriesOnBall.congr (hf : HasFPowerSeriesOnBall f p x r)
     (hg : EqOn f g (EMetric.ball x r)) : HasFPowerSeriesOnBall g p x r :=
   { r_le := hf.r_le
@@ -429,6 +438,13 @@ theorem HasFPowerSeriesOnBall.comp_sub (hf : HasFPowerSeriesOnBall f p x r) (y :
       convert hf.hasSum hz using 2
       abel }
 
+theorem HasFPowerSeriesWithinOnBall.hasSum_sub (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E}
+    (hy : y ∈ (insert x s) ∩ EMetric.ball x r) :
+    HasSum (fun n : ℕ => p n fun _ => y - x) (f y) := by
+  have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_coe_nnnorm_sub] using hy.2
+  have := hf.hasSum (by simpa only [add_sub_cancel] using hy.1) this
+  simpa only [add_sub_cancel]
+
 theorem HasFPowerSeriesOnBall.hasSum_sub (hf : HasFPowerSeriesOnBall f p x r) {y : E}
     (hy : y ∈ EMetric.ball x r) : HasSum (fun n : ℕ => p n fun _ => y - x) (f y) := by
   have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_coe_nnnorm_sub] using hy
@@ -437,10 +453,19 @@ theorem HasFPowerSeriesOnBall.hasSum_sub (hf : HasFPowerSeriesOnBall f p x r) {y
 theorem HasFPowerSeriesOnBall.radius_pos (hf : HasFPowerSeriesOnBall f p x r) : 0 < p.radius :=
   lt_of_lt_of_le hf.r_pos hf.r_le
 
+theorem HasFPowerSeriesWithinOnBall.radius_pos (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    0 < p.radius :=
+  lt_of_lt_of_le hf.r_pos hf.r_le
+
 theorem HasFPowerSeriesAt.radius_pos (hf : HasFPowerSeriesAt f p x) : 0 < p.radius :=
   let ⟨_, hr⟩ := hf
   hr.radius_pos
 
+theorem HasFPowerSeriesWithinOnBall.of_le
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (r'_pos : 0 < r') (hr : r' ≤ r) :
+    HasFPowerSeriesWithinOnBall f p s x r' :=
+  ⟨le_trans hr hf.1, r'_pos, fun hy h'y => hf.hasSum hy (EMetric.ball_subset_ball hr h'y)⟩
+
 theorem HasFPowerSeriesOnBall.mono (hf : HasFPowerSeriesOnBall f p x r) (r'_pos : 0 < r')
     (hr : r' ≤ r) : HasFPowerSeriesOnBall f p x r' :=
   ⟨le_trans hr hf.1, r'_pos, fun hy => hf.hasSum (EMetric.ball_subset_ball hr hy)⟩
@@ -453,6 +478,12 @@ theorem HasFPowerSeriesAt.congr (hf : HasFPowerSeriesAt f p x) (hg : f =ᶠ[𝓝
     (h₁.mono (lt_min h₁.r_pos h₂pos) inf_le_left).congr
       fun y hy => h₂ (EMetric.ball_subset_ball inf_le_right hy)⟩
 
+protected theorem HasFPowerSeriesWithinAt.eventually (hf : HasFPowerSeriesWithinAt f p s x) :
+    ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFPowerSeriesWithinOnBall f p s x r :=
+  let ⟨_, hr⟩ := hf
+  mem_of_superset (Ioo_mem_nhdsWithin_Ioi (left_mem_Ico.2 hr.r_pos)) fun _ hr' =>
+    hr.of_le hr'.1 hr'.2.le
+
 protected theorem HasFPowerSeriesAt.eventually (hf : HasFPowerSeriesAt f p x) :
     ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFPowerSeriesOnBall f p x r :=
   let ⟨_, hr⟩ := hf
@@ -487,6 +518,59 @@ theorem HasFPowerSeriesAt.eventually_eq_zero
   let ⟨_, hr⟩ := hf
   hr.eventually_eq_zero
 
+@[simp] lemma hasFPowerSeriesWithinOnBall_univ :
+    HasFPowerSeriesWithinOnBall f p univ x r ↔ HasFPowerSeriesOnBall f p x r := by
+  constructor
+  · intro h
+    refine ⟨h.r_le, h.r_pos, fun {y} m ↦ h.hasSum (by simp) m⟩
+  · intro h
+    exact ⟨h.r_le, h.r_pos, fun {y} _ m => h.hasSum m⟩
+
+@[simp] lemma hasFPowerSeriesWithinAt_univ :
+    HasFPowerSeriesWithinAt f p univ x ↔ HasFPowerSeriesAt f p x := by
+  simp only [HasFPowerSeriesWithinAt, hasFPowerSeriesWithinOnBall_univ, HasFPowerSeriesAt]
+
+@[simp] lemma analyticWithinAt_univ :
+    AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x := by
+  simp [AnalyticWithinAt, AnalyticAt]
+
+@[simp] lemma analyticWithinOn_univ {f : E → F} :
+    AnalyticWithinOn 𝕜 f univ ↔ AnalyticOn 𝕜 f univ := by
+  simp only [AnalyticWithinOn, analyticWithinAt_univ, AnalyticOn]
+
+lemma HasFPowerSeriesWithinOnBall.mono (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : t ⊆ s) :
+    HasFPowerSeriesWithinOnBall f p t x r where
+  r_le := hf.r_le
+  r_pos := hf.r_pos
+  hasSum hy h'y := hf.hasSum (insert_subset_insert h hy) h'y
+
+lemma HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall (hf : HasFPowerSeriesOnBall f p x r) :
+    HasFPowerSeriesWithinOnBall f p s x r := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  exact hf.mono (subset_univ _)
+
+lemma HasFPowerSeriesWithinAt.mono (hf : HasFPowerSeriesWithinAt f p s x) (h : t ⊆ s) :
+    HasFPowerSeriesWithinAt f p t x := by
+  obtain ⟨r, hp⟩ := hf
+  exact ⟨r, hp.mono h⟩
+
+lemma HasFPowerSeriesAt.hasFPowerSeriesWithinAt (hf : HasFPowerSeriesAt f p x) :
+    HasFPowerSeriesWithinAt f p s x := by
+  rw [← hasFPowerSeriesWithinAt_univ] at hf
+  apply hf.mono (subset_univ _)
+
+lemma AnalyticWithinAt.mono (hf : AnalyticWithinAt 𝕜 f s x) (h : t ⊆ s) :
+    AnalyticWithinAt 𝕜 f t x := by
+  obtain ⟨p, hp⟩ := hf
+  exact ⟨p, hp.mono h⟩
+
+lemma AnalyticAt.analyticWithinAt (hf : AnalyticAt 𝕜 f x) : AnalyticWithinAt 𝕜 f s x := by
+  rw [← analyticWithinAt_univ] at hf
+  apply hf.mono (subset_univ _)
+
+lemma AnalyticOn.analyticWithinOn (hf : AnalyticOn 𝕜 f s) : AnalyticWithinOn 𝕜 f s :=
+  fun x hx ↦ (hf x hx).analyticWithinAt
+
 theorem hasFPowerSeriesOnBall_const {c : F} {e : E} :
     HasFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤ := by
   refine ⟨by simp, WithTop.zero_lt_top, fun _ => hasSum_single 0 fun n hn => ?_⟩
@@ -556,43 +640,53 @@ theorem AnalyticAt.sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
 theorem AnalyticOn.mono {s t : Set E} (hf : AnalyticOn 𝕜 f t) (hst : s ⊆ t) : AnalyticOn 𝕜 f s :=
   fun z hz => hf z (hst hz)
 
-theorem AnalyticOn.congr' {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
+theorem AnalyticOn.congr' (hf : AnalyticOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
     AnalyticOn 𝕜 g s :=
   fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)
 
-theorem analyticOn_congr' {s : Set E} (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s :=
+theorem analyticOn_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s :=
   ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩
 
-theorem AnalyticOn.congr {s : Set E} (hs : IsOpen s) (hf : AnalyticOn 𝕜 f s) (hg : s.EqOn f g) :
+theorem AnalyticOn.congr (hs : IsOpen s) (hf : AnalyticOn 𝕜 f s) (hg : s.EqOn f g) :
     AnalyticOn 𝕜 g s :=
   hf.congr' <| mem_nhdsSet_iff_forall.mpr
     (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)
 
-theorem analyticOn_congr {s : Set E} (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOn 𝕜 f s ↔
+theorem analyticOn_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOn 𝕜 f s ↔
     AnalyticOn 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩
 
-theorem AnalyticOn.add {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
+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)
 
-theorem AnalyticOn.neg {s : Set E} (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s :=
+theorem AnalyticOn.neg (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s :=
   fun z hz ↦ (hf z hz).neg
 
-theorem AnalyticOn.sub {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
+theorem AnalyticOn.sub (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
     AnalyticOn 𝕜 (f - g) s :=
   fun z hz => (hf z hz).sub (hg z hz)
 
-theorem HasFPowerSeriesOnBall.coeff_zero (hf : HasFPowerSeriesOnBall f pf x r) (v : Fin 0 → E) :
-    pf 0 v = f x := by
+theorem HasFPowerSeriesWithinOnBall.coeff_zero (hf : HasFPowerSeriesWithinOnBall f pf s x r)
+    (v : Fin 0 → E) : pf 0 v = f x := by
   have v_eq : v = fun i => 0 := Subsingleton.elim _ _
   have zero_mem : (0 : E) ∈ EMetric.ball (0 : E) r := by simp [hf.r_pos]
   have : ∀ i, i ≠ 0 → (pf i fun j => 0) = 0 := by
     intro i hi
     have : 0 < i := pos_iff_ne_zero.2 hi
     exact ContinuousMultilinearMap.map_coord_zero _ (⟨0, this⟩ : Fin i) rfl
-  have A := (hf.hasSum zero_mem).unique (hasSum_single _ this)
+  have A := (hf.hasSum (by simp) zero_mem).unique (hasSum_single _ this)
   simpa [v_eq] using A.symm
 
+theorem HasFPowerSeriesOnBall.coeff_zero (hf : HasFPowerSeriesOnBall f pf x r)
+    (v : Fin 0 → E) : pf 0 v = f x := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  exact hf.coeff_zero v
+
+theorem HasFPowerSeriesWithinAt.coeff_zero (hf : HasFPowerSeriesWithinAt f pf s x) (v : Fin 0 → E) :
+    pf 0 v = f x :=
+  let ⟨_, hrf⟩ := hf
+  hrf.coeff_zero v
+
 theorem HasFPowerSeriesAt.coeff_zero (hf : HasFPowerSeriesAt f pf x) (v : Fin 0 → E) :
     pf 0 v = f x :=
   let ⟨_, hrf⟩ := hf
@@ -622,14 +716,14 @@ theorem ContinuousLinearMap.comp_analyticOn {s : Set E} (g : F →L[𝕜] G) (h
 sums of this power series on strict subdisks of the disk of convergence.
 
 This version provides an upper estimate that decreases both in `‖y‖` and `n`. See also
-`HasFPowerSeriesOnBall.uniform_geometric_approx` for a weaker version. -/
-theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
-    (hf : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
-    ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
+`HasFPowerSeriesWithinOnBall.uniform_geometric_approx` for a weaker version. -/
+theorem HasFPowerSeriesWithinOnBall.uniform_geometric_approx' {r' : ℝ≥0}
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
+    ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n, x + y ∈ insert x s →
       ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n := by
   obtain ⟨a, ha, C, hC, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n, ‖p n‖ * (r' : ℝ) ^ n ≤ C * a ^ n :=
     p.norm_mul_pow_le_mul_pow_of_lt_radius (h.trans_le hf.r_le)
-  refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), fun y hy n => ?_⟩
+  refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), fun y hy n ys => ?_⟩
   have yr' : ‖y‖ < r' := by
     rw [ball_zero_eq] at hy
     exact hy
@@ -645,7 +739,7 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
     have : 0 < a := ha.1
     gcongr
     apply_rules [sub_pos.2, ha.2]
-  apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.hasSum this)
+  apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.hasSum ys this)
   intro n
   calc
     ‖(p n) fun _ : Fin n => y‖
@@ -655,58 +749,94 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
     _ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc]
 
 /-- If a function admits a power series expansion, then it is exponentially close to the partial
-sums of this power series on strict subdisks of the disk of convergence. -/
-theorem HasFPowerSeriesOnBall.uniform_geometric_approx {r' : ℝ≥0}
+sums of this power series on strict subdisks of the disk of convergence.
+
+This version provides an upper estimate that decreases both in `‖y‖` and `n`. See also
+`HasFPowerSeriesOnBall.uniform_geometric_approx` for a weaker version. -/
+theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
     (hf : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
+    ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
+      ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n := by
+   rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+   simpa using hf.uniform_geometric_approx' h
+
+/-- If a function admits a power series expansion within a set in a ball, then it is exponentially
+close to the partial sums of this power series on strict subdisks of the disk of convergence. -/
+theorem HasFPowerSeriesWithinOnBall.uniform_geometric_approx {r' : ℝ≥0}
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
     ∃ a ∈ Ioo (0 : ℝ) 1,
-      ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n, ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := by
+      ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n, x + y ∈ insert x s →
+      ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := by
   obtain ⟨a, ha, C, hC, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
-      ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
+      x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
     hf.uniform_geometric_approx' h
-  refine ⟨a, ha, C, hC, fun y hy n => (hp y hy n).trans ?_⟩
+  refine ⟨a, ha, C, hC, fun y hy n ys => (hp y hy n ys).trans ?_⟩
   have yr' : ‖y‖ < r' := by rwa [ball_zero_eq] at hy
   have := ha.1.le -- needed to discharge a side goal on the next line
   gcongr
   exact mul_le_of_le_one_right ha.1.le (div_le_one_of_le yr'.le r'.coe_nonneg)
 
-/-- Taylor formula for an analytic function, `IsBigO` version. -/
-theorem HasFPowerSeriesAt.isBigO_sub_partialSum_pow (hf : HasFPowerSeriesAt f p x) (n : ℕ) :
-    (fun y : E => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n := by
+/-- If a function admits a power series expansion, then it is exponentially close to the partial
+sums of this power series on strict subdisks of the disk of convergence. -/
+theorem HasFPowerSeriesOnBall.uniform_geometric_approx {r' : ℝ≥0}
+    (hf : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
+    ∃ a ∈ Ioo (0 : ℝ) 1,
+      ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
+      ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.uniform_geometric_approx h
+
+/-- Taylor formula for an analytic function within a set, `IsBigO` version. -/
+theorem HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow
+    (hf : HasFPowerSeriesWithinAt f p s x) (n : ℕ) :
+    (fun y : E => f (x + y) - p.partialSum n y)
+      =O[𝓝[(x + ·)⁻¹' insert x s] 0] fun y => ‖y‖ ^ n := by
   rcases hf with ⟨r, hf⟩
   rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
   obtain ⟨a, -, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
-      ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
+      x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
     hf.uniform_geometric_approx' h
   refine isBigO_iff.2 ⟨C * (a / r') ^ n, ?_⟩
   replace r'0 : 0 < (r' : ℝ) := mod_cast r'0
-  filter_upwards [Metric.ball_mem_nhds (0 : E) r'0] with y hy
-  simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div] using hp y hy n
+  filter_upwards [inter_mem_nhdsWithin _ (Metric.ball_mem_nhds (0 : E) r'0)] with y hy
+  simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div]
+    using hp y hy.2 n (by simpa using hy.1)
 
-/-- If `f` has formal power series `∑ n, pₙ` on a ball of radius `r`, then for `y, z` in any smaller
-ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by
-`C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This lemma formulates this property using `IsBigO` and
-`Filter.principal` on `E × E`. -/
-theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
-    (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
-    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r')]
+/-- Taylor formula for an analytic function, `IsBigO` version. -/
+theorem HasFPowerSeriesAt.isBigO_sub_partialSum_pow
+    (hf : HasFPowerSeriesAt f p x) (n : ℕ) :
+    (fun y : E => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n := by
+  rw [← hasFPowerSeriesWithinAt_univ] at hf
+  simpa using hf.isBigO_sub_partialSum_pow n
+
+/-- If `f` has formal power series `∑ n, pₙ` in a set, within a ball of radius `r`, then
+for `y, z` in any smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is
+bounded above by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This lemma formulates this property
+using `IsBigO` and `Filter.principal` on `E × E`. -/
+theorem HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
+    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2)
+      =O[𝓟 (EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)))]
       fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ := by
   lift r' to ℝ≥0 using ne_top_of_lt hr
   rcases (zero_le r').eq_or_lt with (rfl | hr'0)
-  · simp only [isBigO_bot, EMetric.ball_zero, principal_empty, ENNReal.coe_zero]
+  · simp only [ENNReal.coe_zero, EMetric.ball_zero, empty_inter, principal_empty, isBigO_bot]
   obtain ⟨a, ha, C, hC : 0 < C, hp⟩ :
       ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n : ℕ, ‖p n‖ * (r' : ℝ) ^ n ≤ C * a ^ n :=
     p.norm_mul_pow_le_mul_pow_of_lt_radius (hr.trans_le hf.r_le)
   simp only [← le_div_iff₀ (pow_pos (NNReal.coe_pos.2 hr'0) _)] at hp
   set L : E × E → ℝ := fun y =>
     C * (a / r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
-  have hL : ∀ y ∈ EMetric.ball (x, x) r', ‖f y.1 - f y.2 - p 1 fun _ => y.1 - y.2‖ ≤ L y := by
-    intro y hy'
+  have hL : ∀ y ∈ EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)),
+      ‖f y.1 - f y.2 - p 1 fun _ => y.1 - y.2‖ ≤ L y := by
+    intro y ⟨hy', ys⟩
     have hy : y ∈ EMetric.ball x r ×ˢ EMetric.ball x r := by
       rw [EMetric.ball_prod_same]
       exact EMetric.ball_subset_ball hr.le hy'
     set A : ℕ → F := fun n => (p n fun _ => y.1 - x) - p n fun _ => y.2 - x
     have hA : HasSum (fun n => A (n + 2)) (f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) := by
-      convert (hasSum_nat_add_iff' 2).2 ((hf.hasSum_sub hy.1).sub (hf.hasSum_sub hy.2)) using 1
+      convert (hasSum_nat_add_iff' 2).2
+        ((hf.hasSum_sub ⟨ys.1, hy.1⟩).sub (hf.hasSum_sub ⟨ys.2, hy.2⟩)) using 1
       rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
         zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
         ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_sub, ← Pi.single,
@@ -742,23 +872,60 @@ theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
       exact (hasSum_coe_mul_geometric_of_norm_lt_one this).add  -- Porting note: was `convert`!
           ((hasSum_geometric_of_norm_lt_one this).mul_left 2)
     exact hA.norm_le_of_bounded hBL hAB
-  suffices L =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ by
+  suffices L =O[𝓟 (EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)))]
+      fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ by
     refine (IsBigO.of_bound 1 (eventually_principal.2 fun y hy => ?_)).trans this
     rw [one_mul]
     exact (hL y hy).trans (le_abs_self _)
   simp_rw [L, mul_right_comm _ (_ * _)]
   exact (isBigO_refl _ _).const_mul_left _
 
+/-- If `f` has formal power series `∑ n, pₙ` on a ball of radius `r`, then for `y, z` in any smaller
+ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by
+`C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This lemma formulates this property using `IsBigO` and
+`Filter.principal` on `E × E`. -/
+theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
+    (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
+    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2)
+      =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.isBigO_image_sub_image_sub_deriv_principal hr
+
+/-- If `f` has formal power series `∑ n, pₙ` within a set, on a ball of radius `r`, then for `y, z`
+in any smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above
+by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. -/
+theorem HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
+    ∃ C, ∀ᵉ (y ∈ insert x s ∩ EMetric.ball x r') (z ∈ insert x s ∩ EMetric.ball x r'),
+      ‖f y - f z - p 1 fun _ => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖ := by
+  have := hf.isBigO_image_sub_image_sub_deriv_principal hr
+  simp only [isBigO_principal, mem_inter_iff, EMetric.mem_ball, Prod.edist_eq, max_lt_iff, mem_prod,
+    norm_mul, Real.norm_eq_abs, abs_norm, and_imp, Prod.forall, mul_assoc] at this ⊢
+  rcases this with ⟨C, hC⟩
+  exact ⟨C, fun y ys hy z zs hz ↦ hC y z hy hz ys zs⟩
+
 /-- If `f` has formal power series `∑ n, pₙ` on a ball of radius `r`, then for `y, z` in any smaller
 ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by
 `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. -/
-theorem HasFPowerSeriesOnBall.image_sub_sub_deriv_le (hf : HasFPowerSeriesOnBall f p x r)
-    (hr : r' < r) :
+theorem HasFPowerSeriesOnBall.image_sub_sub_deriv_le
+    (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
     ∃ C, ∀ᵉ (y ∈ EMetric.ball x r') (z ∈ EMetric.ball x r'),
       ‖f y - f z - p 1 fun _ => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖ := by
-  simpa only [isBigO_principal, mul_assoc, norm_mul, norm_norm, Prod.forall, EMetric.mem_ball,
-    Prod.edist_eq, max_lt_iff, and_imp, @forall_swap (_ < _) E] using
-    hf.isBigO_image_sub_image_sub_deriv_principal hr
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa only [mem_univ, insert_eq_of_mem, univ_inter] using hf.image_sub_sub_deriv_le hr
+
+/-- If `f` has formal power series `∑ n, pₙ` at `x` within a set `s`, then
+`f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)` as `(y, z) → (x, x)`
+within `s × s`. -/
+theorem HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub
+    (hf : HasFPowerSeriesWithinAt f p s x) :
+    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2)
+      =O[𝓝[(insert x s) ×ˢ (insert x s)] (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ := by
+  rcases hf with ⟨r, hf⟩
+  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
+  refine (hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_
+  rw [inter_comm]
+  exact le_principal_iff.2 (inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ r'0))
 
 /-- If `f` has formal power series `∑ n, pₙ` at `x`, then
 `f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)` as `(y, z) → (x, x)`.
@@ -766,27 +933,52 @@ In particular, `f` is strictly differentiable at `x`. -/
 theorem HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub (hf : HasFPowerSeriesAt f p x) :
     (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) =O[𝓝 (x, x)] fun y =>
       ‖y - (x, x)‖ * ‖y.1 - y.2‖ := by
-  rcases hf with ⟨r, hf⟩
-  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
-  refine (hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_
-  exact le_principal_iff.2 (EMetric.ball_mem_nhds _ r'0)
-
-/-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
-partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f (x + y)`
-is the uniform limit of `p.partialSum n y` there. -/
-theorem HasFPowerSeriesOnBall.tendstoUniformlyOn {r' : ℝ≥0} (hf : HasFPowerSeriesOnBall f p x r)
-    (h : (r' : ℝ≥0∞) < r) :
+  rw [← hasFPowerSeriesWithinAt_univ] at hf
+  simpa using hf.isBigO_image_sub_norm_mul_norm_sub
+
+/-- If a function admits a power series expansion within a set at `x`, then it is the uniform limit
+of the partial sums of this power series on strict subdisks of the disk of convergence, i.e.,
+`f (x + y)` is the uniform limit of `p.partialSum n y` there. -/
+theorem HasFPowerSeriesWithinOnBall.tendstoUniformlyOn {r' : ℝ≥0}
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
     TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
-      (Metric.ball (0 : E) r') := by
+      ((x + ·)⁻¹' (insert x s) ∩ Metric.ball (0 : E) r') := by
   obtain ⟨a, ha, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
-    ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := hf.uniform_geometric_approx h
+    x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := hf.uniform_geometric_approx h
   refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_
   have L : Tendsto (fun n => (C : ℝ) * a ^ n) atTop (𝓝 ((C : ℝ) * 0)) :=
     tendsto_const_nhds.mul (tendsto_pow_atTop_nhds_zero_of_lt_one ha.1.le ha.2)
   rw [mul_zero] at L
   refine (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_
   rw [dist_eq_norm]
-  exact (hp y hy n).trans_lt hn
+  exact (hp y hy.2 n hy.1).trans_lt hn
+
+/-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
+partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f (x + y)`
+is the uniform limit of `p.partialSum n y` there. -/
+theorem HasFPowerSeriesOnBall.tendstoUniformlyOn {r' : ℝ≥0} (hf : HasFPowerSeriesOnBall f p x r)
+    (h : (r' : ℝ≥0∞) < r) :
+    TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
+      (Metric.ball (0 : E) r') := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.tendstoUniformlyOn h
+
+/-- If a function admits a power series expansion within a set at `x`, then it is the locally
+uniform limit of the partial sums of this power series on the disk of convergence, i.e., `f (x + y)`
+is the locally uniform limit of `p.partialSum n y` there. -/
+theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
+      ((x + ·)⁻¹' (insert x s) ∩ EMetric.ball (0 : E) r) := by
+  intro u hu y hy
+  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hy.2 with ⟨r', yr', hr'⟩
+  have : EMetric.ball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds EMetric.isOpen_ball yr'
+  refine ⟨(x + ·)⁻¹' (insert x s) ∩ EMetric.ball (0 : E) r', ?_, ?_⟩
+  · rw [nhdsWithin_inter_of_mem']
+    · exact inter_mem_nhdsWithin _ this
+    · apply mem_nhdsWithin_of_mem_nhds
+      apply Filter.mem_of_superset this (EMetric.ball_subset_ball hr'.le)
+  · simpa [Metric.emetric_ball_nnreal] using hf.tendstoUniformlyOn hr' u hu
 
 /-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
 the partial sums of this power series on the disk of convergence, i.e., `f (x + y)`
@@ -794,11 +986,20 @@ is the locally uniform limit of `p.partialSum n y` there. -/
 theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn (hf : HasFPowerSeriesOnBall f p x r) :
     TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
       (EMetric.ball (0 : E) r) := by
-  intro u hu x hx
-  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hx with ⟨r', xr', hr'⟩
-  have : EMetric.ball (0 : E) r' ∈ 𝓝 x := IsOpen.mem_nhds EMetric.isOpen_ball xr'
-  refine ⟨EMetric.ball (0 : E) r', mem_nhdsWithin_of_mem_nhds this, ?_⟩
-  simpa [Metric.emetric_ball_nnreal] using hf.tendstoUniformlyOn hr' u hu
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.tendstoLocallyUniformlyOn
+
+/-- If a function admits a power series expansion within a set at `x`, then it is the uniform limit
+of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
+is the uniform limit of `p.partialSum n (y - x)` there. -/
+theorem HasFPowerSeriesWithinOnBall.tendstoUniformlyOn' {r' : ℝ≥0}
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
+    TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop
+      (insert x s ∩ Metric.ball (x : E) r') := by
+  convert (hf.tendstoUniformlyOn h).comp fun y => y - x using 1
+  · simp [Function.comp_def]
+  · ext z
+    simp [dist_eq_norm]
 
 /-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
 partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
@@ -806,18 +1007,17 @@ is the uniform limit of `p.partialSum n (y - x)` there. -/
 theorem HasFPowerSeriesOnBall.tendstoUniformlyOn' {r' : ℝ≥0} (hf : HasFPowerSeriesOnBall f p x r)
     (h : (r' : ℝ≥0∞) < r) :
     TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball (x : E) r') := by
-  convert (hf.tendstoUniformlyOn h).comp fun y => y - x using 1
-  · simp [Function.comp_def]
-  · ext z
-    simp [dist_eq_norm]
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.tendstoUniformlyOn' h
 
-/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
-the partial sums of this power series on the disk of convergence, i.e., `f y`
+/-- If a function admits a power series expansion within a set at `x`, then it is the locally
+uniform limit of the partial sums of this power series on the disk of convergence, i.e., `f y`
 is the locally uniform limit of `p.partialSum n (y - x)` there. -/
-theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' (hf : HasFPowerSeriesOnBall f p x r) :
+theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
     TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop
-      (EMetric.ball (x : E) r) := by
-  have A : ContinuousOn (fun y : E => y - x) (EMetric.ball (x : E) r) :=
+      (insert x s ∩ EMetric.ball (x : E) r) := by
+  have A : ContinuousOn (fun y : E => y - x) (insert x s ∩ EMetric.ball (x : E) r) :=
     (continuous_id.sub continuous_const).continuousOn
   convert hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A using 1
   · ext z
@@ -825,18 +1025,66 @@ theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' (hf : HasFPowerSeriesOn
   · intro z
     simp [edist_eq_coe_nnnorm, edist_eq_coe_nnnorm_sub]
 
-/-- If a function admits a power series expansion on a disk, then it is continuous there. -/
-protected theorem HasFPowerSeriesOnBall.continuousOn (hf : HasFPowerSeriesOnBall f p x r) :
-    ContinuousOn f (EMetric.ball x r) :=
+/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
+the partial sums of this power series on the disk of convergence, i.e., `f y`
+is the locally uniform limit of `p.partialSum n (y - x)` there. -/
+theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' (hf : HasFPowerSeriesOnBall f p x r) :
+    TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop
+      (EMetric.ball (x : E) r) := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.tendstoLocallyUniformlyOn'
+
+/-- If a function admits a power series expansion within a set on a ball, then it is
+continuous there. -/
+protected theorem HasFPowerSeriesWithinOnBall.continuousOn
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    ContinuousOn f (insert x s ∩ EMetric.ball x r) :=
   hf.tendstoLocallyUniformlyOn'.continuousOn <|
     Eventually.of_forall fun n =>
       ((p.partialSum_continuous n).comp (continuous_id.sub continuous_const)).continuousOn
 
+/-- If a function admits a power series expansion on a ball, then it is continuous there. -/
+protected theorem HasFPowerSeriesOnBall.continuousOn (hf : HasFPowerSeriesOnBall f p x r) :
+    ContinuousOn f (EMetric.ball x r) := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  simpa using hf.continuousOn
+
+protected theorem HasFPowerSeriesWithinOnBall.continuousWithinAt_insert
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    ContinuousWithinAt f (insert x s) x := by
+  apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem
+  exact inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds x hf.r_pos)
+
+protected theorem HasFPowerSeriesWithinOnBall.continuousWithinAt
+    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    ContinuousWithinAt f s x :=
+  hf.continuousWithinAt_insert.mono (subset_insert x s)
+
+protected theorem HasFPowerSeriesWithinAt.continuousWithinAt_insert
+    (hf : HasFPowerSeriesWithinAt f p s x) :
+    ContinuousWithinAt f (insert x s) x := by
+  rcases hf with ⟨r, hr⟩
+  apply hr.continuousWithinAt_insert
+
+protected theorem HasFPowerSeriesWithinAt.continuousWithinAt
+    (hf : HasFPowerSeriesWithinAt f p s x) :
+    ContinuousWithinAt f s x :=
+  hf.continuousWithinAt_insert.mono (subset_insert x s)
+
 protected theorem HasFPowerSeriesAt.continuousAt (hf : HasFPowerSeriesAt f p x) :
     ContinuousAt f x :=
   let ⟨_, hr⟩ := hf
   hr.continuousOn.continuousAt (EMetric.ball_mem_nhds x hr.r_pos)
 
+protected theorem AnalyticWithinAt.continuousWithinAt_insert (hf : AnalyticWithinAt 𝕜 f s x) :
+    ContinuousWithinAt f (insert x s) x :=
+  let ⟨_, hp⟩ := hf
+  hp.continuousWithinAt_insert
+
+protected theorem AnalyticWithinAt.continuousWithinAt (hf : AnalyticWithinAt 𝕜 f s x) :
+    ContinuousWithinAt f s x :=
+  hf.continuousWithinAt_insert.mono (subset_insert x s)
+
 protected theorem AnalyticAt.continuousAt (hf : AnalyticAt 𝕜 f x) : ContinuousAt f x :=
   let ⟨_, hp⟩ := hf
   hp.continuousAt
@@ -1318,11 +1566,11 @@ variable {𝕜}
 
 theorem AnalyticAt.eventually_analyticAt {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
     ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y :=
-(isOpen_analyticAt 𝕜 f).mem_nhds h
+  (isOpen_analyticAt 𝕜 f).mem_nhds h
 
 theorem AnalyticAt.exists_mem_nhds_analyticOn {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
     ∃ s ∈ 𝓝 x, AnalyticOn 𝕜 f s :=
-h.eventually_analyticAt.exists_mem
+  h.eventually_analyticAt.exists_mem
 
 /-- If we're analytic at a point, we're analytic in a nonempty ball -/
 theorem AnalyticAt.exists_ball_analyticOn {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) :
@@ -1368,3 +1616,6 @@ theorem hasFPowerSeriesAt_iff' :
   simp_rw [add_sub_cancel_left]
 
 end
+
+/- TODO: move the part on `ChangeOrigin` to another file. -/
+set_option linter.style.longFile 1800
diff --git a/Mathlib/Analysis/Analytic/Within.lean b/Mathlib/Analysis/Analytic/Within.lean
index d8c30c30b6b97..f751863294169 100644
--- a/Mathlib/Analysis/Analytic/Within.lean
+++ b/Mathlib/Analysis/Analytic/Within.lean
@@ -11,8 +11,7 @@ import Mathlib.Analysis.Calculus.FDeriv.Analytic
 
 From `Mathlib.Analysis.Analytic.Basic`, we have the definitions
 
-1. `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[s] x`, and
-    `f` is continuous within `s` at `x`.
+1. `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[insert x s] x`.
 2. `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
 
 This means there exists an extension of `f` which is analytic and agrees with `f` on `s ∪ {x}`, but
@@ -40,43 +39,9 @@ variable {E F G H : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAd
 ### Basic properties
 -/
 
-@[simp] lemma hasFPowerSeriesWithinOnBall_univ {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
-    {x : E} {r : ℝ≥0∞} :
-    HasFPowerSeriesWithinOnBall f p univ x r ↔ HasFPowerSeriesOnBall f p x r := by
-  constructor
-  · intro h
-    exact ⟨h.r_le, h.r_pos, fun {y} m ↦ h.hasSum (mem_univ _) m⟩
-  · intro h
-    refine ⟨h.r_le, h.r_pos, fun {y} _ m => h.hasSum m, ?_⟩
-    exact (h.continuousOn.continuousAt (EMetric.ball_mem_nhds x h.r_pos)).continuousWithinAt
-
-@[simp] lemma hasFPowerSeriesWithinAt_univ {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} :
-    HasFPowerSeriesWithinAt f p univ x ↔ HasFPowerSeriesAt f p x := by
-  simp only [HasFPowerSeriesWithinAt, hasFPowerSeriesWithinOnBall_univ, HasFPowerSeriesAt]
-
-@[simp] lemma analyticWithinAt_univ {f : E → F} {x : E} :
-    AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x := by
-  simp only [AnalyticWithinAt, hasFPowerSeriesWithinAt_univ, AnalyticAt]
-
-lemma analyticWithinOn_univ {f : E → F} :
-    AnalyticWithinOn 𝕜 f univ ↔ AnalyticOn 𝕜 f univ := by
-  simp only [AnalyticWithinOn, analyticWithinAt_univ, AnalyticOn]
-
-lemma HasFPowerSeriesWithinAt.continuousWithinAt {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
-    {s : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p s x) : ContinuousWithinAt f s x := by
-  rcases h with ⟨r, h⟩
-  exact h.continuousWithinAt
-
-lemma AnalyticWithinAt.continuousWithinAt {f : E → F} {s : Set E} {x : E}
-    (h : AnalyticWithinAt 𝕜 f s x) : ContinuousWithinAt f s x := by
-  rcases h with ⟨p, h⟩
-  exact h.continuousWithinAt
-
 /-- `AnalyticWithinAt` is trivial if `{x} ∈ 𝓝[s] x` -/
 lemma analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : {x} ∈ 𝓝[s] x) :
     AnalyticWithinAt 𝕜 f s x := by
-  have fc : ContinuousWithinAt f s x :=
-    Filter.Tendsto.mono_left (tendsto_pure_nhds _ _) (Filter.le_pure_iff.mpr h)
   rcases mem_nhdsWithin.mp h with ⟨t, ot, xt, st⟩
   rcases Metric.mem_nhds_iff.mp (ot.mem_nhds xt) with ⟨r, r0, rt⟩
   exact ⟨constFormalMultilinearSeries 𝕜 E (f x), .ofReal r, {
@@ -85,29 +50,14 @@ lemma analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : {
     hasSum := by
       intro y ys yr
       simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st
-      specialize st (x + y) (rt (by simpa using yr)) ys
-      simp only [st]
+      simp only [mem_insert_iff, add_right_eq_self] at ys
+      have : x + y = x := by
+        rcases ys with rfl | ys
+        · simp
+        · exact st (x + y) (rt (by simpa using yr)) ys
+      simp only [this]
       apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum
-      simp only [Metric.emetric_ball_top, mem_univ]
-    continuousWithinAt := fc
-  }⟩
-
-/-- Analyticity implies analyticity within any `s` -/
-lemma AnalyticAt.analyticWithinAt {f : E → F} {s : Set E} {x : E} (h : AnalyticAt 𝕜 f x) :
-    AnalyticWithinAt 𝕜 f s x := by
-  rcases h with ⟨p, r, hp⟩
-  exact ⟨p, r, {
-    r_le := hp.r_le
-    r_pos := hp.r_pos
-    hasSum := fun {y} _ yr ↦ hp.hasSum yr
-    continuousWithinAt :=
-      (hp.continuousOn.continuousAt (EMetric.ball_mem_nhds x hp.r_pos)).continuousWithinAt
-  }⟩
-
-/-- Analyticity on `s` implies analyticity within `s` -/
-lemma AnalyticOn.analyticWithinOn {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) :
-    AnalyticWithinOn 𝕜 f s :=
-  fun x m ↦ (h x m).analyticWithinAt
+      simp only [Metric.emetric_ball_top, mem_univ] }⟩
 
 lemma AnalyticWithinOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticWithinOn 𝕜 f s) :
     ContinuousOn f s :=
@@ -125,18 +75,19 @@ lemma analyticWithinOn_of_locally_analyticWithinOn {f : E → F} {s : Set E}
     r_pos := lt_min (by positivity) fp.r_pos
     r_le := min_le_of_right_le fp.r_le
     hasSum := by
-      intro y ys yr
-      simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at yr
-      apply fp.hasSum ⟨ys, ru ?_⟩
-      · simp only [EMetric.mem_ball, yr]
-      · simp only [Metric.mem_ball, dist_self_add_left, yr]
-    continuousWithinAt := by
-      refine (fu.continuousOn x ⟨m, xu⟩).mono_left (le_of_eq ?_)
-      exact nhdsWithin_eq_nhdsWithin xu ou (by simp only [inter_assoc, inter_self])
-  }⟩
+        intro y ys yr
+        simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at yr
+        apply fp.hasSum
+        · simp only [mem_insert_iff, add_right_eq_self] at ys
+          rcases ys with rfl | ys
+          · simp
+          · simp only [mem_insert_iff, add_right_eq_self, mem_inter_iff, ys, true_and]
+            apply Or.inr (ru ?_)
+            simp only [Metric.mem_ball, dist_self_add_left, yr]
+        · simp only [EMetric.mem_ball, yr] }⟩
 
 /-- On open sets, `AnalyticOn` and `AnalyticWithinOn` coincide -/
-@[simp] lemma IsOpen.analyticWithinOn_iff_analyticOn {f : E → F} {s : Set E} (hs : IsOpen s) :
+lemma IsOpen.analyticWithinOn_iff_analyticOn {f : E → F} {s : Set E} (hs : IsOpen s) :
     AnalyticWithinOn 𝕜 f s ↔ AnalyticOn 𝕜 f s := by
   refine ⟨?_, AnalyticOn.analyticWithinOn⟩
   intro hf x m
@@ -148,9 +99,11 @@ lemma analyticWithinOn_of_locally_analyticWithinOn {f : E → F} {s : Set E}
     hasSum := by
       intro y ym
       simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym
-      refine fp.hasSum (rs ?_) ym.2
-      simp only [Metric.mem_ball, dist_self_add_left, ym.1]
-  }⟩
+      refine fp.hasSum ?_ ym.2
+      apply mem_insert_of_mem
+      apply rs
+      simp only [Metric.mem_ball, dist_self_add_left, ym.1] }⟩
+
 
 /-!
 ### Equivalence to analyticity of a local extension
@@ -165,11 +118,11 @@ be stitched together.
 lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpace F] {f : E → F}
     {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ℝ≥0∞} :
     HasFPowerSeriesWithinOnBall f p s x r ↔
-      ContinuousWithinAt f s x ∧ ∃ g, EqOn f g (s ∩ EMetric.ball x r) ∧
+      ∃ g, EqOn f g (insert x s ∩ EMetric.ball x r) ∧
         HasFPowerSeriesOnBall g p x r := by
   constructor
   · intro h
-    refine ⟨h.continuousWithinAt, fun y ↦ p.sum (y - x), ?_, ?_⟩
+    refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
     · intro y ⟨ys,yb⟩
       simp only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub] at yb
       have e0 := p.hasSum (x := y - x) ?_
@@ -186,8 +139,8 @@ lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpac
       apply p.hasSum
       simp only [EMetric.mem_ball] at lt ⊢
       exact lt_of_lt_of_le lt h.r_le
-  · intro ⟨mem, g, hfg, hg⟩
-    refine ⟨hg.r_le, hg.r_pos, ?_, mem⟩
+  · intro ⟨g, hfg, hg⟩
+    refine ⟨hg.r_le, hg.r_pos, ?_⟩
     intro y ys lt
     rw [hfg]
     · exact hg.hasSum lt
@@ -198,18 +151,18 @@ lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpac
 lemma hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt [CompleteSpace F] {f : E → F}
     {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} :
     HasFPowerSeriesWithinAt f p s x ↔
-      ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ HasFPowerSeriesAt g p x := by
+      ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x := by
   constructor
   · intro ⟨r, h⟩
-    rcases hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mp h with ⟨fc, g, e, h⟩
-    refine ⟨fc, g, ?_, ⟨r, h⟩⟩
+    rcases hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mp h with ⟨g, e, h⟩
+    refine ⟨g, ?_, ⟨r, h⟩⟩
     refine Filter.eventuallyEq_iff_exists_mem.mpr ⟨_, ?_, e⟩
     exact inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ h.r_pos)
-  · intro ⟨mem, g, hfg, ⟨r, hg⟩⟩
+  · intro ⟨g, hfg, ⟨r, hg⟩⟩
     simp only [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff] at hfg
     rcases hfg with ⟨e, e0, hfg⟩
     refine ⟨min r (.ofReal e), ?_⟩
-    refine hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨mem, g, ?_, ?_⟩
+    refine hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨g, ?_, ?_⟩
     · intro y ⟨ys, xy⟩
       refine hfg ?_ ys
       simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal] at xy
@@ -219,43 +172,83 @@ lemma hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt [CompleteSpace F] {f
 /-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x` -/
 lemma analyticWithinAt_iff_exists_analyticAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
     AnalyticWithinAt 𝕜 f s x ↔
-      ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ AnalyticAt 𝕜 g x := by
+      ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x := by
   simp only [AnalyticWithinAt, AnalyticAt, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt]
   tauto
 
-/-- If `f` is analytic within `s` at `x`, some local extension of `f` is analytic at `x` -/
-lemma AnalyticWithinAt.exists_analyticAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
-    (h : AnalyticWithinAt 𝕜 f s x) : ∃ g, f x = g x ∧ f =ᶠ[𝓝[s] x] g ∧ AnalyticAt 𝕜 g x := by
-  by_cases s0 : 𝓝[s] x = ⊥
-  · refine ⟨fun _ ↦ f x, rfl, ?_, analyticAt_const⟩
-    simp only [EventuallyEq, s0, eventually_bot]
-  · rcases analyticWithinAt_iff_exists_analyticAt.mp h with ⟨_, g, fg, hg⟩
-    refine ⟨g, ?_, fg, hg⟩
-    exact tendsto_nhds_unique' ⟨s0⟩ h.continuousWithinAt
-      (hg.continuousAt.continuousWithinAt.congr' fg.symm)
+/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`. In this
+version, we make sure that the extension coincides with `f` on all of `insert x s`. -/
+lemma analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
+    AnalyticWithinAt 𝕜 f s x ↔
+      ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x := by
+  classical
+  simp only [analyticWithinAt_iff_exists_analyticAt]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨g, hf, hg⟩
+    rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
+    let g' := Set.piecewise u g f
+    refine ⟨g', ?_, ?_, ?_⟩
+    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
+      simpa [g', xu, this] using hu this
+    · intro y hy
+      by_cases h'y : y ∈ u
+      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
+        simpa [g', h'y, this] using hu this
+      · simp [g', h'y]
+    · apply hg.congr
+      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
+  · rintro ⟨g, -, hf, hg⟩
+    exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
+
+alias ⟨AnalyticWithinAt.exists_analyticAt, _⟩ := analyticWithinAt_iff_exists_analyticAt'
 
 /-!
 ### Congruence
 
-We require completeness to use equivalence to locally extensions, but this is nonessential.
 -/
 
-lemma AnalyticWithinAt.congr_of_eventuallyEq [CompleteSpace F] {f g : E → F} {s : Set E} {x : E}
-    (hf : AnalyticWithinAt 𝕜 f s x) (hs : f =ᶠ[𝓝[s] x] g) (hx : f x = g x) :
+
+lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
+    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
+    (h' : EqOn g f (s ∩ EMetric.ball x r)) (h'' : g x = f x) :
+    HasFPowerSeriesWithinOnBall g p s x r := by
+  refine ⟨h.r_le, h.r_pos, ?_⟩
+  · intro y hy h'y
+    convert h.hasSum hy h'y using 1
+    simp only [mem_insert_iff, add_right_eq_self] at hy
+    rcases hy with rfl | hy
+    · simpa using h''
+    · apply h'
+      refine ⟨hy, ?_⟩
+      simpa [edist_eq_coe_nnnorm_sub] using h'y
+
+lemma HasFPowerSeriesWithinAt.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
+    {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) :
+    HasFPowerSeriesWithinAt g p s x := by
+  rcases h with ⟨r, hr⟩
+  obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, EMetric.ball x ε ∩ s ⊆ {y | g y = f y} :=
+    EMetric.mem_nhdsWithin_iff.1 h'
+  let r' := min r ε
+  refine ⟨r', ?_⟩
+  have := hr.of_le (r' := r') (by simp [r', εpos, hr.r_pos]) (min_le_left _ _)
+  apply this.congr _ h''
+  intro z hz
+  exact hε ⟨EMetric.ball_subset_ball (min_le_right _ _) hz.2, hz.1⟩
+
+
+lemma AnalyticWithinAt.congr_of_eventuallyEq {f g : E → F} {s : Set E} {x : E}
+    (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) :
     AnalyticWithinAt 𝕜 g s x := by
-  rcases hf.exists_analyticAt with ⟨f', fx, ef, hf'⟩
-  rw [analyticWithinAt_iff_exists_analyticAt]
-  have eg := hs.symm.trans ef
-  refine ⟨?_, f', eg, hf'⟩
-  exact hf'.continuousAt.continuousWithinAt.congr_of_eventuallyEq eg (hx.symm.trans fx)
-
-lemma AnalyticWithinAt.congr [CompleteSpace F] {f g : E → F} {s : Set E} {x : E}
-    (hf : AnalyticWithinAt 𝕜 f s x) (hs : EqOn f g s) (hx : f x = g x) :
+  rcases hf with ⟨p, hp⟩
+  exact ⟨p, hp.congr hs hx⟩
+
+lemma AnalyticWithinAt.congr {f g : E → F} {s : Set E} {x : E}
+    (hf : AnalyticWithinAt 𝕜 f s x) (hs : EqOn g f s) (hx : g x = f x) :
     AnalyticWithinAt 𝕜 g s x :=
   hf.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx
 
-lemma AnalyticWithinOn.congr [CompleteSpace F] {f g : E → F} {s : Set E}
-    (hf : AnalyticWithinOn 𝕜 f s) (hs : EqOn f g s) :
+lemma AnalyticWithinOn.congr {f g : E → F} {s : Set E}
+    (hf : AnalyticWithinOn 𝕜 f s) (hs : EqOn g f s) :
     AnalyticWithinOn 𝕜 g s :=
   fun x m ↦ (hf x m).congr hs (hs m)
 
@@ -263,25 +256,6 @@ lemma AnalyticWithinOn.congr [CompleteSpace F] {f g : E → F} {s : Set E}
 ### Monotonicity w.r.t. the set we're analytic within
 -/
 
-lemma HasFPowerSeriesWithinOnBall.mono {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
-    {s t : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p t x r)
-    (hs : s ⊆ t) : HasFPowerSeriesWithinOnBall f p s x r where
-  r_le := h.r_le
-  r_pos := h.r_pos
-  hasSum {_} ys yb := h.hasSum (hs ys) yb
-  continuousWithinAt := h.continuousWithinAt.mono hs
-
-lemma HasFPowerSeriesWithinAt.mono {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
-    {s t : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p t x)
-    (hs : s ⊆ t) : HasFPowerSeriesWithinAt f p s x := by
-  rcases h with ⟨r, hr⟩
-  exact ⟨r, hr.mono hs⟩
-
-lemma AnalyticWithinAt.mono {f : E → F} {s t : Set E} {x : E} (h : AnalyticWithinAt 𝕜 f t x)
-    (hs : s ⊆ t) : AnalyticWithinAt 𝕜 f s x := by
-  rcases h with ⟨p, hp⟩
-  exact ⟨p, hp.mono hs⟩
-
 lemma AnalyticWithinOn.mono {f : E → F} {s t : Set E} (h : AnalyticWithinOn 𝕜 f t)
     (hs : s ⊆ t) : AnalyticWithinOn 𝕜 f s :=
   fun _ m ↦ (h _ (hs m)).mono hs
@@ -298,12 +272,12 @@ lemma AnalyticWithinAt.comp [CompleteSpace F] [CompleteSpace G] {f : F → G} {g
     (h : MapsTo g t s) : AnalyticWithinAt 𝕜 (f ∘ g) t x := by
   rcases hf.exists_analyticAt with ⟨f', _, ef, hf'⟩
   rcases hg.exists_analyticAt with ⟨g', gx, eg, hg'⟩
-  refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨?_, f' ∘ g', ?_, ?_⟩
-  · exact hf.continuousWithinAt.comp hg.continuousWithinAt h
-  · have gt := hg.continuousWithinAt.tendsto_nhdsWithin h
-    filter_upwards [eg, gt.eventually ef]
-    intro y gy fgy
-    simp only [Function.comp_apply, fgy, ← gy]
+  refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨f' ∘ g', ?_, ?_⟩
+  · have h' : MapsTo g (insert x t) (insert (g x) s) := h.insert x
+    have gt := hg.continuousWithinAt_insert.tendsto_nhdsWithin h'
+    filter_upwards [self_mem_nhdsWithin, gt.eventually self_mem_nhdsWithin]
+    intro y gy (fgy : g y ∈ insert (g x) s)
+    simp [Function.comp_apply, ← eg gy, ef fgy]
   · exact hf'.comp_of_eq hg' gx.symm
 
 lemma AnalyticWithinOn.comp [CompleteSpace F] [CompleteSpace G] {f : F → G} {g : E → F} {s : Set F}
@@ -318,7 +292,7 @@ lemma AnalyticWithinOn.comp [CompleteSpace F] [CompleteSpace G] {f : F → G} {g
 lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
     (h : AnalyticWithinAt 𝕜 f s x) {n : ℕ∞} : ContDiffWithinAt 𝕜 n f s x := by
   rcases h.exists_analyticAt with ⟨g, fx, fg, hg⟩
-  exact hg.contDiffAt.contDiffWithinAt.congr_of_eventuallyEq fg fx
+  exact hg.contDiffAt.contDiffWithinAt.congr (fg.mono (subset_insert _ _)) fx
 
 lemma AnalyticWithinOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
     (h : AnalyticWithinOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s :=
@@ -342,7 +316,6 @@ lemma HasFPowerSeriesWithinOnBall.prod {e : E} {f : E → F} {g : E → G} {s :
     refine (hf.hasSum m ?_).prod_mk (hg.hasSum m ?_)
     · exact EMetric.mem_ball.mpr (lt_of_lt_of_le hy (min_le_left _ _))
     · exact EMetric.mem_ball.mpr (lt_of_lt_of_le hy (min_le_right _ _))
-  continuousWithinAt := hf.continuousWithinAt.prod hg.continuousWithinAt
 
 lemma HasFPowerSeriesWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
     {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
index 56e1886f2c539..b6417f67e332f 100644
--- a/Mathlib/Data/Set/Function.lean
+++ b/Mathlib/Data/Set/Function.lean
@@ -417,6 +417,9 @@ theorem mapsTo_union : MapsTo f (s₁ ∪ s₂) t ↔ MapsTo f s₁ t ∧ MapsTo
 theorem MapsTo.inter (h₁ : MapsTo f s t₁) (h₂ : MapsTo f s t₂) : MapsTo f s (t₁ ∩ t₂) := fun _ hx =>
   ⟨h₁ hx, h₂ hx⟩
 
+lemma MapsTo.insert (h : MapsTo f s t) (x : α) : MapsTo f (insert x s) (insert (f x) t) := by
+  simpa [← singleton_union] using h.mono_right subset_union_right
+
 theorem MapsTo.inter_inter (h₁ : MapsTo f s₁ t₁) (h₂ : MapsTo f s₂ t₂) :
     MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂) := fun _ hx => ⟨h₁ hx.1, h₂ hx.2⟩
 
diff --git a/Mathlib/Geometry/Manifold/AnalyticManifold.lean b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
index 5f8e7b2f2bb61..4c999fe006c3e 100644
--- a/Mathlib/Geometry/Manifold/AnalyticManifold.lean
+++ b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
@@ -86,7 +86,7 @@ theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
   suffices h : AnalyticWithinOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by
     simp [h, analyticPregroupoid]
   have hi : AnalyticWithinOn 𝕜 id (univ : Set E) := (analyticOn_id _).analyticWithinOn
-  exact (hi.mono (subset_univ _)).congr (fun x hx ↦ (I.right_inv hx.2).symm)
+  exact (hi.mono (subset_univ _)).congr (fun x hx ↦ I.right_inv hx.2)
 
 /-- The composition of a partial homeomorphism from `H` to `M` and its inverse belongs to
 the analytic groupoid. -/