∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ},
  s ∈ nhds c →
    DifferentiableOn ℂ f (s \ {c}) →
      ((fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) →
        DifferentiableOn ℂ (Function.update f c (limUnder (nhdsWithin c {c}ᶜ) f)) s