obtain ⟨⟨h | h⟩ | h⟩ | h := hx
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
hx : x ∈ RectangleBorder z w
⊢ x ∈ Rectangle z w
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