exact ⟨Set.ne_left_of_mem_uIoo h1.1, Set.ne_right_of_mem_uIoo h1.1,
  Set.ne_left_of_mem_uIoo h1.2, Set.ne_right_of_mem_uIoo h1.2⟩
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
h1 : p ∈ uIoo z.re w.re ×ℂ uIoo z.im w.im
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
no goals