Theorem: ContinuousOn.rectangleBorderNoPIntegrable (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (Rectangle z w \ {p})
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorderIntegrable f z w
Tactic:
refine (hf.mono (Set.subset_diff.mpr ?_)).rectangleBorder_integrable
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (Rectangle z w \ {p})
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (Rectangle 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