refactor(order/filter/basic): redefine filter.pure (#1889)

* refactor(order/filter/basic): redefine `filter.pure`

New definition has `s ∈ pure a` definitionally equal to `a ∈ s`.

* Update src/order/filter/basic.lean

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

* Minor fixes suggested by @gebner

* Fix compile

* Update src/order/filter/basic.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/measure_theory/indicator_function.lean

@@ -117,7 +117,7 @@ lemma tendsto_indicator_of_monotone [nonempty ι] (s : ι → set α) (hs : mono
   (a : α) : tendsto (λi, indicator (s i) f a) at_top (pure $ indicator (Union s) f a) :=
 begin
   by_cases h : ∃i, a ∈ s i,
-  { simp only [tendsto_principal, mem_singleton_iff, mem_at_top_sets, filter.pure_def, mem_set_of_eq],
+  { simp only [tendsto_pure, mem_at_top_sets, mem_set_of_eq],
     rcases h with ⟨i, hi⟩,
     use i, assume n hn,
     rw [indicator_of_mem (hs hn hi) _, indicator_of_mem ((subset_Union _ _) hi) _] },
@@ -134,7 +134,7 @@ lemma tendsto_indicator_of_antimono [nonempty ι] (s : ι → set α) (hs : ∀i
   (a : α) : tendsto (λi, indicator (s i) f a) at_top (pure $ indicator (Inter s) f a) :=
 begin
   by_cases h : ∃i, a ∉ s i,
-  { simp only [tendsto_principal, mem_singleton_iff, mem_at_top_sets, filter.pure_def, mem_set_of_eq],
+  { simp only [tendsto_pure, mem_at_top_sets, mem_set_of_eq],
     rcases h with ⟨i, hi⟩,
     use i, assume n hn,
     rw [indicator_of_not_mem _ _, indicator_of_not_mem _ _],
@@ -153,8 +153,7 @@ lemma tendsto_indicator_bUnion_finset (s : ι → set α) (f : α → β) (a : 
   tendsto (λ (n : finset ι), indicator (⋃i∈n, s i) f a) at_top (pure $ indicator (Union s) f a) :=
 begin
   by_cases h : ∃i, a ∈ s i,
-  { simp only [tendsto_principal, mem_singleton_iff, mem_at_top_sets, filter.pure_def,
-               mem_set_of_eq, ge_iff_le, finset.le_iff_subset],
+  { simp only [mem_at_top_sets, tendsto_pure, mem_set_of_eq, ge_iff_le, finset.le_iff_subset],
     rcases h with ⟨i, hi⟩,
     use {i}, assume n hn,
     replace hn : i ∈ n := hn (finset.mem_singleton_self _),

src/order/filter/basic.lean

@@ -785,27 +785,49 @@ def seq (f : filter (α → β)) (g : filter α) : filter β :=
     ⟨t₀ ∩ u₀, inter_mem_sets ht₀ hu₀, t₁ ∩ u₁, inter_mem_sets ht₁ hu₁,
       assume x ⟨hx₀, hx₁⟩ x ⟨hy₀, hy₁⟩, ⟨ht _ hx₀ _ hy₀, hu _ hx₁ _ hy₁⟩⟩⟩
 
-instance : has_pure filter := ⟨λ(α : Type u) x, principal {x}⟩
+/-- `pure x` is the set of sets that contain `x`. It is equal to `principal {x}` but
+with this definition we have `s ∈ pure a` defeq `a ∈ s`. -/
+instance : has_pure filter :=
+⟨λ (α : Type u) x,
+  { sets := {s | x ∈ s},
+    inter_sets := λ s t, and.intro,
+    sets_of_superset := λ s t hs hst, hst hs,
+    univ_sets := trivial }⟩
 
 instance : has_bind filter := ⟨@filter.bind⟩
 
 instance : has_seq filter := ⟨@filter.seq⟩
 
 instance : functor filter := { map := @filter.map }
 
+lemma pure_sets (a : α) : (pure a : filter α).sets = {s | a ∈ s} := rfl
+
+@[simp] lemma mem_pure_sets {a : α} {s : set α} : s ∈ (pure a : filter α) ↔ a ∈ s := iff.rfl
+
+lemma pure_eq_principal (a : α) : (pure a : filter α) = principal {a} :=
+filter.ext $ λ s, by simp only [mem_pure_sets, mem_principal_sets, singleton_subset_iff]
+
+@[simp] lemma map_pure (f : α → β) (a : α) : map f (pure a) = pure (f a) :=
+filter.ext $ λ s, iff.rfl
+
+@[simp] lemma join_pure (f : filter α) : join (pure f) = f := filter.ext $ λ s, iff.rfl
+
+@[simp] lemma pure_bind (a : α) (m : α → filter β) :
+  bind (pure a) m = m a :=
+by simp only [has_bind.bind, bind, map_pure, join_pure]
+
 section
 -- this section needs to be before applicative, otherwise the wrong instance will be chosen
 protected def monad : monad filter := { map := @filter.map }
 
 local attribute [instance] filter.monad
 protected lemma is_lawful_monad : is_lawful_monad filter :=
 { id_map     := assume α f, filter_eq rfl,
-  pure_bind  := assume α β a f, by simp only [has_bind.bind, pure, bind, Sup_image, image_singleton,
-    join_principal_eq_Sup, lattice.Sup_singleton, map_principal, eq_self_iff_true],
+  pure_bind  := assume α β, pure_bind,
   bind_assoc := assume α β γ f m₁ m₂, filter_eq rfl,
-  bind_pure_comp_eq_map := assume α β f x, filter_eq $
-    by simp only [has_bind.bind, pure, functor.map, bind, join, map, preimage, principal,
-      set.subset_univ, eq_self_iff_true, function.comp_app, mem_set_of_eq, singleton_subset_iff] }
+  bind_pure_comp_eq_map := assume α β f x, filter.ext $ λ s,
+    by simp only [has_bind.bind, bind, functor.map, mem_map, mem_join_sets, mem_set_of_eq,
+      function.comp, mem_pure_sets] }
 end
 
 instance : applicative filter := { map := @filter.map, seq := @filter.seq }
@@ -814,14 +836,6 @@ instance : alternative filter :=
 { failure := λα, ⊥,
   orelse  := λα x y, x ⊔ y }
 
-@[simp] lemma pure_def (x : α) : pure x = principal {x} := rfl
-
-@[simp] lemma mem_pure {a : α} {s : set α} : a ∈ s → s ∈ (pure a : filter α) :=
-by simp only [imp_self, pure_def, mem_principal_sets, singleton_subset_iff]; exact id
-
-@[simp] lemma mem_pure_iff {a : α} {s : set α} : s ∈ (pure a : filter α) ↔ a ∈ s :=
-by rw [pure_def, mem_principal_sets, set.singleton_subset_iff]
-
 @[simp] lemma map_def {α β} (m : α → β) (f : filter α) : m <$> f = map m f := rfl
 
 @[simp] lemma bind_def {α β} (f : filter α) (m : α → filter β) : f >>= m = bind f m := rfl
@@ -1092,15 +1106,18 @@ assume s hs, mem_sets_of_superset (h _ hs) $ image_preimage_subset _ _
 
 section applicative
 
-@[simp] lemma mem_pure_sets {a : α} {s : set α} :
-  s ∈ (pure a : filter α) ↔ a ∈ s :=
-by simp only [iff_self, pure_def, mem_principal_sets, singleton_subset_iff]
-
 lemma singleton_mem_pure_sets {a : α} : {a} ∈ (pure a : filter α) :=
-by simp only [mem_singleton, pure_def, mem_principal_sets, singleton_subset_iff]
+mem_singleton a
+
+lemma pure_inj : function.injective (pure : α → filter α) :=
+assume a b hab, (filter.ext_iff.1 hab {x | a = x}).1 rfl
 
 @[simp] lemma pure_ne_bot {α : Type u} {a : α} : pure a ≠ (⊥ : filter α) :=
-by simp only [pure, has_pure.pure, ne.def, not_false_iff, singleton_ne_empty, principal_eq_bot_iff]
+mt empty_in_sets_eq_bot.2 $ not_mem_empty a
+
+@[simp] lemma le_pure_iff {f : filter α} {a : α} : f ≤ pure a ↔ {a} ∈ f :=
+⟨λ h, h singleton_mem_pure_sets,
+  λ h s hs, mem_sets_of_superset h $ singleton_subset_iff.2 hs⟩
 
 lemma mem_seq_sets_def {f : filter (α → β)} {g : filter α} {s : set β} :
   s ∈ f.seq g ↔ (∃u ∈ f, ∃t ∈ g, ∀x∈u, ∀y∈t, (x : α → β) y ∈ s) :=
@@ -1133,28 +1150,17 @@ le_seq $ assume s hs t ht, seq_mem_seq_sets (hf hs) (hg ht)
 begin
   refine le_antisymm  (le_map $ assume s hs, _) (le_seq $ assume s hs t ht, _),
   { rw ← singleton_seq, apply seq_mem_seq_sets _ hs,
-    simp only [mem_singleton, pure_def, mem_principal_sets, singleton_subset_iff] },
-  { rw mem_pure_sets at hs,
-    refine sets_of_superset (map g f) (image_mem_map ht) _,
+    exact singleton_mem_pure_sets },
+  { refine sets_of_superset (map g f) (image_mem_map ht) _,
     rintros b ⟨a, ha, rfl⟩, exact ⟨g, hs, a, ha, rfl⟩ }
 end
 
-@[simp] lemma map_pure (f : α → β) (a : α) : map f (pure a) = pure (f a) :=
-le_antisymm
-  (le_principal_iff.2 $ sets_of_superset (map f (pure a)) (image_mem_map singleton_mem_pure_sets) $
-    by simp only [image_singleton, mem_singleton, singleton_subset_iff])
-  (le_map $ assume s, begin
-    simp only [mem_image, pure_def, mem_principal_sets, singleton_subset_iff],
-    exact assume has, ⟨a, has, rfl⟩
-  end)
-
 @[simp] lemma seq_pure (f : filter (α → β)) (a : α) : seq f (pure a) = map (λg:α → β, g a) f :=
 begin
   refine le_antisymm (le_map $ assume s hs, _) (le_seq $ assume s hs t ht, _),
-  { rw ← seq_singleton, exact seq_mem_seq_sets hs
-    (by simp only [mem_singleton, pure_def, mem_principal_sets, singleton_subset_iff]) },
-  { rw mem_pure_sets at ht,
-    refine sets_of_superset (map (λg:α→β, g a) f) (image_mem_map hs) _,
+  { rw ← seq_singleton,
+    exact seq_mem_seq_sets hs singleton_mem_pure_sets },
+  { refine sets_of_superset (map (λg:α→β, g a) f) (image_mem_map hs) _,
     rintros b ⟨g, hg, rfl⟩, exact ⟨g, hg, a, ht, rfl⟩ }
 end
 
@@ -1411,13 +1417,16 @@ lemma tendsto_principal_principal {f : α → β} {s : set α} {t : set β} :
   tendsto f (principal s) (principal t) ↔ ∀a∈s, f a ∈ t :=
 by simp only [tendsto, image_subset_iff, le_principal_iff, map_principal, mem_principal_sets]; refl
 
+lemma tendsto_pure {f : α → β} {a : filter α} {b : β} :
+  tendsto f a (pure b) ↔ {x | f x = b} ∈ a :=
+by simp only [tendsto, le_pure_iff, mem_map, mem_singleton_iff]
+
 lemma tendsto_pure_pure (f : α → β) (a : α) :
   tendsto f (pure a) (pure (f a)) :=
-show filter.map f (pure a) ≤ pure (f a),
-  by rw [filter.map_pure]; exact le_refl _
+tendsto_pure.2 rfl
 
-lemma tendsto_const_pure {a : filter α} {b : β} : tendsto (λa, b) a (pure b) :=
-by simp [tendsto]; exact univ_mem_sets
+lemma tendsto_const_pure {a : filter α} {b : β} : tendsto (λx, b) a (pure b) :=
+tendsto_pure.2 $ univ_mem_sets' $ λ _, rfl
 
 lemma tendsto_if {l₁ : filter α} {l₂ : filter β}
     {f g : α → β} {p : α → Prop} [decidable_pred p]
@@ -1543,7 +1552,7 @@ by simp only [filter.prod, comap_inf, inf_comm, inf_assoc, lattice.inf_left_comm
 by simp only [filter.prod, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; refl
 
 @[simp] lemma prod_pure_pure {a : α} {b : β} : filter.prod (pure a) (pure b) = pure (a, b) :=
-by simp
+by simp [pure_eq_principal]
 
 lemma prod_eq_bot {f : filter α} {g : filter β} : filter.prod f g = ⊥ ↔ (f = ⊥ ∨ g = ⊥) :=
 begin
@@ -2063,8 +2072,8 @@ lemma mem_traverse_sets_iff (fs : list β) (t : set (list α)) :
 begin
   split,
   { induction fs generalizing t,
-    case nil { simp only [sequence, pure_def, imp_self, forall₂_nil_left_iff, pure_def,
-      exists_eq_left, mem_principal_sets, set.pure_def, singleton_subset_iff, traverse_nil] },
+    case nil { simp only [sequence, mem_pure_sets, imp_self, forall₂_nil_left_iff,
+      exists_eq_left, set.pure_def, singleton_subset_iff, traverse_nil] },
     case cons : b fs ih t {
       assume ht,
       rcases mem_seq_sets_iff.1 ht with ⟨u, hu, v, hv, ht⟩,

src/topology/list.lean

@@ -22,7 +22,7 @@ begin
     case list.nil { exact le_refl _ },
     case list.cons : a l ih {
       suffices : list.cons <$> pure a <*> pure l ≤ list.cons <$> 𝓝 a <*> traverse 𝓝 l,
-      { simpa only [-filter.pure_def] with functor_norm using this },
+      { simpa only [] with functor_norm using this },
       exact filter.seq_mono (filter.map_mono $ pure_le_nhds a) ih } },
   { assume l s hs,
     rcases (mem_traverse_sets_iff _ _).1 hs with ⟨u, hu, hus⟩, clear as hs,
@@ -101,7 +101,7 @@ lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
 | 0     l  := tendsto_cons'
 | (n+1) [] :=
   suffices tendsto (λa, []) (𝓝 a) (𝓝 ([] : list α)),
-    by simpa [nhds_nil, tendsto, map_prod, -filter.pure_def, (∘), insert_nth],
+    by simpa [nhds_nil, tendsto, map_prod, (∘), insert_nth],
   tendsto_const_nhds
 | (n+1) (a'::l) :=
   have (𝓝 a).prod (𝓝 (a' :: l)) =

src/topology/order.lean

@@ -203,11 +203,9 @@ lemma continuous_of_discrete_topology [topological_space α] [discrete_topology
 
 lemma nhds_bot (α : Type*) : (@nhds α ⊥) = pure :=
 begin
-  ext a s,
-  rw [mem_nhds_sets_iff, mem_pure_iff],
-  split,
-  { exact assume ⟨t, ht, _, hta⟩, ht hta },
-  { exact assume h, ⟨{a}, set.singleton_subset_iff.2 h, trivial, set.mem_singleton a⟩ }
+  refine le_antisymm _ (@pure_le_nhds α ⊥),
+  assume a s hs,
+  exact @mem_nhds_sets α ⊥ a s trivial hs
 end
 
 lemma nhds_discrete (α : Type*) [topological_space α] [discrete_topology α] : (@nhds α _) = pure :=
@@ -225,9 +223,7 @@ le_antisymm
   (le_of_nhds_le_nhds $ assume x, le_of_eq $ (h x).symm)
 
 lemma eq_bot_of_singletons_open {t : topological_space α} (h : ∀ x, t.is_open {x}) : t = ⊥ :=
-bot_unique  $ le_of_nhds_le_nhds $ assume x,
-  have 𝓝 x ≤ pure x, from nhds_le_of_le (mem_singleton _) (h x) (by simp),
-  le_trans this (@pure_le_nhds _ ⊥ x)
+bot_unique $ λ s hs, bUnion_of_singleton s ▸ is_open_bUnion (λ x _, h x)
 
 end lattice
 

src/topology/stone_cech.lean

@@ -2,15 +2,18 @@
 Copyright (c) 2018 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton
+-/
+
+import topology.bases topology.dense_embedding
+
+/-! # Stone-Čech compactification
 
 Construction of the Stone-Čech compactification using ultrafilters.
 
 Parts of the formalization are based on "Ultrafilters and Topology"
 by Marius Stekelenburg, particularly section 5.
 -/
 
-import topology.bases topology.dense_embedding
-
 noncomputable theory
 
 open filter lattice set
@@ -89,9 +92,7 @@ begin
   rw ←le_principal_iff,
   refine lattice.infi_le_of_le {u | s ∈ u.val} _,
   refine lattice.infi_le_of_le ⟨hs, ⟨s, rfl⟩⟩ _,
-  rw principal_mono,
-  intros a ha,
-  exact mem_pure_iff.mp ha
+  exact principal_mono.2 (λ a, id)
 end
 
 section embedding
@@ -115,7 +116,7 @@ dense_inducing.mk' pure continuous_bot
       ultrafilter_converges_iff.mpr (bind_pure x).symm⟩)
   (assume a s as,
      ⟨{u | s ∈ u.val},
-      mem_nhds_sets (ultrafilter_is_open_basic s) (mem_pure_sets.mpr (mem_of_nhds as)),
+      mem_nhds_sets (ultrafilter_is_open_basic s) (mem_of_nhds as : a ∈ s),
       assume b hb, mem_pure_sets.mp hb⟩)
 
 -- The following refined version will never be used
@@ -172,7 +173,7 @@ lemma ultrafilter_extend_eq_iff {f : α → γ} {b : ultrafilter α} {c : γ} :
    -- the facts that ultrafilter.extend is a continuous extension of f.
    let b' : ultrafilter (ultrafilter α) := b.map pure,
    have t : b'.val ≤ 𝓝 b,
-     from ultrafilter_converges_iff.mpr (by exact (bind_pure _).symm),
+     from ultrafilter_converges_iff.mpr (bind_pure _).symm,
    rw ←h,
    have := (continuous_ultrafilter_extend f).tendsto b,
    refine le_trans _ (le_trans (map_mono t) this),

src/topology/uniform_space/cauchy.lean

@@ -49,9 +49,7 @@ lemma cauchy_nhds {a : α} : cauchy (𝓝 a) :=
     ... ≤ 𝓤 α : comp_le_uniformity⟩
 
 lemma cauchy_pure {a : α} : cauchy (pure a) :=
-cauchy_downwards cauchy_nhds
-  (show principal {a} ≠ ⊥, by simp)
-  (pure_le_nhds a)
+cauchy_downwards cauchy_nhds pure_ne_bot (pure_le_nhds a)
 
 /-- The common part of the proofs of `le_nhds_of_cauchy_adhp` and
 `sequentially_complete.le_nhds_of_seq_tendsto_nhds`: if for any entourage `s`

src/topology/uniform_space/completion.lean

@@ -150,12 +150,7 @@ lemma uniform_inducing_pure_cauchy : uniform_inducing (pure_cauchy : α → Cauc
       ... = 𝓤 α : by simp [this]⟩
 
 lemma uniform_embedding_pure_cauchy : uniform_embedding (pure_cauchy : α → Cauchy α) :=
-{ inj :=
-    assume a₁ a₂ h,
-    have (pure_cauchy a₁).val = (pure_cauchy a₂).val, from congr_arg _ h,
-    have {a₁} = ({a₂} : set α),
-      from principal_eq_iff_eq.mp this,
-    by simp at this; assumption,
+{ inj := assume a₁ a₂ h, pure_inj $ subtype.ext.1 h,
   ..uniform_inducing_pure_cauchy }
 
 lemma pure_cauchy_dense : ∀x, x ∈ closure (range pure_cauchy) :=
@@ -170,7 +165,7 @@ have h_ex : ∀ s ∈ 𝓤 (Cauchy α), ∃y:α, (f, pure_cauchy y) ∈ s, from
   let ⟨x, (hx : x ∈ t)⟩ := inhabited_of_mem_sets f.property.left ht in
   have t'' ∈ filter.prod f.val (pure x),
     from mem_prod_iff.mpr ⟨t, ht, {y:α | (x, y) ∈ t'},
-      assume y, begin simp, intro h, simp [h], exact refl_mem_uniformity ht'₁ end,
+      h $ mk_mem_prod hx hx,
       assume ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩,
         ht'₂ $ prod_mk_mem_comp_rel (@h (a, x) ⟨h₁, hx⟩) h₂⟩,
   ⟨x, ht''₂ $ by dsimp [gen]; exact this⟩,
@@ -213,7 +208,7 @@ complete_space_extension
     let ⟨t, ht₁, (ht₂ : gen t ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs in
     let ⟨t', ht', (h : set.prod t' t' ⊆ t)⟩ := mem_prod_same_iff.mp (hf.right ht₁) in
     have t' ⊆ { y : α | (f', pure_cauchy y) ∈ gen t },
-      from assume x hx, (filter.prod f (pure x)).sets_of_superset (prod_mem_prod ht' $ mem_pure hx) h,
+      from assume x hx, (filter.prod f (pure x)).sets_of_superset (prod_mem_prod ht' hx) h,
     f.sets_of_superset ht' $ subset.trans this (preimage_mono ht₂),
   ⟨f', by simp [nhds_eq_uniformity]; assumption⟩
 end