simp [Real.pi_ne_zero, hr.ne.symm]
ι : 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
⊢ 2 * Real.pi * r ≠ 0
no goals