Theorem: mem_Rect (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
p : ℂ
⊢ p ∈ Rectangle z w ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im
Tactic:
rw [Rectangle, uIcc_of_le zRe_lt_wRe, uIcc_of_le zIm_lt_wIm]
State after:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
p : ℂ
⊢ p ∈ Icc z.re w.re ×ℂ Icc z.im w.im ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
p : ℂ
⊢ p ∈ Icc z.re w.re ×ℂ Icc z.im w.im ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im
Tactic:
exact and_assoc
State after:
no goals