Theorem: not_mem_rectangleBorder_of_rectangle_mem_nhds (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
⊢ p ∉ RectangleBorder z w
Tactic:
refine Set.disjoint_right.mp (rectangleBorder_disjoint_singleton ?_) rfl
State after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
Tactic:
have h1 := rectangle_mem_nhds_iff.mp hp
State after:
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

State before:
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
Tactic:
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⟩
State after:
no goals