case pos =>
  have f_cont : ContinuousOn f (sphere z₀ r) := F_conv.continuousOn F_cont
  rw [Metric.tendsto_nhds]
  intro ε hε
  have twopir_ne_zero : 2 * Real.pi * r ≠ 0 := by simp [Real.pi_ne_zero, hr.ne.symm]
  have : (2 * Real.pi * r)⁻¹ * ε > 0 :=
    mul_pos (inv_pos.mpr (mul_pos (mul_pos two_pos Real.pi_pos) hr)) hε.lt
  filter_upwards [tendstoUniformlyOn_iff.mp F_conv ((2 * Real.pi * r)⁻¹ * ε) this, F_cont] with n h h'
  simp_rw [dist_comm (f _) _, Complex.dist_eq, ← Complex.norm_eq_abs] at h
  rw [Complex.dist_eq, ← circleIntegral.integral_sub (h'.circleIntegrable hr.le) (f_cont.circleIntegrable hr.le),
    ← Complex.norm_eq_abs]
  have : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε := by
    have : z₀ + r ∈ sphere z₀ r := by simp [hr.le, Real.norm_eq_abs]
    exact ⟨z₀ + r, this, h _ this⟩
  convert circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr (h'.sub f_cont) (λ z hz => (h z hz).le) this
  field_simp [hr.ne, Real.pi_ne_zero, two_ne_zero]; ring
ι : 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
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
no goals