∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E}
  {s : Set ℂ},
  s.Countable →
    w ∈ Metric.ball c R →
      ContinuousOn f (Metric.closedBall c R) →
        (∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
          (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w