-- Mathlib/Analysis/Analytic/Basic.lean
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)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
⊢ ∃ t ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x + y)) y, (fun n y => p.partialSum n y) n y) ∈ u

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hy.2 with ⟨r', yr', hr'⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
⊢ ∃ t ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x + y)) y, (fun n y => p.partialSum n y) n y) ∈ u

Proof state:
case intro.intro.refine_1.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ EMetric.ball 0 r ∈ 𝓝 y

Tactic:
apply Filter.mem_of_superset this (EMetric.ball_subset_ball hr'.le)

Result:
no goals

Proof state:
case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 ↑r' ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s] y

Tactic:
exact inter_mem_nhdsWithin _ this

Result:
no goals

Proof state:
case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 ↑r' ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r] y

Tactic:
rw [nhdsWithin_inter_of_mem']

Result:
case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 ↑r' ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s] y

case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ EMetric.ball 0 r ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s] y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
    ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r)

Tactic:
intro u hu y hy

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
⊢ ∃ t ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x + y)) y, (fun n y => p.partialSum n y) n y) ∈ u

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
⊢ ∃ t ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x + y)) y, (fun n y => p.partialSum n y) n y) ∈ u

Tactic:
have : EMetric.ball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds EMetric.isOpen_ball yr'

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ ∃ t ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x + y)) y, (fun n y => p.partialSum n y) n y) ∈ u