feat(order/filter): change definition of inf (#8657)

The current definition of `filter.inf` came directly from the Galois insertion: `u ∈ f ⊓ g` if it contains `s ∩ t` for some `s ∈ f` and `t ∈ g`, but the new one is tidier: `u ∈ f ⊓ g` if `u = s ∩ t` for some `s ∈ f` and `t ∈ g`. This gives a stronger assertion to work with when assuming a set belongs to a filter inf. On the other hand it makes it harder to prove such a statement so we keep the old version as a lemma `filter.mem_inf_of_inter :  ∀ {f g : filter α} {s t u : set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g`.

Also renames lots of lemmas to remove the word "sets" that was a remnant of the very early days.

In passing I also changed the simp lemma `filter.mem_map` from  `t ∈ map m f ↔ {x | m x ∈ t} ∈ f` to 
`t ∈ map m f ↔ m ⁻¹' t ∈ f` which seemed more normal form to me. But this led to a lot of breakage, so I also kept the old version as `mem_map'`.



Co-authored-by: Yury G. Kudryashov <[email protected]>

roadmap/topology/paracompact.lean

@@ -59,7 +59,7 @@ begin
   refine ⟨s, λ b, u b.val, λ b, uo b.val, _, _, λ b, ⟨b.val, subset.refl _⟩⟩,
   { todo },
   { intro x,
-    refine ⟨univ, univ_mem_sets, _⟩,
+    refine ⟨univ, univ_mem, _⟩,
     todo },
 end
 

src/analysis/analytic/basic.lean

@@ -346,7 +346,7 @@ lemma has_fpower_series_on_ball.mono
 protected lemma has_fpower_series_at.eventually (hf : has_fpower_series_at f p x) :
   ∀ᶠ r : ℝ≥0∞ in 𝓝[Ioi 0] 0, has_fpower_series_on_ball f p x r :=
 let ⟨r, hr⟩ := hf in
-mem_sets_of_superset (Ioo_mem_nhds_within_Ioi (left_mem_Ico.2 hr.r_pos)) $
+mem_of_superset (Ioo_mem_nhds_within_Ioi (left_mem_Ico.2 hr.r_pos)) $
   λ r' hr', hr.mono hr'.1 hr'.2.le
 
 lemma has_fpower_series_on_ball.add
@@ -997,7 +997,7 @@ lemma is_open_analytic_at : is_open {x | analytic_at 𝕜 f x} :=
 begin
   rw is_open_iff_mem_nhds,
   rintro x ⟨p, r, hr⟩,
-  exact mem_sets_of_superset (emetric.ball_mem_nhds _ hr.r_pos) (λ y hy, hr.analytic_at_of_mem hy)
+  exact mem_of_superset (emetric.ball_mem_nhds _ hr.r_pos) (λ y hy, hr.analytic_at_of_mem hy)
 end
 
 end

src/analysis/analytic/composition.lean

@@ -1044,7 +1044,7 @@ def sigma_equiv_sigma_pi (n : ℕ) :
     { blocks := (of_fn (λ j, (i.2 j).blocks)).join,
       blocks_pos :=
       begin
-        simp only [and_imp, mem_join, exists_imp_distrib, forall_mem_of_fn_iff],
+        simp only [and_imp, list.mem_join, exists_imp_distrib, forall_mem_of_fn_iff],
         exact λ i j hj, composition.blocks_pos _ hj
       end,
       blocks_sum := by simp [sum_of_fn, composition.blocks_sum, composition.sum_blocks_fun] },

src/analysis/asymptotics/asymptotics.lean

@@ -141,7 +141,7 @@ lemma is_O.is_O_with {f : α → E} {g : α → F} {l : filter α} :
   is_O f g l → ∃ c : ℝ, is_O_with c f g l := is_O_iff_is_O_with.1
 
 theorem is_O_with.weaken (h : is_O_with c f g' l) (hc : c ≤ c') : is_O_with c' f g' l :=
-is_O_with.of_bound $ mem_sets_of_superset h.bound $ λ x hx,
+is_O_with.of_bound $ mem_of_superset h.bound $ λ x hx,
 calc ∥f x∥ ≤ c * ∥g' x∥ : hx
 ... ≤ _ : mul_le_mul_of_nonneg_right hc (norm_nonneg _)
 
@@ -199,7 +199,7 @@ theorem is_O_with.congr' {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α →
 theorem is_O_with.congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
   (hc : c₁ = c₂) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
   is_O_with c₁ f₁ g₁ l → is_O_with c₂ f₂ g₂ l :=
-λ h, h.congr' hc (univ_mem_sets' hf) (univ_mem_sets' hg)
+λ h, h.congr' hc (univ_mem' hf) (univ_mem' hg)
 
 theorem is_O_with.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
   is_O_with c f₁ g l → is_O_with c f₂ g l :=
@@ -226,7 +226,7 @@ theorem is_O.congr' {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α
 theorem is_O.congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
     (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
   is_O f₁ g₁ l → is_O f₂ g₂ l :=
-λ h, h.congr' (univ_mem_sets' hf) (univ_mem_sets' hg)
+λ h, h.congr' (univ_mem' hf) (univ_mem' hg)
 
 theorem is_O.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
   is_O f₁ g l → is_O f₂ g l :=
@@ -249,7 +249,7 @@ theorem is_o.congr' {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α
 theorem is_o.congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
     (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
   is_o f₁ g₁ l → is_o f₂ g₂ l :=
-λ h, h.congr' (univ_mem_sets' hf) (univ_mem_sets' hg)
+λ h, h.congr' (univ_mem' hf) (univ_mem' hg)
 
 theorem is_o.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
   is_o f₁ g l → is_o f₂ g l :=
@@ -345,7 +345,7 @@ section
 variable (l)
 
 theorem is_O_with_of_le' (hfg : ∀ x, ∥f x∥ ≤ c * ∥g x∥) : is_O_with c f g l :=
-is_O_with.of_bound $ univ_mem_sets' hfg
+is_O_with.of_bound $ univ_mem' hfg
 
 theorem is_O_with_of_le (hfg : ∀ x, ∥f x∥ ≤ ∥g x∥) : is_O_with 1 f g l :=
 is_O_with_of_le' l $ λ x, by { rw one_mul, exact hfg x }
@@ -389,12 +389,12 @@ end bot
 
 theorem is_O_with.join (h : is_O_with c f g l) (h' : is_O_with c f g l') :
   is_O_with c f g (l ⊔ l') :=
-is_O_with.of_bound $ mem_sup_sets.2 ⟨h.bound, h'.bound⟩
+is_O_with.of_bound $ mem_sup.2 ⟨h.bound, h'.bound⟩
 
 theorem is_O_with.join' (h : is_O_with c f g' l) (h' : is_O_with c' f g' l') :
   is_O_with (max c c') f g' (l ⊔ l') :=
 is_O_with.of_bound $
-mem_sup_sets.2 ⟨(h.weaken $ le_max_left c c').bound, (h'.weaken $ le_max_right c c').bound⟩
+mem_sup.2 ⟨(h.weaken $ le_max_left c c').bound, (h'.weaken $ le_max_right c c').bound⟩
 
 theorem is_O.join (h : is_O f g' l) (h' : is_O f g' l') : is_O f g' (l ⊔ l') :=
 let ⟨c, hc⟩ := h.is_O_with, ⟨c', hc'⟩ := h'.is_O_with in (hc.join' hc').is_O
@@ -697,14 +697,14 @@ section zero_const
 variables (g g' l)
 
 theorem is_o_zero : is_o (λ x, (0 : E')) g' l :=
-is_o.of_bound $ λ c hc, univ_mem_sets' $ λ x,
+is_o.of_bound $ λ c hc, univ_mem' $ λ x,
 by simpa using mul_nonneg (le_of_lt hc) (norm_nonneg $ g' x)
 
 theorem is_O_with_zero (hc : 0 ≤ c) : is_O_with c (λ x, (0 : E')) g' l :=
-is_O_with.of_bound $ univ_mem_sets' $ λ x, by simpa using mul_nonneg hc (norm_nonneg $ g' x)
+is_O_with.of_bound $ univ_mem' $ λ x, by simpa using mul_nonneg hc (norm_nonneg $ g' x)
 
 theorem is_O_with_zero' : is_O_with 0 (λ x, (0 : E')) g l :=
-is_O_with.of_bound $ univ_mem_sets' $ λ x, by simp
+is_O_with.of_bound $ univ_mem' $ λ x, by simp
 
 theorem is_O_zero : is_O (λ x, (0 : E')) g l :=
 is_O_iff_is_O_with.2 ⟨0, is_O_with_zero' _ _⟩
@@ -734,7 +734,7 @@ theorem is_O_with_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α)
   is_O_with (∥c∥ / ∥c'∥) (λ x : α, c) (λ x, c') l :=
 begin
   unfold is_O_with,
-  apply univ_mem_sets',
+  apply univ_mem',
   intro x,
   rw [mem_set_of_eq, div_mul_cancel],
   rwa [ne.def, norm_eq_zero]
@@ -1261,7 +1261,7 @@ theorem div_is_bounded_under_of_is_O {α : Type*} {l : filter α}
   is_bounded_under (≤) l (λ x, ∥f x / g x∥) :=
 begin
   obtain ⟨c, hc⟩ := is_O_iff.mp h,
-  refine ⟨max c 0, eventually_map.2 (filter.mem_sets_of_superset hc (λ x hx, _))⟩,
+  refine ⟨max c 0, eventually_map.2 (filter.mem_of_superset hc (λ x hx, _))⟩,
   simp only [mem_set_of_eq, normed_field.norm_div] at ⊢ hx,
   by_cases hgx : g x = 0,
   { rw [hgx, norm_zero, div_zero, le_max_iff],
@@ -1277,7 +1277,7 @@ begin
   obtain ⟨c, hc⟩ := h,
   rw filter.eventually_iff at hgf hc,
   simp only [mem_set_of_eq, mem_map, normed_field.norm_div] at hc,
-  refine is_O_iff.2 ⟨c, filter.eventually_of_mem (inter_mem_sets hgf hc) (λ x hx, _)⟩,
+  refine is_O_iff.2 ⟨c, filter.eventually_of_mem (inter_mem hgf hc) (λ x hx, _)⟩,
   by_cases hgx : g x = 0,
   { simp [hx.1 hgx, hgx] },
   { refine (div_le_iff (norm_pos_iff.2 hgx)).mp hx.2 },
@@ -1324,7 +1324,7 @@ by simpa only [pow_one, is_o_norm_right] using @is_o_norm_pow_norm_pow E' _ _ _
 
 theorem is_O_with.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c f₁ f₂ l) (hc : c < 1) :
   is_O_with (1 / (1 - c)) f₂ (λx, f₂ x - f₁ x) l :=
-is_O_with.of_bound $ mem_sets_of_superset h.bound $ λ x hx,
+is_O_with.of_bound $ mem_of_superset h.bound $ λ x hx,
 begin
   simp only [mem_set_of_eq] at hx ⊢,
   rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff, mul_sub, mul_one, mul_comm],

src/analysis/calculus/deriv.lean

@@ -1872,10 +1872,10 @@ begin
   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 (is_open.mem_nhds is_open_Iio hr),
   have B : ∀ᶠ z in 𝓝[{x}] x, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
-    from mem_sets_of_superset self_mem_nhds_within
+    from mem_of_superset self_mem_nhds_within
       (singleton_subset_iff.2 $ by simp [hr₀]),
-  have C := mem_sup_sets.2 ⟨A, B⟩,
-  rw [← nhds_within_union, diff_union_self, nhds_within_union, mem_sup_sets] at C,
+  have C := mem_sup.2 ⟨A, B⟩,
+  rw [← nhds_within_union, diff_union_self, nhds_within_union, mem_sup] at C,
   filter_upwards [C.1],
   simp only [norm_smul, mem_Iio, normed_field.norm_inv],
   exact λ _, id

src/analysis/calculus/extend_deriv.lean

@@ -185,7 +185,7 @@ begin
       self_mem_nhds_within,
     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, _),
+    apply mem_of_superset self_mem_nhds_within (λy hy, _),
     exact (f_diff y (ne_of_gt hy)).deriv.symm },
   have B : has_deriv_within_at f (g x) (Iic x) x,
   { have diff : differentiable_on ℝ f (Iio x) :=
@@ -196,7 +196,7 @@ begin
       self_mem_nhds_within,
     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, _),
+    apply mem_of_superset self_mem_nhds_within (λy hy, _),
     exact (f_diff y (ne_of_lt hy)).deriv.symm },
   simpa using B.union A
 end

src/analysis/calculus/fderiv.lean

@@ -376,7 +376,7 @@ lemma has_fderiv_at.lim (hf : has_fderiv_at f f' x) (v : E) {α : Type*} {c : α
   {l : filter α} (hc : tendsto (λ n, ∥c n∥) l at_top) :
   tendsto (λ n, (c n) • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 (f' v)) :=
 begin
-  refine (has_fderiv_within_at_univ.2 hf).lim _ (univ_mem_sets' (λ _, trivial)) hc _,
+  refine (has_fderiv_within_at_univ.2 hf).lim _ (univ_mem' (λ _, trivial)) hc _,
   assume U hU,
   refine (eventually_ne_of_tendsto_norm_at_top hc (0:𝕜)).mono (λ y hy, _),
   convert mem_of_mem_nhds hU,
@@ -664,7 +664,7 @@ lemma has_fderiv_at_filter.congr_of_eventually_eq (h : has_fderiv_at_filter f f'
 
 lemma has_fderiv_within_at.congr_mono (h : has_fderiv_within_at f f' s x) (ht : ∀x ∈ t, f₁ x = f x)
   (hx : f₁ x = f x) (h₁ : t ⊆ s) : has_fderiv_within_at f₁ f' t x :=
-has_fderiv_at_filter.congr_of_eventually_eq (h.mono h₁) (filter.mem_inf_sets_of_right ht) hx
+has_fderiv_at_filter.congr_of_eventually_eq (h.mono h₁) (filter.mem_inf_of_right ht) hx
 
 lemma has_fderiv_within_at.congr (h : has_fderiv_within_at f f' s x) (hs : ∀x ∈ s, f₁ x = f x)
   (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x :=
@@ -734,7 +734,7 @@ lemma fderiv_within_congr (hs : unique_diff_within_at 𝕜 s x)
   fderiv_within 𝕜 f₁ s x = fderiv_within 𝕜 f s x :=
 begin
   apply filter.eventually_eq.fderiv_within_eq hs _ hx,
-  apply mem_sets_of_superset self_mem_nhds_within,
+  apply mem_of_superset self_mem_nhds_within,
   exact hL
 end
 
@@ -2778,7 +2778,7 @@ lemma has_fderiv_within_at.maps_to_tangent_cone {x : E} (h : has_fderiv_within_a
   maps_to f' (tangent_cone_at 𝕜 s x) (tangent_cone_at 𝕜 (f '' s) (f x)) :=
 begin
   rintros v ⟨c, d, dtop, clim, cdlim⟩,
-  refine ⟨c, (λn, f (x + d n) - f x), mem_sets_of_superset dtop _, clim,
+  refine ⟨c, (λn, f (x + d n) - f x), mem_of_superset dtop _, clim,
     h.lim at_top dtop clim cdlim⟩,
   simp [-mem_image, mem_image_of_mem] {contextual := tt}
 end

src/analysis/calculus/inverse.lean

@@ -316,7 +316,7 @@ lemma image_mem_nhds (hf : approximates_linear_on f f' s c) (f'symm : f'.nonline
 begin
   obtain ⟨t, hts, ht, xt⟩ : ∃ t ⊆ s, is_open t ∧ x ∈ t := _root_.mem_nhds_iff.1 hs,
   have := is_open.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt),
-  exact mem_sets_of_superset this (image_subset _ hts),
+  exact mem_of_superset this (image_subset _ hts),
 end
 
 lemma map_nhds_eq (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse)
@@ -326,8 +326,8 @@ begin
   refine le_antisymm ((hf.continuous_on x (mem_of_mem_nhds hs)).continuous_at hs)
     (le_map (λ t ht, _)),
   have : f '' (s ∩ t) ∈ 𝓝 (f x) := (hf.mono_set (inter_subset_left s t)).image_mem_nhds
-    f'symm (inter_mem_sets hs ht) hc,
-  exact mem_sets_of_superset this (image_subset _ (inter_subset_right _ _)),
+    f'symm (inter_mem hs ht) hc,
+  exact mem_of_superset this (image_subset _ (inter_subset_right _ _)),
 end
 
 end locally_onto

src/analysis/calculus/lhopital.lean

@@ -319,7 +319,7 @@ begin
   rcases hgg' with ⟨s₂, hs₂, hgg'⟩,
   rcases hg' with ⟨s₃, hs₃, hg'⟩,
   let s := s₁ ∩ s₂ ∩ s₃,
-  have hs : s ∈ 𝓝[Ioi a] a := inter_mem_sets (inter_mem_sets hs₁ hs₂) hs₃,
+  have hs : s ∈ 𝓝[Ioi a] a := inter_mem (inter_mem hs₁ hs₂) hs₃,
   rw mem_nhds_within_Ioi_iff_exists_Ioo_subset at hs,
   rcases hs with ⟨u, hau, hu⟩,
   refine lhopital_zero_right_on_Ioo hau _ _ _ hfa hga hdiv;
@@ -342,7 +342,7 @@ begin
   rcases hgg' with ⟨s₂, hs₂, hgg'⟩,
   rcases hg' with ⟨s₃, hs₃, hg'⟩,
   let s := s₁ ∩ s₂ ∩ s₃,
-  have hs : s ∈ 𝓝[Iio a] a := inter_mem_sets (inter_mem_sets hs₁ hs₂) hs₃,
+  have hs : s ∈ 𝓝[Iio a] a := inter_mem (inter_mem hs₁ hs₂) hs₃,
   rw mem_nhds_within_Iio_iff_exists_Ioo_subset at hs,
   rcases hs with ⟨l, hal, hl⟩,
   refine lhopital_zero_left_on_Ioo hal _ _ _ hfa hga hdiv;
@@ -396,7 +396,7 @@ begin
   rcases hgg' with ⟨s₂, hs₂, hgg'⟩,
   rcases hg' with ⟨s₃, hs₃, hg'⟩,
   let s := s₁ ∩ s₂ ∩ s₃,
-  have hs : s ∈ at_top := inter_mem_sets (inter_mem_sets hs₁ hs₂) hs₃,
+  have hs : s ∈ at_top := inter_mem (inter_mem hs₁ hs₂) hs₃,
   rw mem_at_top_sets at hs,
   rcases hs with ⟨l, hl⟩,
   have hl' : Ioi l ⊆ s := λ x hx, hl x (le_of_lt hx),
@@ -420,7 +420,7 @@ begin
   rcases hgg' with ⟨s₂, hs₂, hgg'⟩,
   rcases hg' with ⟨s₃, hs₃, hg'⟩,
   let s := s₁ ∩ s₂ ∩ s₃,
-  have hs : s ∈ at_bot := inter_mem_sets (inter_mem_sets hs₁ hs₂) hs₃,
+  have hs : s ∈ at_bot := inter_mem (inter_mem hs₁ hs₂) hs₃,
   rw mem_at_bot_sets at hs,
   rcases hs with ⟨l, hl⟩,
   have hl' : Iio l ⊆ s := λ x hx, hl x (le_of_lt hx),

src/analysis/calculus/local_extr.lean

@@ -81,15 +81,15 @@ def pos_tangent_cone_at (s : set E) (x : E) : set E :=
 lemma pos_tangent_cone_at_mono : monotone (λ s, pos_tangent_cone_at s a) :=
 begin
   rintros s t hst y ⟨c, d, hd, hc, hcd⟩,
-  exact ⟨c, d, mem_sets_of_superset hd $ λ h hn, hst hn, hc, hcd⟩
+  exact ⟨c, d, mem_of_superset hd $ λ h hn, hst hn, hc, hcd⟩
 end
 
 lemma mem_pos_tangent_cone_at_of_segment_subset {s : set E} {x y : E} (h : segment x y ⊆ s) :
   y - x ∈ pos_tangent_cone_at s x :=
 begin
   let c := λn:ℕ, (2:ℝ)^n,
   let d := λn:ℕ, (c n)⁻¹ • (y-x),
-  refine ⟨c, d, filter.univ_mem_sets' (λn, h _),
+  refine ⟨c, d, filter.univ_mem' (λn, h _),
     tendsto_pow_at_top_at_top_of_one_lt one_lt_two, _⟩,
   show x + d n ∈ segment x y,
   { rw segment_eq_image',

src/analysis/calculus/mean_value.lean

@@ -101,7 +101,7 @@ begin
   rintros x ⟨hxB : f x ≤ B x, xab⟩ y hy,
   cases hxB.lt_or_eq with hxB hxB,
   { -- If `f x < B x`, then all we need is continuity of both sides
-    refine nonempty_of_mem_sets (inter_mem_sets _ (Ioc_mem_nhds_within_Ioi ⟨le_rfl, hy⟩)),
+    refine nonempty_of_mem (inter_mem _ (Ioc_mem_nhds_within_Ioi ⟨le_rfl, hy⟩)),
     have : ∀ᶠ x in 𝓝[Icc a b] x, f x < B x,
       from A x (Ico_subset_Icc_self xab)
         (is_open.mem_nhds (is_open_lt continuous_fst continuous_snd) hxB),
@@ -1145,7 +1145,7 @@ begin
 -- turn little-o definition of strict_fderiv into an epsilon-delta statement
   refine is_o_iff.mpr (λ c hc, metric.eventually_nhds_iff_ball.mpr _),
 -- the correct ε is the modulus of continuity of f'
-  rcases metric.mem_nhds_iff.mp (inter_mem_sets hder (hcont $ ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩,
+  rcases metric.mem_nhds_iff.mp (inter_mem hder (hcont $ ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩,
   refine ⟨ε, ε0, _⟩,
 -- simplify formulas involving the product E × E
   rintros ⟨a, b⟩ h,

src/analysis/calculus/parametric_integral.lean

@@ -98,7 +98,7 @@ begin
   have : ∀ᶠ x in 𝓝 x₀,
       ∥x - x₀∥⁻¹ * ∥∫ a, F x a ∂μ - ∫ a, F x₀ a ∂μ - (∫ a, F' a ∂μ) (x - x₀)∥ =
        ∥∫ a, ∥x - x₀∥⁻¹ • (F x a - F x₀ a  - F' a (x - x₀)) ∂μ∥,
-  { apply mem_sets_of_superset (ball_mem_nhds _ ε_pos),
+  { apply mem_of_superset (ball_mem_nhds _ ε_pos),
     intros x x_in,
     rw [set.mem_set_of_eq, ← norm_smul_of_nonneg (nneg _), integral_smul,
         integral_sub, integral_sub, ← continuous_linear_map.integral_apply hF'_int],
@@ -113,7 +113,7 @@ begin
     apply ae_measurable.const_smul,
     exact ((hF_meas _ x_in).sub (hF_meas _ x₀_in)).sub (hF'_meas.apply_continuous_linear_map _) },
   { simp [measurable_const] },
-  { apply mem_sets_of_superset h_ball,
+  { apply mem_of_superset h_ball,
     intros x hx,
     apply (h_diff.and h_lipsch).mono,
     rintros a ⟨ha_deriv, ha_bound⟩,

src/analysis/calculus/specific_functions.lean

@@ -140,12 +140,12 @@ begin
     -- extension results.
     apply has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff _ self_mem_nhds_within,
     { refine (f_aux_limit (n+1)).congr' _,
-      apply mem_sets_of_superset self_mem_nhds_within (λx hx, _),
+      apply mem_of_superset self_mem_nhds_within (λx hx, _),
       simp [(f_aux_deriv_pos n x hx).deriv] },
     { have : f_aux n 0 = 0, by simp [f_aux, le_refl],
       simp only [continuous_within_at, this],
       refine (f_aux_limit n).congr' _,
-      apply mem_sets_of_superset self_mem_nhds_within (λx hx, _),
+      apply mem_of_superset self_mem_nhds_within (λx hx, _),
       have : ¬(x ≤ 0), by simpa using hx,
       simp [f_aux, this] } },
   simpa using A.union B,

src/analysis/calculus/tangent_cone.lean

@@ -76,7 +76,7 @@ lemma tangent_cone_univ : tangent_cone_at 𝕜 univ x = univ :=
 begin
   refine univ_subset_iff.1 (λy hy, _),
   rcases exists_one_lt_norm 𝕜 with ⟨w, hw⟩,
-  refine ⟨λn, w^n, λn, (w^n)⁻¹ • y, univ_mem_sets' (λn, mem_univ _),  _, _⟩,
+  refine ⟨λn, w^n, λn, (w^n)⁻¹ • y, univ_mem' (λn, mem_univ _),  _, _⟩,
   { simp only [norm_pow],
     exact tendsto_pow_at_top_at_top_of_one_lt hw },
   { convert tendsto_const_nhds,
@@ -92,7 +92,7 @@ lemma tangent_cone_mono (h : s ⊆ t) :
   tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x :=
 begin
   rintros y ⟨c, d, ds, ctop, clim⟩,
-  exact ⟨c, d, mem_sets_of_superset ds (λn hn, h hn), ctop, clim⟩
+  exact ⟨c, d, mem_of_superset ds (λn hn, h hn), ctop, clim⟩
 end
 
 /-- Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
@@ -213,7 +213,7 @@ lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment x y
 begin
   let c := λn:ℕ, (2:ℝ)^n,
   let d := λn:ℕ, (c n)⁻¹ • (y-x),
-  refine ⟨c, d, filter.univ_mem_sets' (λn, h _), _, _⟩,
+  refine ⟨c, d, filter.univ_mem' (λn, h _), _, _⟩,
   show x + d n ∈ segment x y,
   { rw segment_eq_image,
     refine ⟨(c n)⁻¹, ⟨_, _⟩, _⟩,
@@ -378,7 +378,7 @@ begin
     simp [(submodule.span ℝ (tangent_cone_at ℝ s x)).eq_top_of_nonempty_interior'
       ⟨y - x, interior_mono submodule.subset_span this⟩] },
   rw [mem_interior_iff_mem_nhds] at hy ⊢,
-  apply mem_sets_of_superset ((is_open_map_sub_right x).image_mem_nhds hy),
+  apply mem_of_superset ((is_open_map_sub_right x).image_mem_nhds hy),
   rintros _ ⟨z, zs, rfl⟩,
   exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs zs)
 end