feat(analysis/calculus/times_cont_diff): differentiability of field i…

…nverse (#4795)

src/algebra/field.lean

@@ -33,6 +33,14 @@ instance division_ring.to_group_with_zero :
 { .. ‹division_ring α›,
   .. (infer_instance : semiring α) }
 
+lemma inverse_eq_has_inv : (ring.inverse : α → α) = has_inv.inv :=
+begin
+  ext x,
+  by_cases hx : x = 0,
+  { simp [hx] },
+  { exact ring.inverse_unit (units.mk0 x hx) }
+end
+
 @[field_simps] lemma inv_eq_one_div (a : α) : a⁻¹ = 1 / a := by simp
 
 local attribute [simp]

src/analysis/calculus/times_cont_diff.lean

@@ -468,46 +468,25 @@ begin
     exact ⟨u, hu, p, hp⟩ }
 end
 
-lemma times_cont_diff_within_at.continuous_within_at' {n : with_top ℕ}
-  (h : times_cont_diff_within_at 𝕜 n f s x) : continuous_within_at f (insert x s) x :=
+lemma times_cont_diff_within_at.continuous_within_at {n : with_top ℕ}
+  (h : times_cont_diff_within_at 𝕜 n f s x) : continuous_within_at f s x :=
 begin
   rcases h 0 bot_le with ⟨u, hu, p, H⟩,
-  rcases mem_nhds_within.1 hu with ⟨t, t_open, xt, tu⟩,
-  have A : x ∈ t ∩ insert x s, by simp [xt],
-  have := (H.mono tu).continuous_on.continuous_within_at A,
-  rw inter_comm at this,
-  exact (continuous_within_at_inter (mem_nhds_sets t_open xt)).1 this
+  rw [mem_nhds_within_insert] at hu,
+  exact (H.continuous_on.continuous_within_at hu.1).mono_of_mem hu.2
 end
 
