intro ⟨⟨⟨hz're_ge, hz're_le⟩, ⟨hz'im_ge, hz'im_le⟩⟩,
  ⟨⟨hw're_ge, hw're_le⟩, ⟨hw'im_ge, hw'im_le⟩⟩⟩ x ⟨⟨hxre_ge, hxre_le⟩, ⟨hxim_ge, hxim_le⟩⟩
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w → Rectangle z' w' ⊆ Rectangle z w
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x ∈ Rectangle z w