Theorem: existsDifferentiableOn_of_bddAbove (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w p c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : HolomorphicOn f (s \ {c})
hb : BddAbove (Norm.norm ∘ f '' (s \ {c}))
z : ℂ
hz : z ∈ s \ {c}
h : ¬z = c
⊢ f z = Function.update f c (limUnder (𝓝[≠] c) f) z
Tactic:
simp [h]
State after:
no goals