filter_upwards [tendstoUniformlyOn_iff.mp F_conv ((2 * Real.pi * r)⁻¹ * ε) this, F_cont] with n h h'
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h : ∀ x ∈ sphere z₀ r, dist (f x) (F n x) < (2 * Real.pi * r)⁻¹ * ε
h' : ContinuousOn (F n) (sphere z₀ r)
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε