chore(topology/algebra/ordered): golf a proof (#4311)

* generalize `continuous_within_at_Ioi_iff_Ici` from `linear_order α`
  to `partial_order α`;
* base the proof on a more general fact:
  `continuous_within_at f (s \ {x}) x ↔ continuous_within_at f s x`.

src/topology/algebra/ordered.lean

@@ -2677,25 +2677,10 @@ begin
   exact this hf hb
 end
 
-lemma continuous_within_at_Ioi_iff_Ici
-  {α β : Type*} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :
+lemma continuous_within_at_Ioi_iff_Ici {α β : Type*} [topological_space α] [partial_order α]
+  [topological_space β] {a : α} {f : α → β} :
   continuous_within_at f (Ioi a) a ↔ continuous_within_at f (Ici a) a :=
-begin
-  split,
-  { intros h s hs,
-    specialize h hs,
-    rw [mem_map, mem_nhds_within_iff_exists_mem_nhds_inter] at *,
-    rcases h with ⟨u, huna, hu⟩,
-    use [u, huna],
-    { intros x hx,
-      cases hx with hxu hx,
-      by_cases h : x = a,
-      { rw [h, mem_set_of_eq],
-        exact mem_of_nhds hs, },
-      exact hu ⟨hxu, lt_of_le_of_ne hx (ne_comm.2 h)⟩ } },
-  { intros h,
-    exact h.mono Ioi_subset_Ici_self }
-end
+by simp only [← Ici_diff_left, continuous_within_at_diff_self]
 
 lemma continuous_within_at_Iio_iff_Iic
   {α β : Type*} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :

src/topology/continuous_on.lean

@@ -269,8 +269,8 @@ lemma eventually_nhds_within_of_eventually_nhds {α : Type*} [topological_space
   ∀ᶠ x in 𝓝[s] a, p x :=
 mem_nhds_within_of_mem_nhds h
 
-/-
-nhds_within and subtypes
+/-!
+### `nhds_within` and subtypes
 -/
 
 theorem mem_nhds_within_subtype {s : set α} {a : {x // x ∈ s}} {t u : set {x // x ∈ s}} :
@@ -433,6 +433,19 @@ begin
   exact (hf x hx).mem_closure_image hx
 end
 
+lemma continuous_within_at_singleton {f : α → β} {x : α} : continuous_within_at f {x} x :=
+by simp [continuous_within_at, nhds_within, inf_eq_right.2 (pure_le_nhds x), tendsto_pure_nhds]
+
+lemma continuous_within_at.diff_iff {f : α → β} {s t : set α} {x : α}
+  (ht : continuous_within_at f t x) :
+  continuous_within_at f (s \ t) x ↔ continuous_within_at f s x :=
+⟨λ h, (h.union ht).mono $ by simp only [diff_union_self, subset_union_left],
+  λ h, h.mono (diff_subset _ _)⟩
+
+@[simp] lemma continuous_within_at_diff_self {f : α → β} {s : set α} {x : α} :
+  continuous_within_at f (s \ {x}) x ↔ continuous_within_at f s x :=
+continuous_within_at_singleton.diff_iff
+
 theorem is_open_map.continuous_on_image_of_left_inv_on {f : α → β} {s : set α}
   (h : is_open_map (s.restrict f)) {finv : β → α} (hleft : left_inv_on finv f s) :
   continuous_on finv (f '' s) :=