Theorem: rectangle_mem_nhds_iff (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
⊢ Rectangle z w ∈ 𝓝 p ↔ p ∈ uIoo z.re w.re ×ℂ uIoo z.im w.im
Tactic:
simp_rw [← mem_interior_iff_mem_nhds, Rectangle, Complex.interior_reProdIm, uIoo, uIcc, interior_Icc]
State after:
no goals