Theorem: rectangleBorder_subset_rectangle (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ RectangleBorder z w ⊆ Rectangle z w
Tactic:
intro x hx
State after:
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
hx : x ∈ RectangleBorder z w
⊢ x ∈ Rectangle z w

State before:
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
hx : x ∈ RectangleBorder z w
⊢ x ∈ Rectangle z w
Tactic:
obtain ⟨⟨h | h⟩ | h⟩ | h := hx
State after:
case inl.inl.inl
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {z.im}
⊢ x ∈ Rectangle z w

case inl.inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {z.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w

case inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {w.im}
⊢ x ∈ Rectangle z w

case inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {w.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w

State before:
case inl.inl.inl
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {z.im}
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1, h.2 ▸ left_mem_uIcc⟩
State after:
no goals

State before:
case inl.inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {z.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1 ▸ left_mem_uIcc, h.2⟩
State after:
no goals

State before:
case inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {w.im}
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1, h.2 ▸ right_mem_uIcc⟩
State after:
no goals

State before:
case inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {w.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1 ▸ right_mem_uIcc, h.2⟩
State after:
no goals