Theorem: mapsTo_rectangle_left_im_NoP (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ MapsTo (fun x => ↑x + ↑z.im * I) [[z.re, w.re]] (Rectangle z w \ {p})
Tactic:
refine (mapsTo_rectangleBorder_left_im 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