feat(*): has_mem (set α) (filter α) (#799)

src/analysis/asymptotics.lean

@@ -41,10 +41,10 @@ section
 variables [has_norm β] [has_norm γ] [has_norm δ]
 
 def is_O (f : α → β) (g : α → γ) (l : filter α) : Prop :=
-∃ c > 0, { x | ∥ f x ∥ ≤ c * ∥ g x ∥ } ∈ l.sets
+∃ c > 0, { x | ∥ f x ∥ ≤ c * ∥ g x ∥ } ∈ l
 
 def is_o (f : α → β) (g : α → γ) (l : filter α) : Prop :=
-∀ c > 0, { x | ∥ f x ∥ ≤  c * ∥ g x ∥ } ∈ l.sets
+∀ c > 0, { x | ∥ f x ∥ ≤  c * ∥ g x ∥ } ∈ l
 
 theorem is_O_refl (f : α → β) (l : filter α) : is_O f f l :=
 ⟨1, zero_lt_one, by { filter_upwards [univ_mem_sets], intros x _, simp }⟩
@@ -124,14 +124,14 @@ begin
 end
 
 theorem is_O_congr {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
-    (hf : {x | f₁ x = f₂ x} ∈ l.sets) (hg : {x | g₁ x = g₂ x} ∈ l.sets) :
+    (hf : {x | f₁ x = f₂ x} ∈ l) (hg : {x | g₁ x = g₂ x} ∈ l) :
   is_O f₁ g₁ l ↔ is_O f₂ g₂ l :=
 bex_congr $ λ c _, filter.congr_sets $
 by filter_upwards [hf, hg] λ x e₁ e₂,
   by dsimp at e₁ e₂ ⊢; rw [e₁, e₂]
 
 theorem is_o_congr {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
-    (hf : {x | f₁ x = f₂ x} ∈ l.sets) (hg : {x | g₁ x = g₂ x} ∈ l.sets) :
+    (hf : {x | f₁ x = f₂ x} ∈ l) (hg : {x | g₁ x = g₂ x} ∈ l) :
   is_o f₁ g₁ l ↔ is_o f₂ g₂ l :=
 ball_congr $ λ c _, filter.congr_sets $
 by filter_upwards [hf, hg] λ x e₁ e₂,
@@ -148,12 +148,12 @@ theorem is_o.congr {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter 
 (is_o_congr (univ_mem_sets' hf) (univ_mem_sets' hg)).1
 
 theorem is_O_congr_left {f₁ f₂ : α → β} {g : α → γ} {l : filter α}
-    (h : {x | f₁ x = f₂ x} ∈ l.sets) :
+    (h : {x | f₁ x = f₂ x} ∈ l) :
   is_O f₁ g l ↔ is_O f₂ g l :=
 is_O_congr h (univ_mem_sets' $ λ _, rfl)
 
 theorem is_o_congr_left {f₁ f₂ : α → β} {g : α → γ} {l : filter α}
-    (h : {x | f₁ x = f₂ x} ∈ l.sets) :
+    (h : {x | f₁ x = f₂ x} ∈ l) :
   is_o f₁ g l ↔ is_o f₂ g l :=
 is_o_congr h (univ_mem_sets' $ λ _, rfl)
 
@@ -166,12 +166,12 @@ theorem is_o.congr_left {f₁ f₂ : α → β} {g : α → γ} {l : filter α}
 is_o.congr hf (λ _, rfl)
 
 theorem is_O_congr_right {f : α → β} {g₁ g₂ : α → γ} {l : filter α}
-    (h : {x | g₁ x = g₂ x} ∈ l.sets) :
+    (h : {x | g₁ x = g₂ x} ∈ l) :
   is_O f g₁ l ↔ is_O f g₂ l :=
 is_O_congr (univ_mem_sets' $ λ _, rfl) h
 
 theorem is_o_congr_right {f : α → β} {g₁ g₂ : α → γ} {l : filter α}
-    (h : {x | g₁ x = g₂ x} ∈ l.sets) :
+    (h : {x | g₁ x = g₂ x} ∈ l) :
   is_o f g₁ l ↔ is_o f g₂ l :=
 is_o_congr (univ_mem_sets' $ λ _, rfl) h
 
@@ -209,14 +209,14 @@ theorem is_o_neg_right {f : α → β} {g : α → γ} {l : filter α} :
 by { rw ←is_o_norm_right, simp only [norm_neg], rw is_o_norm_right }
 
 theorem is_O_iff {f : α → β} {g : α → γ} {l : filter α} :
-  is_O f g l ↔ ∃ c, { x | ∥f x∥ ≤ c * ∥g x∥ } ∈ l.sets :=
-suffices (∃ c, { x | ∥f x∥ ≤ c * ∥g x∥ } ∈ l.sets) → is_O f g l,
+  is_O f g l ↔ ∃ c, { x | ∥f x∥ ≤ c * ∥g x∥ } ∈ l :=
+suffices (∃ c, { x | ∥f x∥ ≤ c * ∥g x∥ } ∈ l) → is_O f g l,
   from ⟨λ ⟨c, cpos, hc⟩, ⟨c, hc⟩, this⟩,
 assume ⟨c, hc⟩,
 or.elim (lt_or_ge 0 c)
   (assume : c > 0, ⟨c, this, hc⟩)
   (assume h'c : c ≤ 0,
-    have {x : α | ∥f x∥ ≤ 1 * ∥g x∥} ∈ l.sets,
+    have {x : α | ∥f x∥ ≤ 1 * ∥g x∥} ∈ l,
       begin
         filter_upwards [hc], intros x,
         show ∥f x∥ ≤ c * ∥g x∥ → ∥f x∥ ≤ 1 * ∥g x∥,
@@ -349,7 +349,7 @@ theorem is_O_refl_left {f : α → β} {g : α → γ} {l : filter α} :
 by simpa using is_O_zero g l
 
 theorem is_O_zero_right_iff {f : α → β} {l : filter α} :
-  is_O f (λ x, (0 : γ)) l ↔ {x | f x = 0} ∈ l.sets :=
+  is_O f (λ x, (0 : γ)) l ↔ {x | f x = 0} ∈ l :=
 begin
   rw [is_O_iff], split,
   { rintros ⟨c, hc⟩,
@@ -374,7 +374,7 @@ theorem is_o_refl_left {f : α → β} {g : α → γ} {l : filter α} :
 by simpa using is_o_zero g l
 
 theorem is_o_zero_right_iff {f : α → β} (l : filter α) :
-  is_o f (λ x, (0 : γ)) l ↔ {x | f x = 0} ∈ l.sets :=
+  is_o f (λ x, (0 : γ)) l ↔ {x | f x = 0} ∈ l :=
 begin
   split,
   { intro h, exact is_O_zero_right_iff.mp h.to_is_O },
@@ -393,8 +393,10 @@ theorem is_O_const_one (c : β) (l : filter α) :
   is_O (λ x : α, c) (λ x, (1 : γ)) l :=
 begin
   rw is_O_iff,
-  use ∥c∥, simp only [norm_one, mul_one],
-  convert univ_mem_sets, simp only [le_refl]
+  refine ⟨∥c∥, _⟩,
+  simp only [norm_one, mul_one],
+  apply univ_mem_sets',
+  simp [le_refl],
 end
 
 end
@@ -404,13 +406,13 @@ variables [normed_field β] [normed_group γ]
 
 theorem is_O_const_mul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) (c : β) :
   is_O (λ x, c * f x) g l :=
-begin
+ begin
   cases classical.em (c = 0) with h'' h'',
   { simp [h''], apply is_O_zero },
   rcases h with ⟨c', c'pos, h'⟩,
   have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp h'',
   have cpos : ∥c∥ > 0, from lt_of_le_of_ne (norm_nonneg _) (ne.symm cne0),
-  use [∥c∥ * c', mul_pos cpos c'pos],
+  refine ⟨∥c∥ * c', mul_pos cpos c'pos, _⟩,
   filter_upwards [h'], dsimp,
   intros x h₀,
   rw [normed_field.norm_mul, mul_assoc],
@@ -467,7 +469,7 @@ begin
   have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp h',
   have cpos : ∥c∥ > 0, from lt_of_le_of_ne (norm_nonneg _) (ne.symm cne0),
   rcases h with ⟨c', c'pos, h''⟩,
-  use [c' * ∥c∥, mul_pos c'pos cpos],
+  refine ⟨c' * ∥c∥, mul_pos c'pos cpos, _⟩,
   convert h'', ext x, dsimp,
   rw [normed_field.norm_mul, mul_assoc]
 end
@@ -546,7 +548,7 @@ theorem is_O_mul {f₁ f₂ : α → β} {g₁ g₂ : α → γ} {l : filter α}
 begin
   rcases h₁ with ⟨c₁, c₁pos, hc₁⟩,
   rcases h₂ with ⟨c₂, c₂pos, hc₂⟩,
-  use [c₁ * c₂, mul_pos c₁pos c₂pos],
+  refine ⟨c₁ * c₂, mul_pos c₁pos c₂pos, _⟩,
   filter_upwards [hc₁, hc₂], dsimp,
   intros x hx₁ hx₂,
   rw [normed_field.norm_mul, normed_field.norm_mul, mul_assoc, mul_left_comm c₂, ←mul_assoc],

src/analysis/normed_space/basic.lean

@@ -118,7 +118,7 @@ lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
 theorem normed_space.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
-  tendsto f l (nhds 0) ↔ ∀ ε > 0, { x | ∥ f x ∥ < ε } ∈ l.sets :=
+  tendsto f l (nhds 0) ↔ ∀ ε > 0, { x | ∥ f x ∥ < ε } ∈ l :=
 begin
   rw [metric.tendsto_nhds], simp only [normed_group.dist_eq, sub_zero],
   split,

src/analysis/normed_space/deriv.lean

@@ -92,7 +92,7 @@ theorem has_fderiv_at_within_of_has_fderiv_at {f : E → F} {f' : E → F} {x :
 has_fderiv_at_filter_of_has_fderiv_at lattice.inf_le_left
 
 theorem has_fderiv_at_filter_congr' {f₀ f₁ : E → F} {f₀' f₁' : E → F} {x : E} {L : filter E}
-  (hx : f₀ x = f₁ x) (h₀ : {x | f₀ x = f₁ x} ∈ L.sets) (h₁ : ∀ x, f₀' x = f₁' x) :
+  (hx : f₀ x = f₁ x) (h₀ : {x | f₀ x = f₁ x} ∈ L) (h₁ : ∀ x, f₀' x = f₁' x) :
   has_fderiv_at_filter f₀ f₀' x L ↔ has_fderiv_at_filter f₁ f₁' x L :=
 by rw (funext h₁ : f₀' = f₁'); exact
 and_congr_right (λ _, is_o_congr

src/analysis/specific_limits.lean

@@ -36,7 +36,7 @@ tendsto_infi.2 $ assume p, tendsto_principal.2 $
       ... = 1 + add_monoid.smul n (r - 1) : by rw [add_monoid.smul_eq_mul]
       ... ≤ (1 + (r - 1)) ^ n : pow_ge_one_add_mul (le_of_lt this) _
       ... ≤ r ^ n : by simp; exact le_refl _,
-  show {n | p ≤ r ^ n} ∈ at_top.sets,
+  show {n | p ≤ r ^ n} ∈ at_top,
     from mem_at_top_sets.mpr ⟨n, assume m hnm, le_trans this (pow_le_pow (le_of_lt h) hnm)⟩
 
 lemma tendsto_inverse_at_top_nhds_0 : tendsto (λr:ℝ, r⁻¹) at_top (nhds 0) :=

src/data/analysis/filter.lean

@@ -52,7 +52,7 @@ def to_filter (F : cfilter (set α) σ) : filter α :=
     subset_inter (subset.trans (F.inf_le_left _ _) h₁) (subset.trans (F.inf_le_right _ _) h₂)⟩ }
 
 @[simp] theorem mem_to_filter_sets (F : cfilter (set α) σ) {a : set α} :
-  a ∈ F.to_filter.sets ↔ ∃ b, F b ⊆ a := iff.rfl
+  a ∈ F.to_filter ↔ ∃ b, F b ⊆ a := iff.rfl
 
 end cfilter
 
@@ -66,7 +66,7 @@ protected def cfilter.to_realizer (F : cfilter (set α) σ) : F.to_filter.realiz
 
 namespace filter.realizer
 
-theorem mem_sets {f : filter α} (F : f.realizer) {a : set α} : a ∈ f.sets ↔ ∃ b, F.F b ⊆ a :=
+theorem mem_sets {f : filter α} (F : f.realizer) {a : set α} : a ∈ f ↔ ∃ b, F.F b ⊆ a :=
 by cases F; subst f; simp
 
 -- Used because it has better definitional equalities than the eq.rec proof
@@ -230,4 +230,4 @@ by haveI := classical.prop_decidable;
 ⟨λ ⟨x, e⟩ _, ⟨x, le_of_eq e⟩,
  λ h, let ⟨x, h⟩ := h () in ⟨x, lattice.le_bot_iff.1 h⟩⟩
 
-end filter.realizer
+end filter.realizer

src/data/analysis/topology.lean

@@ -55,7 +55,7 @@ theorem to_topsp_is_topological_basis (F : ctop α σ) :
 eq_univ_iff_forall.2 $ λ x, ⟨_, ⟨_, rfl⟩, F.top_mem x⟩, rfl⟩
 
 @[simp] theorem mem_nhds_to_topsp (F : ctop α σ) {s : set α} {a : α} :
-  s ∈ (@nhds _ F.to_topsp a).sets ↔ ∃ b, a ∈ F b ∧ F b ⊆ s :=
+  s ∈ @nhds _ F.to_topsp a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s :=
 (@topological_space.mem_nhds_of_is_topological_basis
   _ F.to_topsp _ _ _ F.to_topsp_is_topological_basis).trans $
 ⟨λ ⟨_, ⟨x, rfl⟩, h⟩, ⟨x, h⟩, λ ⟨x, h⟩, ⟨_, ⟨x, rfl⟩, h⟩⟩
@@ -80,7 +80,7 @@ protected theorem is_basis [T : topological_space α] (F : realizer α) :
 by have := to_topsp_is_topological_basis F.F; rwa F.eq at this
 
 protected theorem mem_nhds [T : topological_space α] (F : realizer α) {s : set α} {a : α} :
-  s ∈ (nhds a).sets ↔ ∃ b, a ∈ F.F b ∧ F.F b ⊆ s :=
+  s ∈ nhds a ↔ ∃ b, a ∈ F.F b ∧ F.F b ⊆ s :=
 by have := mem_nhds_to_topsp F.F; rwa F.eq at this
 
 theorem is_open_iff [topological_space α] (F : realizer α) {s : set α} :
@@ -102,19 +102,19 @@ protected theorem is_open [topological_space α] (F : realizer α) (s : F.σ) :
 is_open_iff_nhds.2 $ λ a m, by simpa using F.mem_nhds.2 ⟨s, m, subset.refl _⟩
 
 theorem ext' [T : topological_space α] {σ : Type*} {F : ctop α σ}
-  (H : ∀ a s, s ∈ (nhds a).sets ↔ ∃ b, a ∈ F b ∧ F b ⊆ s) :
+  (H : ∀ a s, s ∈ nhds a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s) :
   F.to_topsp = T :=
 topological_space_eq $ funext $ λ s, begin
   have : ∀ T s, @topological_space.is_open _ T s ↔ _ := @is_open_iff_mem_nhds α,
   rw [this, this],
-  apply congr_arg (λ f : α → filter α, ∀ a ∈ s, s ∈ (f a).sets),
+  apply congr_arg (λ f : α → filter α, ∀ a ∈ s, s ∈ f a),
   funext a, apply filter_eq, apply set.ext, intro x,
   rw [mem_nhds_to_topsp, H]
 end
 
 theorem ext [T : topological_space α] {σ : Type*} {F : ctop α σ}
   (H₁ : ∀ a, is_open (F a))
-  (H₂ : ∀ a s, s ∈ (nhds a).sets → ∃ b, a ∈ F b ∧ F b ⊆ s) :
+  (H₂ : ∀ a s, s ∈ nhds a → ∃ b, a ∈ F b ∧ F b ⊆ s) :
   F.to_topsp = T :=
 ext' $ λ a s, ⟨H₂ a s, λ ⟨b, h₁, h₂⟩, mem_nhds_sets_iff.2 ⟨_, h₂, H₁ _, h₁⟩⟩
 

src/measure_theory/integration.lean

@@ -481,7 +481,7 @@ calc f.integral ≤ f.integral ⊔ g.integral : le_sup_left
   ... ≤ (f ⊔ g).integral : integral_sup_le _ _
   ... = g.integral : by rw [sup_of_le_right h]
 
-lemma integral_congr (f g : α →ₛ ennreal) (h : {a | f a = g a} ∈ (@measure_space.μ α _).a_e.sets) :
+lemma integral_congr (f g : α →ₛ ennreal) (h : {a | f a = g a} ∈ (@measure_space.μ α _).a_e) :
   f.integral = g.integral :=
 show ((pair f g).map prod.fst).integral = ((pair f g).map prod.snd).integral, from
 begin
@@ -546,7 +546,7 @@ begin
   refine le_antisymm
     (supr_le $ assume s, supr_le $ assume hs, _)
     (supr_le $ assume s, supr_le $ assume hs, le_supr_of_le (s.map c) $ le_supr _ hs),
-  by_cases {a | s a ≠ ⊤} ∈ ((@measure_space.μ α _).a_e).sets,
+  by_cases {a | s a ≠ ⊤} ∈ (@measure_space.μ α _).a_e,
   { have : f ≥ (s.map ennreal.to_nnreal).map c :=
       le_trans (assume a, ennreal.coe_to_nnreal_le_self) hs,
     refine le_supr_of_le (s.map ennreal.to_nnreal) (le_supr_of_le this (le_of_eq $ integral_congr _ _ _)),
@@ -736,7 +736,7 @@ lemma lintegral_le_lintegral_ae {f g : α → ennreal} (h : ∀ₘ a, f a ≤ g
   (∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
 begin
   rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, hts, ht, ht0⟩,
-  have : - t ∈ (@measure_space.μ α _).a_e.sets,
+  have : - t ∈ (@measure_space.μ α _).a_e,
   { rw [measure.mem_a_e_iff, lattice.neg_neg, ht0] },
   refine (supr_le $ assume s, supr_le $ assume hfs,
     le_supr_of_le (s.restrict (- t)) $ le_supr_of_le _ _),

src/measure_theory/measure_space.lean

@@ -861,7 +861,7 @@ associated with `α`. This means that the measure of the complementary of `p` is
 
 In a probability measure, the measure of `p` is `1`, when `p` is measurable.
 -/
-def all_ae (p : α → Prop) : Prop := { a | p a } ∈ (@measure_space.μ α _).a_e.sets
+def all_ae (p : α → Prop) : Prop := { a | p a } ∈ (@measure_space.μ α _).a_e
 
 notation `∀ₘ` binders `, ` r:(scoped P, all_ae P) := r