refactor(*): add a notation for nhds_within (#3683)

The definition is still there and can be used too.

src/analysis/ODE/gronwall.lean

@@ -32,7 +32,7 @@ variables {E : Type*} [normed_group E] [normed_space ℝ E]
           {F : Type*} [normed_group F] [normed_space ℝ F]
 
 open metric set asymptotics filter real
-open_locale classical
+open_locale classical topological_space
 
 /-! ### Technical lemmas about `gronwall_bound` -/
 
@@ -107,7 +107,7 @@ See also `norm_le_gronwall_bound_of_norm_deriv_right_le` for a version bounding
 theorem le_gronwall_bound_of_liminf_deriv_right_le {f f' : ℝ → ℝ} {δ K ε : ℝ} {a b : ℝ}
   (hf : continuous_on f (Icc a b))
   (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
-    ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r)
+    ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r)
   (ha : f a ≤ δ) (bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε) :
   ∀ x ∈ Icc a b, f x ≤ gronwall_bound δ K ε (x - a) :=
 begin

src/analysis/calculus/deriv.lean

@@ -107,7 +107,7 @@ has_fderiv_at_filter f (smul_right 1 f' : 𝕜 →L[𝕜] F) x L
 That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x` inside `s`.
 -/
 def has_deriv_within_at (f : 𝕜 → F) (f' : F) (s : set 𝕜) (x : 𝕜) :=
-has_deriv_at_filter f f' x (nhds_within x s)
+has_deriv_at_filter f f' x (𝓝[s] x)
 
 /--
 `f` has the derivative `f'` at the point `x`.
@@ -215,7 +215,7 @@ theorem has_deriv_at_filter_iff_tendsto :
 has_fderiv_at_filter_iff_tendsto
 
 theorem has_deriv_within_at_iff_tendsto : has_deriv_within_at f f' s x ↔
-  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (nhds_within x s) (𝓝 0) :=
+  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝[s] x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
 theorem has_deriv_at_iff_tendsto : has_deriv_at f f' x ↔
@@ -244,23 +244,23 @@ end
 
 lemma has_deriv_within_at_iff_tendsto_slope {x : 𝕜} {s : set 𝕜} :
   has_deriv_within_at f f' s x ↔
-    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (s \ {x})) (𝓝 f') :=
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[s \ {x}] x) (𝓝 f') :=
 begin
   simp only [has_deriv_within_at, nhds_within, diff_eq, inf_assoc.symm, inf_principal.symm],
   exact has_deriv_at_filter_iff_tendsto_slope
 end
 
 lemma has_deriv_within_at_iff_tendsto_slope' {x : 𝕜} {s : set 𝕜} (hs : x ∉ s) :
   has_deriv_within_at f f' s x ↔
-    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x s) (𝓝 f') :=
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[s] x) (𝓝 f') :=
 begin
   convert ← has_deriv_within_at_iff_tendsto_slope,
   exact diff_singleton_eq_self hs
 end
 
 lemma has_deriv_at_iff_tendsto_slope {x : 𝕜} :
   has_deriv_at f f' x ↔
-    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x {x}ᶜ) (𝓝 f') :=
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[{x}ᶜ] x) (𝓝 f') :=
 has_deriv_at_filter_iff_tendsto_slope
 
 theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔
@@ -297,7 +297,7 @@ theorem has_deriv_at_unique
   (h₀ : has_deriv_at f f₀' x) (h₁ : has_deriv_at f f₁' x) : f₀' = f₁' :=
 smul_right_one_eq_iff.mp $ has_fderiv_at_unique h₀ h₁
 
-lemma has_deriv_within_at_inter' (h : t ∈ nhds_within x s) :
+lemma has_deriv_within_at_inter' (h : t ∈ 𝓝[s] x) :
   has_deriv_within_at f f' (s ∩ t) x ↔ has_deriv_within_at f f' s x :=
 has_fderiv_within_at_inter' h
 
@@ -313,7 +313,7 @@ begin
 end
 
 lemma has_deriv_within_at.nhds_within (h : has_deriv_within_at f f' s x)
-  (ht : s ∈ nhds_within x t) : has_deriv_within_at f f' t x :=
+  (ht : s ∈ 𝓝[t] x) : has_deriv_within_at f f' t x :=
 (has_deriv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _))
 
 lemma has_deriv_within_at.has_deriv_at (h : has_deriv_within_at f f' s x) (hs : s ∈ 𝓝 x) :
@@ -386,15 +386,15 @@ lemma has_deriv_within_at.congr (h : has_deriv_within_at f f' s x) (hs : ∀x 
 h.congr_mono hs hx (subset.refl _)
 
 lemma has_deriv_within_at.congr_of_eventually_eq (h : has_deriv_within_at f f' s x)
-  (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : has_deriv_within_at f₁ f' s x :=
+  (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : has_deriv_within_at f₁ f' s x :=
 has_deriv_at_filter.congr_of_eventually_eq h h₁ hx
 
 lemma has_deriv_at.congr_of_eventually_eq (h : has_deriv_at f f' x)
   (h₁ : f₁ =ᶠ[𝓝 x] f) : has_deriv_at f₁ f' x :=
 has_deriv_at_filter.congr_of_eventually_eq h h₁ (mem_of_nhds h₁ : _)
 
 lemma filter.eventually_eq.deriv_within_eq (hs : unique_diff_within_at 𝕜 s x)
-  (hL : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
+  (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
   deriv_within f₁ s x = deriv_within f s x :=
 by { unfold deriv_within, rw hL.fderiv_within_eq hs hx }
 
@@ -941,9 +941,8 @@ theorem has_deriv_within_at.scomp {t : set 𝕜}
   has_deriv_within_at (g ∘ h) (h' • g') s x :=
 begin
   apply has_deriv_at_filter.scomp _ (has_deriv_at_filter.mono hg _) hh,
-  calc map h (nhds_within x s)
-      ≤ nhds_within (h x) (h '' s) : hh.continuous_within_at.tendsto_nhds_within_image
-  ... ≤ nhds_within (h x) t        : nhds_within_mono _ (image_subset_iff.mpr hst)
+  calc map h (𝓝[s] x) ≤ 𝓝[h '' s] (h x) : hh.continuous_within_at.tendsto_nhds_within_image
+                  ... ≤ 𝓝[t] (h x)      : nhds_within_mono _ (image_subset_iff.mpr hst)
 end
 
 /-- The chain rule. -/
@@ -1685,17 +1684,17 @@ section real
 variables {f : ℝ → ℝ} {f' : ℝ} {s : set ℝ} {x : ℝ} {r : ℝ}
 
 lemma has_deriv_within_at.limsup_slope_le (hf : has_deriv_within_at f f' s x) (hr : f' < r) :
-  ∀ᶠ z in nhds_within x (s \ {x}), (z - x)⁻¹ * (f z - f x) < r :=
+  ∀ᶠ z in 𝓝[s \ {x}] x, (z - x)⁻¹ * (f z - f x) < r :=
 has_deriv_within_at_iff_tendsto_slope.1 hf (mem_nhds_sets is_open_Iio hr)
 
 lemma has_deriv_within_at.limsup_slope_le' (hf : has_deriv_within_at f f' s x)
   (hs : x ∉ s) (hr : f' < r) :
-  ∀ᶠ z in nhds_within x s, (z - x)⁻¹ * (f z - f x) < r :=
+  ∀ᶠ z in 𝓝[s] x, (z - x)⁻¹ * (f z - f x) < r :=
 (has_deriv_within_at_iff_tendsto_slope' hs).1 hf (mem_nhds_sets is_open_Iio hr)
 
 lemma has_deriv_within_at.liminf_right_slope_le
   (hf : has_deriv_within_at f f' (Ioi x) x) (hr : f' < r) :
-  ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r :=
+  ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r :=
 (hf.limsup_slope_le' (lt_irrefl x) hr).frequently
 
 end real
@@ -1713,12 +1712,12 @@ In other words, the limit superior of this ratio as `z` tends to `x` along `s`
 is less than or equal to `∥f'∥`. -/
 lemma has_deriv_within_at.limsup_norm_slope_le
   (hf : has_deriv_within_at f f' s x) (hr : ∥f'∥ < r) :
-  ∀ᶠ z in nhds_within x s, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
+  ∀ᶠ z in 𝓝[s] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
 begin
   have hr₀ : 0 < r, from lt_of_le_of_lt (norm_nonneg f') hr,
-  have A : ∀ᶠ z in nhds_within x (s \ {x}), ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
+  have A : ∀ᶠ z in 𝓝[s \ {x}] x, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
     from (has_deriv_within_at_iff_tendsto_slope.1 hf).norm (mem_nhds_sets is_open_Iio hr),
-  have B : ∀ᶠ z in nhds_within x {x}, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
+  have B : ∀ᶠ z in 𝓝[{x}] x, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
     from mem_sets_of_superset self_mem_nhds_within
       (singleton_subset_iff.2 $ by simp [hr₀]),
   have C := mem_sup_sets.2 ⟨A, B⟩,
@@ -1737,7 +1736,7 @@ This lemma is a weaker version of `has_deriv_within_at.limsup_norm_slope_le`
 where `∥f z∥ - ∥f x∥` is replaced by `∥f z - f x∥`. -/
 lemma has_deriv_within_at.limsup_slope_norm_le
   (hf : has_deriv_within_at f f' s x) (hr : ∥f'∥ < r) :
-  ∀ᶠ z in nhds_within x s, ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) < r :=
+  ∀ᶠ z in 𝓝[s] x, ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) < r :=
 begin
   apply (hf.limsup_norm_slope_le hr).mono,
   assume z hz,
@@ -1752,7 +1751,7 @@ is less than or equal to `∥f'∥`. See also `has_deriv_within_at.limsup_norm_s
 for a stronger version using limit superior and any set `s`. -/
 lemma has_deriv_within_at.liminf_right_norm_slope_le
   (hf : has_deriv_within_at f f' (Ioi x) x) (hr : ∥f'∥ < r) :
-  ∃ᶠ z in nhds_within x (Ioi x), ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
+  ∃ᶠ z in 𝓝[Ioi x] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
 (hf.limsup_norm_slope_le hr).frequently
 
 /-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ∥f'∥` the ratio
@@ -1768,7 +1767,7 @@ See also
   `∥f z - f x∥` instead of `∥f z∥ - ∥f x∥`. -/
 lemma has_deriv_within_at.liminf_right_slope_norm_le
   (hf : has_deriv_within_at f f' (Ioi x) x) (hr : ∥f'∥ < r) :
-  ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r :=
+  ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r :=
 begin
   have := (hf.limsup_slope_norm_le hr).frequently,
   refine this.mp (eventually.mono self_mem_nhds_within _),

src/analysis/calculus/extend_deriv.lean

@@ -34,7 +34,7 @@ with derivative `f'`. -/
 theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : set E} {x : E} {f' : E →L[ℝ] F}
   (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s)
   (f_cont : ∀y ∈ closure s, continuous_within_at f s y)
-  (h : tendsto (λy, fderiv ℝ f y) (nhds_within x s) (𝓝 f')) :
+  (h : tendsto (λy, fderiv ℝ f y) (𝓝[s] x) (𝓝 f')) :
   has_fderiv_within_at f f' (closure s) x :=
 begin
   classical,
@@ -83,7 +83,7 @@ begin
     obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s,
       by simpa [closure_prod_eq] using closure_mono this uv_in,
     apply continuous_within_at.mono _ this,
-    simp only [continuous_within_at, nhds_prod_eq] },
+    simp only [continuous_within_at] },
   rw nhds_within_prod_eq,
   { have : f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by abel,
     rw this,
@@ -100,8 +100,8 @@ end
 its derivative also converges at `a`, then `f` is differentiable on the right at `a`. -/
 lemma has_deriv_at_interval_left_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
   (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
-  (hs : s ∈ nhds_within a (Ioi a))
-  (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Ioi a)) (𝓝 e)) :
+  (hs : s ∈ 𝓝[Ioi a] a)
+  (f_lim' : tendsto (λx, deriv f x) (𝓝[Ioi a] a) (𝓝 e)) :
   has_deriv_within_at f e (Ici a) a :=
 begin
   /- This is a specialization of `has_fderiv_at_boundary_of_tendsto_fderiv`. To be in the setting of
@@ -122,7 +122,7 @@ begin
     { rw h, exact f_lim.mono ts },
     { have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (ne.symm h), hy.2⟩,
       exact (f_diff.continuous_on y this).mono ts } },
-  have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)),
+  have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)),
   { simp [deriv_fderiv.symm],
     refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
     exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Ioi_self) f_lim' },
@@ -137,8 +137,8 @@ end
 its derivative also converges at `a`, then `f` is differentiable on the left at `a`. -/
 lemma has_deriv_at_interval_right_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
   (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
-  (hs : s ∈ nhds_within a (Iio a))
-  (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Iio a)) (𝓝 e)) :
+  (hs : s ∈ 𝓝[Iio a] a)
+  (f_lim' : tendsto (λx, deriv f x) (𝓝[Iio a] a) (𝓝 e)) :
   has_deriv_within_at f e (Iic a) a :=
 begin
   /- This is a specialization of `has_fderiv_at_boundary_of_differentiable`. To be in the setting of
@@ -159,7 +159,7 @@ begin
     { rw h, exact f_lim.mono ts },
     { have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩,
       exact (f_diff.continuous_on y this).mono ts } },
-  have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)),
+  have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)),
   { simp [deriv_fderiv.symm],
     refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
     exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Iio_self) f_lim' },
@@ -184,7 +184,7 @@ begin
     -- extension results.
     apply has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff hf.continuous_within_at
       self_mem_nhds_within,
-    have : tendsto g (nhds_within x (Ioi x)) (𝓝 (g x)) := tendsto_inf_left hg,
+    have : tendsto g (𝓝[Ioi x] x) (𝓝 (g x)) := tendsto_inf_left hg,
     apply this.congr' _,
     apply mem_sets_of_superset self_mem_nhds_within (λy hy, _),
     exact (f_diff y (ne_of_gt hy)).deriv.symm },
@@ -195,7 +195,7 @@ begin
     -- extension results.
     apply has_deriv_at_interval_right_endpoint_of_tendsto_deriv diff hf.continuous_within_at
       self_mem_nhds_within,
-    have : tendsto g (nhds_within x (Iio x)) (𝓝 (g x)) := tendsto_inf_left hg,
+    have : tendsto g (𝓝[Iio x] x) (𝓝 (g x)) := tendsto_inf_left hg,
     apply this.congr' _,
     apply mem_sets_of_superset self_mem_nhds_within (λy hy, _),
     exact (f_diff y (ne_of_lt hy)).deriv.symm },

src/analysis/calculus/fderiv.lean

@@ -128,15 +128,15 @@ variables {G' : Type*} [normed_group G'] [normed_space 𝕜 G']
 /-- A function `f` has the continuous linear map `f'` as derivative along the filter `L` if
 `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` converges along the filter `L`. This definition
 is designed to be specialized for `L = 𝓝 x` (in `has_fderiv_at`), giving rise to the usual notion
-of Fréchet derivative, and for `L = nhds_within x s` (in `has_fderiv_within_at`), giving rise to
+of Fréchet derivative, and for `L = 𝓝[s] x` (in `has_fderiv_within_at`), giving rise to
 the notion of Fréchet derivative along the set `s`. -/
 def has_fderiv_at_filter (f : E → F) (f' : E →L[𝕜] F) (x : E) (L : filter E) :=
 is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L
 
 /-- A function `f` has the continuous linear map `f'` as derivative at `x` within a set `s` if
 `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x` inside `s`. -/
 def has_fderiv_within_at (f : E → F) (f' : E →L[𝕜] F) (s : set E) (x : E) :=
-has_fderiv_at_filter f f' x (nhds_within x s)
+has_fderiv_at_filter f f' x (𝓝[s] x)
 
 /-- A function `f` has the continuous linear map `f'` as derivative at `x` if
 `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x`. -/
@@ -213,13 +213,13 @@ theorem has_fderiv_within_at.lim (h : has_fderiv_within_at f f' s x) {α : Type*
   (cdlim : tendsto (λ n, c n • d n) l (𝓝 v)) :
   tendsto (λn, c n • (f (x + d n) - f x)) l (𝓝 (f' v)) :=
 begin
-  have tendsto_arg : tendsto (λ n, x + d n) l (nhds_within x s),
-  { conv in (nhds_within x s) { rw ← add_zero x },
+  have tendsto_arg : tendsto (λ n, x + d n) l (𝓝[s] x),
+  { conv in (𝓝[s] x) { rw ← add_zero x },
     rw [nhds_within, tendsto_inf],
     split,
     { apply tendsto_const_nhds.add (tangent_cone_at.lim_zero l clim cdlim) },
     { rwa tendsto_principal } },
-  have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (nhds_within x s) := h,
+  have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (𝓝[s] x) := h,
   have : is_o (λ n, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n)  - x) l :=
     this.comp_tendsto tendsto_arg,
   have : is_o (λ n, f (x + d n) - f x - f' (d n)) d l := by simpa only [add_sub_cancel'],
@@ -288,7 +288,7 @@ begin
 end
 
 theorem has_fderiv_within_at_iff_tendsto : has_fderiv_within_at f f' s x ↔
-  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) (nhds_within x s) (𝓝 0) :=
+  tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) (𝓝[s] x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
 theorem has_fderiv_at_iff_tendsto : has_fderiv_at f f' x ↔
@@ -379,7 +379,7 @@ begin
   exact unique_diff_within_at_univ.eq h₀ h₁
 end
 
-lemma has_fderiv_within_at_inter' (h : t ∈ nhds_within x s) :
+lemma has_fderiv_within_at_inter' (h : t ∈ 𝓝[s] x) :
   has_fderiv_within_at f f' (s ∩ t) x ↔ has_fderiv_within_at f f' s x :=
 by simp [has_fderiv_within_at, nhds_within_restrict'' s h]
 
@@ -395,7 +395,7 @@ begin
 end
 
 lemma has_fderiv_within_at.nhds_within (h : has_fderiv_within_at f f' s x)
-  (ht : s ∈ nhds_within x t) : has_fderiv_within_at f f' t x :=
+  (ht : s ∈ 𝓝[t] x) : has_fderiv_within_at f f' t x :=
 (has_fderiv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _))
 
 lemma has_fderiv_within_at.has_fderiv_at (h : has_fderiv_within_at f f' s x) (hs : s ∈ 𝓝 x) :
@@ -453,7 +453,7 @@ lemma differentiable_within_at_inter (ht : t ∈ 𝓝 x) :
 by simp only [differentiable_within_at, has_fderiv_within_at, has_fderiv_at_filter,
     nhds_within_restrict' s ht]
 
-lemma differentiable_within_at_inter' (ht : t ∈ nhds_within x s) :
+lemma differentiable_within_at_inter' (ht : t ∈ 𝓝[s] x) :
   differentiable_within_at 𝕜 f (s ∩ t) x ↔ differentiable_within_at 𝕜 f s x :=
 by simp only [differentiable_within_at, has_fderiv_within_at, has_fderiv_at_filter,
     nhds_within_restrict'' s ht]
@@ -617,7 +617,7 @@ lemma has_fderiv_within_at.congr (h : has_fderiv_within_at f f' s x) (hs : ∀x
 h.congr_mono hs hx (subset.refl _)
 
 lemma has_fderiv_within_at.congr_of_eventually_eq (h : has_fderiv_within_at f f' s x)
-  (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x :=
+  (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x :=
 has_fderiv_at_filter.congr_of_eventually_eq h h₁ hx
 
 lemma has_fderiv_at.congr_of_eventually_eq (h : has_fderiv_at f f' x)
@@ -633,7 +633,7 @@ lemma differentiable_within_at.congr (h : differentiable_within_at 𝕜 f s x)
 differentiable_within_at.congr_mono h ht hx (subset.refl _)
 
 lemma differentiable_within_at.congr_of_eventually_eq
-  (h : differentiable_within_at 𝕜 f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f)
+  (h : differentiable_within_at 𝕜 f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f)
   (hx : f₁ x = f x) : differentiable_within_at 𝕜 f₁ s x :=
 (h.has_fderiv_within_at.congr_of_eventually_eq h₁ hx).differentiable_within_at
 
@@ -661,7 +661,7 @@ lemma differentiable_within_at.fderiv_within_congr_mono (h : differentiable_with
 (has_fderiv_within_at.congr_mono h.has_fderiv_within_at hs hx h₁).fderiv_within hxt
 
 lemma filter.eventually_eq.fderiv_within_eq (hs : unique_diff_within_at 𝕜 s x)
-  (hL : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
+  (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
   fderiv_within 𝕜 f₁ s x = fderiv_within 𝕜 f s x :=
 if h : differentiable_within_at 𝕜 f s x
 then has_fderiv_within_at.fderiv_within (h.has_fderiv_within_at.congr_of_eventually_eq hL hx) hs
@@ -924,9 +924,9 @@ theorem has_fderiv_within_at.comp {g : F → G} {g' : F →L[𝕜] G} {t : set F
   has_fderiv_within_at (g ∘ f) (g'.comp f') s x :=
 begin
   apply has_fderiv_at_filter.comp _ (has_fderiv_at_filter.mono hg _) hf,
-  calc map f (nhds_within x s)
-      ≤ nhds_within (f x) (f '' s) : hf.continuous_within_at.tendsto_nhds_within_image
-  ... ≤ nhds_within (f x) t        : nhds_within_mono _ (image_subset_iff.mpr hst)
+  calc map f (𝓝[s] x)
+      ≤ 𝓝[f '' s] (f x) : hf.continuous_within_at.tendsto_nhds_within_image
+  ... ≤ 𝓝[t] (f x)        : nhds_within_mono _ (image_subset_iff.mpr hst)
 end
 
 /-- The chain rule. -/

src/analysis/calculus/local_extr.lean

@@ -123,7 +123,7 @@ begin
   have hc' : tendsto (λ n, ∥c n∥) at_top at_top,
     from tendsto_at_top_mono (λ n, le_abs_self _) hc,
   refine le_of_tendsto (hf.lim at_top hd hc' hcd) _,
-  replace hd : tendsto (λ n, a + d n) at_top (nhds_within (a + 0) s),
+  replace hd : tendsto (λ n, a + d n) at_top (𝓝[s] (a + 0)),
   from tendsto_inf.2 ⟨tendsto_const_nhds.add (tangent_cone_at.lim_zero _ hc' hcd),
     by rwa tendsto_principal⟩,
   rw [add_zero] at hd,