Theorem: mapsTo_rectangleBorder_left_im (PrimeNumberTheoremAnd/Rectangle.lean)

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