-lemma times_cont_diff_within_at.continuous_within_at {n : with_top ℕ}
-  (h : times_cont_diff_within_at 𝕜 n f s x) : continuous_within_at f s x :=
-(h.continuous_within_at').mono (subset_insert x s)
-
 lemma times_cont_diff_within_at.congr_of_eventually_eq {n : with_top ℕ}
   (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
   times_cont_diff_within_at 𝕜 n f₁ s x :=
-begin
-  assume m hm,
-  rcases h m hm with ⟨u, hu, p, H⟩,
-  rcases h₁.exists_mem with ⟨v, v_neighb, hv⟩,
-  refine ⟨u ∩ ((insert x v) ∩ (insert x s)), _, p, _⟩,
-  { exact filter.inter_mem_sets hu (filter.inter_mem_sets (mem_nhds_within_insert v_neighb)
-      self_mem_nhds_within) },
-  { apply (H.mono (inter_subset_left u _)).congr (λ y hy, _),
-    simp at hy,
-    rcases hy.2.1 with rfl|hy',
-    { exact hx },
-    { exact hv hy' } }
-end
+λ m hm, let ⟨u, hu, p, H⟩ := h m hm in
+⟨{x ∈ u | f₁ x = f x}, filter.inter_mem_sets hu (mem_nhds_within_insert.2 ⟨hx, h₁⟩), p,
+  (H.mono (sep_subset _ _)).congr (λ _, and.right)⟩
 
 lemma times_cont_diff_within_at.congr_of_eventually_eq' {n : with_top ℕ}
   (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
   times_cont_diff_within_at 𝕜 n f₁ s x :=
-begin
-  apply h.congr_of_eventually_eq h₁,
-  rcases h₁.exists_mem with ⟨t, ht, t_eq⟩,
-  exact t_eq (mem_of_mem_nhds_within hx ht)
-end
+h.congr_of_eventually_eq h₁ $ h₁.self_of_nhds_within hx
 
 lemma filter.eventually_eq.times_cont_diff_within_at_iff {n : with_top ℕ}
   (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
@@ -520,30 +499,37 @@ lemma times_cont_diff_within_at.congr {n : with_top ℕ}
   times_cont_diff_within_at 𝕜 n f₁ s x :=
 h.congr_of_eventually_eq (filter.eventually_eq_of_mem self_mem_nhds_within h₁) hx
 
-lemma times_cont_diff_within_at.mono {n : with_top ℕ}
-  (h : times_cont_diff_within_at 𝕜 n f s x) {t : set E} (hst : t ⊆ s) :
+lemma times_cont_diff_within_at.mono_of_mem {n : with_top ℕ}
+  (h : times_cont_diff_within_at 𝕜 n f s x) {t : set E} (hst : s ∈ 𝓝[t] x) :
   times_cont_diff_within_at 𝕜 n f t x :=
 begin
   assume m hm,
   rcases h m hm with ⟨u, hu, p, H⟩,
-  exact ⟨u, nhds_within_mono _ (insert_subset_insert hst) hu, p, H⟩,
+  exact ⟨u, nhds_within_le_of_mem (insert_mem_nhds_within_insert hst) hu, p, H⟩
 end
 
+lemma times_cont_diff_within_at.mono {n : with_top ℕ}
+  (h : times_cont_diff_within_at 𝕜 n f s x) {t : set E} (hst : t ⊆ s) :
+  times_cont_diff_within_at 𝕜 n f t x :=
+h.mono_of_mem $ filter.mem_sets_of_superset self_mem_nhds_within hst
+
+lemma times_cont_diff_within_at.congr_nhds {n : with_top ℕ}
+  (h : times_cont_diff_within_at 𝕜 n f s x) {t : set E} (hst : 𝓝[s] x = 𝓝[t] x) :
+  times_cont_diff_within_at 𝕜 n f t x :=
+h.mono_of_mem $ hst ▸ self_mem_nhds_within
+
+lemma times_cont_diff_within_at_congr_nhds {n : with_top ℕ} {t : set E} (hst : 𝓝[s] x = 𝓝[t] x) :
+  times_cont_diff_within_at 𝕜 n f s x ↔ times_cont_diff_within_at 𝕜 n f t x :=
+⟨λ h, h.congr_nhds hst, λ h, h.congr_nhds hst.symm⟩
+
 lemma times_cont_diff_within_at.of_le {m n : with_top ℕ}
   (h : times_cont_diff_within_at 𝕜 n f s x) (hmn : m ≤ n) :
   times_cont_diff_within_at 𝕜 m f s x :=
 λ k hk, h k (le_trans hk hmn)
 
 lemma times_cont_diff_within_at_inter' {n : with_top ℕ} (h : t ∈ 𝓝[s] x) :
   times_cont_diff_within_at 𝕜 n f (s ∩ t) x ↔ times_cont_diff_within_at 𝕜 n f s x :=
-begin
-  refine ⟨λ H m hm, _, λ H, H.mono (inter_subset_left _ _)⟩,
-  rcases H m hm with ⟨u, u_nhbd, p, hu⟩,
-  refine ⟨(insert x s ∩ insert x t) ∩ u, _, p, hu.mono (inter_subset_right _ _)⟩,
-  rw nhds_within_restrict'' (insert x s) (mem_nhds_within_insert h),
-  rw insert_inter at u_nhbd,
-  exact filter.inter_mem_sets self_mem_nhds_within u_nhbd
-end
+times_cont_diff_within_at_congr_nhds $ eq.symm $ nhds_within_restrict'' _ h
 
 lemma times_cont_diff_within_at_inter {n : with_top ℕ} (h : t ∈ 𝓝 x) :
   times_cont_diff_within_at 𝕜 n f (s ∩ t) x ↔ times_cont_diff_within_at 𝕜 n f s x :=
@@ -639,7 +625,8 @@ lemma times_cont_diff_within_at.times_cont_diff_on {n : with_top ℕ} {m : ℕ}
   ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ times_cont_diff_on 𝕜 m f u :=
 begin
   rcases h m hm with ⟨u, u_nhd, p, hp⟩,
-  refine ⟨u ∩ insert x s, filter.inter_mem_sets u_nhd self_mem_nhds_within, inter_subset_right _ _, _⟩,
+  refine ⟨u ∩ insert x s, filter.inter_mem_sets u_nhd self_mem_nhds_within,
+    inter_subset_right _ _, _⟩,
   assume y hy m' hm',
   refine ⟨u ∩ insert x s, _, p, (hp.mono (inter_subset_left _ _)).of_le hm'⟩,
   convert self_mem_nhds_within,
@@ -1243,6 +1230,11 @@ lemma times_cont_diff_within_at.times_cont_diff_at {n : with_top ℕ}
   times_cont_diff_at 𝕜 n f x :=
 by rwa [times_cont_diff_at, ← times_cont_diff_within_at_inter hx, univ_inter]
 
+lemma times_cont_diff_at.congr_of_eventually_eq {n : with_top ℕ}
+  (h : times_cont_diff_at 𝕜 n f x) (hg : f₁ =ᶠ[𝓝 x] f) :
+  times_cont_diff_at 𝕜 n f₁ x :=
+h.congr_of_eventually_eq' (by rwa nhds_within_univ) (mem_univ x)
+
 lemma times_cont_diff_at.of_le {m n : with_top ℕ}
   (h : times_cont_diff_at 𝕜 n f x) (hmn : m ≤ n) :
   times_cont_diff_at 𝕜 m f x :=
@@ -1628,6 +1620,18 @@ The identity is `C^∞`.
 lemma times_cont_diff_id {n : with_top ℕ} : times_cont_diff 𝕜 n (id : E → E) :=
 is_bounded_linear_map.id.times_cont_diff
 
+lemma times_cont_diff_within_at_id {n : with_top ℕ} {s x} :
+  times_cont_diff_within_at 𝕜 n (id : E → E) s x :=
+times_cont_diff_id.times_cont_diff_within_at
+
+lemma times_cont_diff_at_id {n : with_top ℕ} {x} :
+  times_cont_diff_at 𝕜 n (id : E → E) x :=
+times_cont_diff_id.times_cont_diff_at
+
+lemma times_cont_diff_on_id {n : with_top ℕ} {s} :
+  times_cont_diff_on 𝕜 n (id : E → E) s :=
+times_cont_diff_id.times_cont_diff_on
+
 /--
 Bilinear functions are `C^∞`.
 -/
@@ -2018,7 +2022,7 @@ begin
     ⟨(mem_of_mem_nhds_within (mem_insert (f x) _) u_nhd : _),
     mem_of_mem_nhds_within (mem_insert x s) v_nhd⟩,
   have : f ⁻¹' u ∈ 𝓝[insert x s] x,
-  { apply hf.continuous_within_at'.preimage_mem_nhds_within',
+  { apply hf.continuous_within_at.insert_self.preimage_mem_nhds_within',
     apply nhds_within_mono _ _ u_nhd,
     rw image_insert_eq,
     exact insert_subset_insert (image_subset_iff.mpr st) },
@@ -2041,9 +2045,13 @@ lemma times_cont_diff_within_at.comp' {n : with_top ℕ} {s : set E} {t : set F}
   times_cont_diff_within_at 𝕜 n (g ∘ f) (s ∩ f⁻¹' t) x :=
 hg.comp x (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
 
+lemma times_cont_diff_at.comp_times_cont_diff_within_at {n} (x : E)
+  (hg : times_cont_diff_at 𝕜 n g (f x)) (hf : times_cont_diff_within_at 𝕜 n f s x) :
+  times_cont_diff_within_at 𝕜 n (g ∘ f) s x :=
+hg.comp x hf (maps_to_univ _ _)
+
 /-- The composition of `C^n` functions at points is `C^n`. -/
-lemma times_cont_diff_at.comp
-  {n : with_top ℕ} {g : F → G} {f : E → F} (x : E)
+lemma times_cont_diff_at.comp {n : with_top ℕ} (x : E)
   (hg : times_cont_diff_at 𝕜 n g (f x))
   (hf : times_cont_diff_at 𝕜 n f x) :
   times_cont_diff_at 𝕜 n (g ∘ f) x :=
@@ -2242,6 +2250,12 @@ lemma times_cont_diff.mul {n : with_top ℕ} {f g : E → 𝕜}
   times_cont_diff 𝕜 n (λ x, f x * g x) :=
 times_cont_diff_mul.comp (hf.prod hg)
 
+lemma times_cont_diff.pow {n : with_top ℕ} {f : E → 𝕜}
+  (hf : times_cont_diff 𝕜 n f) :
+  ∀ m : ℕ, times_cont_diff 𝕜 n (λ x, (f x) ^ m)
+| 0 := by simpa using times_cont_diff_const
+| (m + 1) := hf.mul (times_cont_diff.pow m)
+
 /-- The product of two `C^n` functions on a domain is `C^n`. -/
 lemma times_cont_diff_on.mul {n : with_top ℕ} {s : set E} {f g : E → 𝕜}
   (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) :
@@ -2347,7 +2361,7 @@ end prod_map
 /-! ### Inversion in a complete normed algebra -/
 
 section algebra_inverse
-variables (𝕜) (R : Type*) [normed_ring R] [normed_algebra 𝕜 R]
+variables (𝕜) {R : Type*} [normed_ring R] [normed_algebra 𝕜 R]
 open normed_ring continuous_linear_map ring
 
 /-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
@@ -2380,6 +2394,49 @@ begin
   { exact times_cont_diff_at_top.mpr Itop }
 end
 
+variables (𝕜) {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜']
+
+lemma times_cont_diff_at_inv {x : 𝕜'} (hx : x ≠ 0) {n} :
+  times_cont_diff_at 𝕜 n has_inv.inv x :=
+by simpa only [inverse_eq_has_inv] using times_cont_diff_at_ring_inverse 𝕜 (units.mk0 x hx)
+
+variable {𝕜}
+
+-- TODO: the next few lemmas don't need `𝕜` or `𝕜'` to be complete
+-- A good way to show this is to generalize `times_cont_diff_at_ring_inverse` to the setting
+-- of a function `f` such that `∀ᶠ x in 𝓝 a, x * f x = 1`.
+
+lemma times_cont_diff_within_at.inv {f : E → 𝕜'} {n} (hf : times_cont_diff_within_at 𝕜 n f s x)
+  (hx : f x ≠ 0) :
+  times_cont_diff_within_at 𝕜 n (λ x, (f x)⁻¹) s x :=
+(times_cont_diff_at_inv 𝕜 hx).comp_times_cont_diff_within_at x hf
+
+lemma times_cont_diff_at.inv {f : E → 𝕜'} {n} (hf : times_cont_diff_at 𝕜 n f x) (hx : f x ≠ 0) :
+  times_cont_diff_at 𝕜 n (λ x, (f x)⁻¹) x :=
+hf.inv hx
+
+-- TODO: generalize to `f g : E → 𝕜'`
+lemma times_cont_diff_within_at.div [complete_space 𝕜] {f g : E → 𝕜} {n}
+  (hf : times_cont_diff_within_at 𝕜 n f s x) (hg : times_cont_diff_within_at 𝕜 n g s x)
+  (hx : g x ≠ 0) :
+  times_cont_diff_within_at 𝕜 n (λ x, f x / g x) s x :=
+hf.mul (hg.inv hx)
+
+lemma times_cont_diff_at.div [complete_space 𝕜] {f g : E → 𝕜} {n}
+  (hf : times_cont_diff_at 𝕜 n f x) (hg : times_cont_diff_at 𝕜 n g x)
+  (hx : g x ≠ 0) :
+  times_cont_diff_at 𝕜 n (λ x, f x / g x) x :=
+hf.div hg hx
+
+lemma times_cont_diff.div [complete_space 𝕜] {f g : E → 𝕜} {n}
+  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g)
+  (h0 : ∀ x, g x ≠ 0) :
+  times_cont_diff 𝕜 n (λ x, f x / g x) :=
+begin
+  simp only [times_cont_diff_iff_times_cont_diff_at] at *,
+  exact λ x, (hf x).div (hg x) (h0 x)
+end
+
 end algebra_inverse
 
 /-! ### Inversion of continuous linear maps between Banach spaces -/
@@ -2402,13 +2459,14 @@ begin
   rw this,
   -- `O₁` and `O₂` are `times_cont_diff`, so we reduce to proving that `ring.inverse` is `times_cont_diff`
   have h₁ : times_cont_diff 𝕜 n O₁,
-  { exact is_bounded_bilinear_map_comp.times_cont_diff.comp (times_cont_diff_const.prod times_cont_diff_id) },
+    from is_bounded_bilinear_map_comp.times_cont_diff.comp
+      (times_cont_diff_const.prod times_cont_diff_id),
   have h₂ : times_cont_diff 𝕜 n O₂,
-  { exact is_bounded_bilinear_map_comp.times_cont_diff.comp (times_cont_diff_id.prod times_cont_diff_const) },
+    from is_bounded_bilinear_map_comp.times_cont_diff.comp
+      (times_cont_diff_id.prod times_cont_diff_const),
   refine h₁.times_cont_diff_at.comp _ (times_cont_diff_at.comp _ _ h₂.times_cont_diff_at),
-  convert times_cont_diff_at_ring_inverse 𝕜 (E →L[𝕜] E) 1,
-  simp [O₂],
-  refl
+  convert times_cont_diff_at_ring_inverse 𝕜 (1 : units (E →L[𝕜] E)),
+  simp [O₂, one_def]
 end
 
 end map_inverse

src/geometry/manifold/times_cont_mdiff.lean

@@ -689,13 +689,14 @@ lemma times_cont_mdiff_within_at.comp {t : set M'} {g : M' → M''} (x : M)
   (st : s ⊆ f ⁻¹' t) : times_cont_mdiff_within_at I I'' n (g ∘ f) s x :=
 begin
   apply times_cont_mdiff_within_at_iff_nat.2 (λ m hm, _),
-  rcases times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.1 (hg.of_le hm) with ⟨v, v_nhds, hv⟩,
-  rcases times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.1 (hf.of_le hm) with ⟨u, u_nhds, hu⟩,
+  rcases times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.1 (hg.of_le hm)
+    with ⟨v, v_nhds, hv⟩,
+  rcases times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.1 (hf.of_le hm)
+    with ⟨u, u_nhds, hu⟩,
   apply times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.2 ⟨_, _, hv.comp' hu⟩,
   apply filter.inter_mem_sets u_nhds,
   suffices h : v ∈ 𝓝[f '' s] (f x),
-  { convert mem_nhds_within_insert (hf.continuous_within_at.preimage_mem_nhds_within' h),
-    rw insert_eq_of_mem,
+  { refine mem_nhds_within_insert.2 ⟨_, hf.continuous_within_at.preimage_mem_nhds_within' h⟩,
     apply mem_of_mem_nhds_within (mem_insert (f x) t) v_nhds },
   apply nhds_within_mono _ _ v_nhds,
   rw image_subset_iff,

src/topology/algebra/module.lean

@@ -283,6 +283,7 @@ end
 
 instance : has_one (M →L[R] M) := ⟨id R M⟩
 
+lemma one_def : (1 : M →L[R] M) = id R M := rfl
 lemma id_apply : id R M x = x := rfl
 @[simp, norm_cast] lemma coe_id : (id R M : M →ₗ[R] M) = linear_map.id := rfl
 @[simp, norm_cast] lemma coe_id' : (id R M : M → M) = _root_.id := rfl

src/topology/continuous_on.lean

@@ -169,17 +169,20 @@ theorem nhds_within_inter' (a : α) (s t : set α) :
   𝓝[s ∩ t] a = (𝓝[s] a) ⊓ 𝓟 t :=
 by { delta nhds_within, rw [←inf_principal, inf_assoc] }
 
-lemma mem_nhds_within_insert {a : α} {s t : set α} (h : t ∈ 𝓝[s] a) :
+@[simp] theorem nhds_within_singleton (a : α) : 𝓝[{a}] a = pure a :=
+by rw [nhds_within, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
+
+@[simp] theorem nhds_within_insert (a : α) (s : set α) :
+  𝓝[insert a s] a = pure a ⊔ 𝓝[s] a :=
+by rw [← singleton_union, nhds_within_union, nhds_within_singleton]
+
+lemma mem_nhds_within_insert {a : α} {s t : set α} :
+  t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a :=
+by simp
+
+lemma insert_mem_nhds_within_insert {a : α} {s t : set α} (h : t ∈ 𝓝[s] a) :
   insert a t ∈ 𝓝[insert a s] a :=
-begin
-  rcases mem_nhds_within.1 h with ⟨o, o_open, ao, ho⟩,
-  apply mem_nhds_within.2 ⟨o, o_open, ao, _⟩,
-  assume y,
-  simp only [and_imp, mem_inter_eq, mem_insert_iff],
-  rintro yo (rfl | ys),
-  { simp },
-  { simp [ho ⟨yo, ys⟩] }
-end
+by simp [mem_sets_of_superset h]
 
 lemma nhds_within_prod_eq {α : Type*} [topological_space α] {β : Type*} [topological_space β]
   (a : α) (b : β) (s : set α) (t : set β) :
@@ -406,6 +409,10 @@ lemma continuous_within_at.mono {f : α → β} {s t : set α} {x : α} (h : con
   (hs : s ⊆ t) : continuous_within_at f s x :=
 h.mono_left (nhds_within_mono x hs)
 
+lemma continuous_within_at.mono_of_mem {f : α → β} {s t : set α} {x : α}
+  (h : continuous_within_at f t x) (hs : t ∈ 𝓝[s] x) : continuous_within_at f s x :=
+h.mono_left (nhds_within_le_of_mem hs)
+
 lemma continuous_within_at_inter' {f : α → β} {s t : set α} {x : α} (h : t ∈ 𝓝[s] x) :
   continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x :=
 by simp [continuous_within_at, nhds_within_restrict'' s h]
@@ -414,10 +421,14 @@ lemma continuous_within_at_inter {f : α → β} {s t : set α} {x : α} (h : t
   continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x :=
 by simp [continuous_within_at, nhds_within_restrict' s h]
 
+lemma continuous_within_at_union {f : α → β} {s t : set α} {x : α} :
+  continuous_within_at f (s ∪ t) x ↔ continuous_within_at f s x ∧ continuous_within_at f t x :=
+by simp only [continuous_within_at, nhds_within_union, tendsto_sup]
+
 lemma continuous_within_at.union {f : α → β} {s t : set α} {x : α}
   (hs : continuous_within_at f s x) (ht : continuous_within_at f t x) :
   continuous_within_at f (s ∪ t) x :=
-by simp only [continuous_within_at, nhds_within_union, tendsto, map_sup, sup_le_iff.2 ⟨hs, ht⟩]
+continuous_within_at_union.2 ⟨hs, ht⟩
 
 lemma continuous_within_at.mem_closure_image  {f : α → β} {s : set α} {x : α}
   (h : continuous_within_at f s x) (hx : x ∈ closure s) : f x ∈ closure (f '' s) :=
@@ -437,8 +448,15 @@ 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]
+@[simp] lemma continuous_within_at_singleton {f : α → β} {x : α} : continuous_within_at f {x} x :=
+by simp only [continuous_within_at, nhds_within_singleton, tendsto_pure_nhds]
+
+@[simp] lemma continuous_within_at_insert_self {f : α → β} {x : α} {s : set α} :
+  continuous_within_at f (insert x s) x ↔ continuous_within_at f s x :=
+by simp only [← singleton_union, continuous_within_at_union, continuous_within_at_singleton,
+  true_and]
+
+alias continuous_within_at_insert_self ↔ _ continuous_within_at.insert_self
 
 lemma continuous_within_at.diff_iff {f : α → β} {s t : set α} {x : α}
   (ht : continuous_within_at f t x) :