Theorem: mapsTo_rectangleBorder_left_re (PrimeNumberTheoremAnd/Rectangle.lean)

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