apply RectSubRect' <;> tauto
z w : ℂ
c : ℝ
z₀ z₁ z₂ z₃ p : ℂ
hz : z₀.re ≤ z₁.re ∧ z₁.re ≤ z₂.re ∧ z₂.re ≤ z₃.re ∧ z₀.im ≤ z₁.im ∧ z₁.im ≤ z₂.im ∧ z₂.im ≤ z₃.im
hp : p.re ≠ z₁.re ∧ p.re ≠ z₂.re ∧ p.im ≠ z₁.im ∧ p.im ≠ z₂.im
⊢ Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
no goals