Theorem: rectangle_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 ∨ z₁.re < p.re ∧ z₂.re < p.re ∨ z₁.im < p.im ∧ z₂.im < p.im
⊢ Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
Tactic:
apply RectSubRect' <;> tauto
State after:
no goals