Theorem: rectangle_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 ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im
⊢ Disjoint (Rectangle z w) {p}
Tactic:
refine disjoint_singleton_right.mpr (not_and_or.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 ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[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 ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
obtain h | h | h | h := h
State after:
case inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

case inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.im < z.im ∧ p.im < w.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

case inr.inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.re < p.re ∧ w.re < p.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

case inr.inr.inr
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

State before:
case inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inl (not_mem_uIcc_of_lt h.1 h.2)
State after:
no goals

State before:
case inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.im < z.im ∧ p.im < w.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inr (not_mem_uIcc_of_lt h.1 h.2)
State after:
no goals

State before:
case inr.inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.re < p.re ∧ w.re < p.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inl (not_mem_uIcc_of_gt h.1 h.2)
State after:
no goals

State before:
case inr.inr.inr
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inr (not_mem_uIcc_of_gt h.1 h.2)
State after:
no goals