Theorem: rectangleBorder_subset_punctured_rect (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
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₃
Tactic:
apply RectSubRect' <;> tauto
State after:
no goals