exact λ z hz => (e5 hz).2
case intro.intro.refine_2
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ ∀ z ∈ thickening δ (closedBall c r), f z ≠ 0
no goals