Theorem: mapsTo_rectangle_left_re_NoP (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ MapsTo (fun y => ↑z.re + ↑y * I) [[z.im, w.im]] (Rectangle z w \ {p})
Tactic:
refine (mapsTo_rectangleBorder_left_re z w).mono_right (Set.subset_diff.mpr ?_)
State after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Tactic:
exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
State after:
no goals