-- Mathlib/Analysis/Analytic/Basic.lean
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
      ((x + ·)⁻¹' (insert x s) ∩ Metric.ball (0 : E) r')

Proof state:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
⊢ TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
    ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')

Tactic:
refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Result:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 => x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε

Proof state:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)
n : ℕ
hn : C * a ^ n < ε
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r'
⊢ dist (f (x + y)) (p.partialSum n y) < ε

Tactic:
rw [dist_eq_norm]

Result:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)
n : ℕ
hn : C * a ^ n < ε
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r'
⊢ ‖f (x + y) - p.partialSum n 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
    ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')

Tactic:
obtain ⟨a, ha, C, -, hp⟩ : ∃ 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 ^ n := hf.uniform_geometric_approx h

Result:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
⊢ TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
    ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')

Proof state:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 (C * 0))
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 => x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε

Tactic:
rw [mul_zero] at L

Result:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 => x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε

Proof state:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 => x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε

Tactic:
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)

Result:
case intro.intro.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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 (C * 0))
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 => x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε