Theorem: mapsTo_rectangle_left_re (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.im, w.im]]
⊢ (fun y => ↑z.re + ↑y * I) x✝ ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simp
State after:
no goals

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.im, w.im]]
⊢ (fun y => ↑z.re + ↑y * I) x✝ ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simp [hx]
State after:
no goals