Theorem: Square_apply (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Square p c = Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)
Tactic:
rw [Square, Rectangle, uIcc_of_le (by simp; linarith), uIcc_of_le (by simp; linarith)]
State after:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Icc (-↑c - ↑c * I + p).re (↑c + ↑c * I + p).re ×ℂ Icc (-↑c - ↑c * I + p).im (↑c + ↑c * I + p).im =
    Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)

State before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Icc (-↑c - ↑c * I + p).re (↑c + ↑c * I + p).re ×ℂ Icc (-↑c - ↑c * I + p).im (↑c + ↑c * I + p).im =
    Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)
Tactic:
simp
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re
Tactic:
simp
State after:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ 0 ≤ c

State before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ 0 ≤ c
Tactic:
linarith
State after:
no goals

State before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im
Tactic:
simp
State after:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ 0 ≤ c