Theorem: rectangleBorder_disjoint_singleton (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ Disjoint (RectangleBorder z w) {p}
Tactic:
refine disjoint_singleton_right.mpr ?_
State after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ p ∉ RectangleBorder z w

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ p ∉ RectangleBorder z w
Tactic:
simp_rw [RectangleBorder, Set.mem_union, not_or]
State after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ ((p ∉ [[z.re, w.re]] ×ℂ {z.im} ∧ p ∉ {z.re} ×ℂ [[z.im, w.im]]) ∧ p ∉ [[z.re, w.re]] ×ℂ {w.im}) ∧
    p ∉ {w.re} ×ℂ [[z.im, w.im]]

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ ((p ∉ [[z.re, w.re]] ×ℂ {z.im} ∧ p ∉ {z.re} ×ℂ [[z.im, w.im]]) ∧ p ∉ [[z.re, w.re]] ×ℂ {w.im}) ∧
    p ∉ {w.re} ×ℂ [[z.im, w.im]]
Tactic:
exact ⟨⟨⟨fun hc ↦ h.2.2.1 hc.2, fun hc ↦ h.1 hc.1⟩, fun hc ↦ h.2.2.2 hc.2⟩, fun hc ↦ h.2.1 hc.1⟩
State after:
no goals