no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi : IntegrableOn (fun z => I • ↑(fderiv ℝ f z) 1 - ↑(fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
x : ℂ
hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x
simpa only [← mem_interior_iff_mem_nhds, interior_reProdIm, uIcc, interior_Icc] using hx.1