Theorem: mapsTo_rectangle_left_im (PrimeNumberTheoremAnd/Rectangle.lean)

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

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