filter_upwards [Ioo_mem_nhdsWithin_Ioi' (hε0)] with _ ⟨hε'0, hε'⟩
case intro.intro
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w
case h
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
a✝ : ℝ
hε'0 : 0 < a✝
hε' : a✝ < ε
⊢ Square p a✝ ⊆ Rectangle z w