diff --git a/docs/theories/topology.md b/docs/theories/topology.md
index a790b58ad60a7..6ac2bd491dfaa 100644
--- a/docs/theories/topology.md
+++ b/docs/theories/topology.md
@@ -1,7 +1,7 @@
 # Maths in lean : Topological Spaces.
 
 The `topological_space` typeclass is defined in mathlib,
-in `topology/basic.lean`. There are over 4500
+in `topology/basic.lean`. There are about 18000
 lines of code in `topology` at the time of writing,
 covering the basics of topological spaces, continuous functions,
 topological groups and rings, and infinite sums. These docs
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index a560e864fe1ef..71b346e6dedf6 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -368,6 +368,24 @@ begin
   exact ⟨x, ⟨hx, hf _⟩⟩,
 end
 
+lemma eq_finite_Union_of_finite_subset_Union  {ι} {s : ι → set α} {t : set α} (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
+  ∃ I : set ι, (finite I) ∧ ∃ σ : {i | i ∈ I} → set α,
+     (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i :=
+let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
+⟨I, Ifin, λ x, s x ∩ t,
+    λ i, finite_subset tfin (inter_subset_right _ _),
+    λ i, inter_subset_left _ _,
+    begin
+      ext x,
+      rw mem_Union,
+      split,
+      { intro x_in,
+        rcases mem_Union.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩,
+        use [i, hi, H, x_in] },
+      { rintros ⟨i, hi, H⟩,
+        exact H }
+    end⟩
+
 lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))
   (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) :=
 finite_subset (finite_union hf hg) range_ite_subset
diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index af5e13b4a3bca..a2bf918c2c432 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -197,6 +197,14 @@ theorem diff_Inter (s : set β) (t : ι → set β) :
   s \ (⋂ i, t i) = ⋃ i, s \ t i :=
 by rw [diff_eq, compl_Inter, inter_Union]; refl
 
+lemma directed_on_Union {r} {ι : Sort v} {f : ι → set α} (hd : directed (⊆) f)
+  (h : ∀x, directed_on r (f x)) : directed_on r (⋃x, f x) :=
+by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact
+assume a₁ b₁ fb₁ a₂ b₂ fb₂,
+let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂,
+    ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in
+⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
+
 /- bounded unions and intersections -/
 
 theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
@@ -385,6 +393,13 @@ theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃
 
 theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union
 
+theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i :=
+begin
+  ext x,
+  simp only [mem_Union, mem_Inter, mem_sInter, exists_imp_distrib],
+  split ; tauto
+end
+
 @[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T := Sup_insert
 
 @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert
diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean
index 29cfdb7d7987e..ba96c9bcc3993 100644
--- a/src/measure_theory/bochner_integration.lean
+++ b/src/measure_theory/bochner_integration.lean
@@ -1026,7 +1026,7 @@ variables [normed_group β] [second_countable_topology β] [normed_space ℝ β]
   [measurable_space β] [borel_space β]
           [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ]
   [measurable_space γ] [borel_space γ]
-  
+
 /-- The Bochner integral -/
 def integral (f : α → β) : β :=
 if hf : measurable f ∧ integrable f
@@ -1151,7 +1151,7 @@ end
 /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
   {F : ι → α → β} {f : α → β} (bound : α → ℝ)
-  (hl_cb : l.has_countable_basis)
+  (hl_cb : l.is_countably_generated)
   (hF_meas : ∀ᶠ n in l, measurable (F n))
   (f_measurable : measurable f)
   (h_bound : ∀ᶠ n in l, ∀ₘ a, ∥F n a∥ ≤ bound a)
diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean
index bf26a73a00be0..537ed59ed1e17 100644
--- a/src/measure_theory/integration.lean
+++ b/src/measure_theory/integration.lean
@@ -1177,7 +1177,7 @@ end
 /-- Dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι}
   {F : ι → α → ennreal} {f : α → ennreal} (bound : α → ennreal)
-  (hl_cb : l.has_countable_basis)
+  (hl_cb : l.is_countably_generated)
   (hF_meas : ∀ᶠ n in l, measurable (F n))
   (h_bound : ∀ᶠ n in l, ∀ₘ a, F n a ≤ bound a)
   (h_fin : lintegral bound < ⊤)
diff --git a/src/measure_theory/set_integral.lean b/src/measure_theory/set_integral.lean
index ceba7c4f974e6..dc105caec272b 100644
--- a/src/measure_theory/set_integral.lean
+++ b/src/measure_theory/set_integral.lean
@@ -306,7 +306,7 @@ begin
 end
 
 -- TODO : prove this for an encodable type
--- by proving an encodable version of `filter.has_countable_basis_at_top_finset_nat`
+-- by proving an encodable version of `filter.is_countably_generated_at_top_finset_nat `
 lemma integral_on_Union (s : ℕ → set α) (f : α → β) (hm : ∀i, is_measurable (s i))
   (hd : ∀ i j, i ≠ j → s i ∩ s j = ∅) (hfm : measurable_on (Union s) f) (hfi : integrable_on (Union s) f) :
   (∫ a in (Union s), f a) = ∑i, ∫ a in s i, f a :=
@@ -322,7 +322,7 @@ begin
   rw this,
   refine tendsto_integral_filter_of_dominated_convergence _ _ _ _ _ _ _,
   { exact indicator (Union s) (λ a, ∥f a∥) },
-  { exact has_countable_basis_at_top_finset_nat },
+  { exact is_countably_generated_at_top_finset_nat },
   { refine univ_mem_sets' (λ n, _),
     simp only [mem_set_of_eq],
     refine hfm.subset (is_measurable.Union (λ i, is_measurable.Union_Prop (λh, hm _)))
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
index 8c85d842295db..6546636c8a69d 100644
--- a/src/order/complete_lattice.lean
+++ b/src/order/complete_lattice.lean
@@ -667,6 +667,10 @@ lemma infi_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
   (⨅ i (h : p i), f i h) = (⨅ x : subtype p, f x.val x.property) :=
 (@infi_subtype _ _ _ p (λ x, f x.val x.property)).symm
 
+lemma infi_subtype'' {ι} (s : set ι) (f : ι → α) :
+(⨅ i : s, f i) = ⨅ (t : ι) (H : t ∈ s), f t :=
+infi_subtype
+
 theorem supr_subtype {p : ι → Prop} {f : subtype p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
 le_antisymm
   (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean
index f950acea0e7f4..c2ffc57291c90 100644
--- a/src/order/filter/bases.lean
+++ b/src/order/filter/bases.lean
@@ -1,15 +1,34 @@
 /-
 Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Yury Kudryashov
+Author: Yury Kudryashov, Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 
-import order.filter.basic
+import order.filter.basic data.set.countable
 
 /-! # Filter bases
 
-In this file we define `filter.has_basis l p s`, where `l` is a filter on `α`, `p` is a predicate
-on some index set `ι`, and `s : ι → set α`.
+A filter basis `B : filter_basis α` on a type `α` is a nonempty collection of sets of `α`
+such that the intersection of two elements of this collection contains some element of
+the collection. Compared to filters, filter bases do not require that any set containing
+an element of `B` belongs to `B`.
+A filter basis `B` can be used to construct `B.filter : filter α` such that a set belongs
+to `B.filter` if and only if it contains an element of `B`.
+
+Given an indexing type `ι`, a predicate `p : ι → Prop`, and a map `s : ι → set α`,
+the proposition `h : filter.is_basis p s` makes sure the range of `s` bounded by `p`
+(ie. `s '' set_of p`) defines a filter basis `h.filter_basis`.
+
+If one already has a filter `l` on `α`, `filter.has_basis l p s` (where `p : ι → Prop`
+and `s : ι → set α` as above) means that a set belongs to `l` if and
+only if it contains some `s i` with `p i`. It implies `h : filter.is_basis p s`, and
+`l = h.filter_basis.filter`. The point of this definition is that checking statements
+involving elements of `l` often reduces to checking them on the basis elements.
+
+This file also introduces more restricted classes of bases, involving monotonicity or
+countability. In particular, for `l : filter α`, `l.is_countably_generated` means
+there is a countable set of sets which generates `s`. This is reformulated in term of bases,
+and consequences are derived.
 
 ## Main statements
 
@@ -23,6 +42,10 @@ on some index set `ι`, and `s : ι → set α`.
   of bases.
 * `has_basis.tendsto_right_iff`, `has_basis.tendsto_left_iff`, `has_basis.tendsto_iff` : restate
   `tendsto f l l'` in terms of bases.
+* `is_countably_generated_iff_exists_antimono_basis` : proves a filter is
+  countably generated if and only if it admis a basis parametrized by a
+  decreasing sequence of sets indexed by `ℕ`.
+* `tendsto_iff_seq_tendsto ` : an abstract version of "sequentially continuous implies continuous".
 
 ## Implementation notes
 
@@ -40,57 +63,204 @@ machinery, e.g., `simp only [exists_prop, true_and]` or `simp only [forall_const
 with the case `p = λ _, true`.
 -/
 
-namespace filter
+open set filter
+
 variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*} {ι' : Type*}
 
-open set
+/-- A filter basis `B` on a type `α` is a nonempty collection of sets of `α`
+such that the intersection of two elements of this collection contains some element
+of the collection. -/
+structure filter_basis (α : Type*) :=
+(sets                   : set (set α))
+(nonempty               : sets.nonempty)
+(inter_sets {x y}       : x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y)
+
+/-- If `B` is a filter basis on `α`, and `U` a subset of `α` then we can write `U ∈ B` as on paper. -/
+@[reducible]
+instance {α : Type*}: has_mem (set α) (filter_basis α) := ⟨λ U B, U ∈ B.sets⟩
+
+-- For illustration purposes, the filter basis defining (at_top : filter ℕ)
+instance : inhabited (filter_basis ℕ) :=
+⟨{ sets := range Ici,
+  nonempty := ⟨Ici 0, mem_range_self 0⟩,
+  inter_sets := begin
+    rintros _ _ ⟨n, rfl⟩ ⟨m, rfl⟩,
+    refine ⟨Ici (max n m), mem_range_self _, _⟩,
+    rintros p p_in,
+    split ; rw mem_Ici at *,
+    exact le_of_max_le_left p_in,
+    exact le_of_max_le_right p_in,
+  end }⟩
+
+/-- `is_basis p s` means the image of `s` bounded by `p` is a filter basis. -/
+protected structure filter.is_basis (p : ι → Prop) (s : ι → set α) : Prop :=
+(nonempty : ∃ i, p i)
+(inter : ∀ {i j}, p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j)
+
+namespace filter
+namespace is_basis
+
+/-- Constructs a filter basis from an indexed family of sets satisfying `is_basis`. -/
+protected def filter_basis {p : ι → Prop} {s : ι → set α} (h : is_basis p s) : filter_basis α :=
+{ sets := s '' set_of p,
+  nonempty := let ⟨i, hi⟩ := h.nonempty in ⟨s i, mem_image_of_mem s hi⟩,
+  inter_sets := by { rintros _ _ ⟨i, hi, rfl⟩ ⟨j, hj, rfl⟩,
+                     rcases h.inter hi hj with ⟨k, hk, hk'⟩,
+                     exact ⟨_, mem_image_of_mem s hk, hk'⟩ } }
+
+variables {p : ι → Prop} {s : ι → set α} (h : is_basis p s)
+
+lemma mem_filter_basis_iff {U : set α} : U ∈ h.filter_basis ↔ ∃ i, p i ∧ s i = U :=
+iff.rfl
+end is_basis
+end filter
+
+namespace filter_basis
+
+/-- The filter associated to a filter basis. -/
+protected def filter (B : filter_basis α) : filter α :=
+{ sets := {s | ∃ t ∈ B, t ⊆ s},
+  univ_sets := let ⟨s, s_in⟩ := B.nonempty in ⟨s, s_in, s.subset_univ⟩,
+  sets_of_superset := λ x y ⟨s, s_in, h⟩ hxy, ⟨s, s_in, set.subset.trans h hxy⟩,
+  inter_sets := λ x y ⟨s, s_in, hs⟩ ⟨t, t_in, ht⟩,
+                let ⟨u, u_in, u_sub⟩ := B.inter_sets s_in t_in in
+                ⟨u, u_in, set.subset.trans u_sub $ set.inter_subset_inter hs ht⟩ }
+
+lemma mem_filter_iff (B : filter_basis α) {U : set α} : U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U :=
+iff.rfl
+
+lemma mem_filter_of_mem (B : filter_basis α) {U : set α} : U ∈ B → U ∈ B.filter:=
+λ U_in, ⟨U, U_in, subset.refl _⟩
+
+lemma eq_infi_principal (B : filter_basis α) : B.filter = ⨅ s : B.sets, principal s :=
+begin
+  ext U,
+  rw [mem_filter_iff, mem_infi],
+  { simp },
+  { rintros ⟨U, U_in⟩ ⟨V, V_in⟩,
+    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩,
+    use [W, W_in],
+    finish },
+  cases B.nonempty with U U_in,
+  exact ⟨⟨U, U_in⟩⟩,
+end
+
+protected lemma generate (B : filter_basis α) : generate B.sets = B.filter :=
+begin
+  apply le_antisymm,
+  { intros U U_in,
+    rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩,
+    exact generate_sets.superset (generate_sets.basic V_in) h },
+  { rw sets_iff_generate,
+    apply mem_filter_of_mem }
+end
+end filter_basis
+
+namespace filter
+namespace is_basis
+variables {p : ι → Prop} {s : ι → set α}
+
+/-- Constructs a filter from an indexed family of sets satisfying `is_basis`. -/
+protected def filter (h : is_basis p s) : filter α := h.filter_basis.filter
+
+protected lemma mem_filter_iff (h : is_basis p s) {U : set α} :
+  U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U :=
+begin
+  erw [h.filter_basis.mem_filter_iff],
+  simp only [mem_filter_basis_iff h, exists_prop],
+  split,
+  { rintros ⟨_, ⟨i, pi, rfl⟩, h⟩,
+    tauto },
+  { tauto }
+end
+
+lemma filter_eq_generate (h : is_basis p s) : h.filter = generate {U | ∃ i, p i ∧ s i = U} :=
+by erw h.filter_basis.generate ; refl
+end is_basis
 
 /-- We say that a filter `l` has a basis `s : ι → set α` bounded by `p : ι → Prop`,
 if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`. -/
-protected def has_basis (l : filter α) (p : ι → Prop) (s : ι → set α) : Prop :=
-∀ t : set α, t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t
+protected structure has_basis (l : filter α) (p : ι → Prop) (s : ι → set α) : Prop :=
+(mem_iff' : ∀ (t : set α), t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t)
 
 section same_type
 
 variables {l l' : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} {i : ι}
   {p' : ι' → Prop} {s' : ι' → set α} {i' : ι'}
 
-/-- Definition of `has_basis` unfolded to make it useful for `rw` and `simp`. -/
+lemma has_basis_generate (s : set (set α)) : (generate s).has_basis (λ t, finite t ∧ t ⊆ s) (λ t, ⋂₀ t) :=
+⟨begin
+  intro U,
+  rw mem_generate_iff,
+  apply exists_congr,
+  tauto
+end⟩
+
+/-- The smallest filter basis containing a given collection of sets. -/
+def filter_basis.of_sets (s : set (set α)) : filter_basis α :=
+{ sets := sInter '' { t | finite t ∧ t ⊆ s},
+  nonempty := ⟨univ, ∅, ⟨⟨finite_empty, empty_subset s⟩, sInter_empty⟩⟩,
+  inter_sets := begin
+    rintros _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩,
+    exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨finite_union fina finb, union_subset suba subb⟩,
+           by rw sInter_union⟩,
+  end }
+
+/-- Definition of `has_basis` unfolded with implicit set argument. -/
 lemma has_basis.mem_iff (hl : l.has_basis p s) : t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t :=
-hl t
+hl.mem_iff' t
 
-lemma has_basis.eventually_iff (hl : l.has_basis p s) {q : α → Prop} :
-  (∀ᶠ x in l, q x) ↔ ∃ i (hi : p i), ∀ ⦃x⦄, x ∈ s i → q x :=
-hl _
+protected lemma is_basis.has_basis (h : is_basis p s) : has_basis h.filter p s :=
+⟨λ t, by simp only [h.mem_filter_iff, exists_prop]⟩
 
 lemma has_basis.mem_of_superset (hl : l.has_basis p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l :=
-(hl t).2 ⟨i, hi, ht⟩
+(hl.mem_iff).2 ⟨i, hi, ht⟩
 
 lemma has_basis.mem_of_mem (hl : l.has_basis p s) (hi : p i) : s i ∈ l :=
 hl.mem_of_superset hi $ subset.refl _
 
+lemma has_basis.is_basis (h : l.has_basis p s) : is_basis p s :=
+{ nonempty := let ⟨i, hi, H⟩ := h.mem_iff.mp univ_mem_sets in ⟨i, hi⟩,
+  inter := λ i j hi hj, by simpa [h.mem_iff] using l.inter_sets (h.mem_of_mem hi) (h.mem_of_mem hj) }
+
+lemma has_basis.filter_eq (h : l.has_basis p s) : h.is_basis.filter = l :=
+by { ext U, simp [h.mem_iff, is_basis.mem_filter_iff] }
+
+lemma has_basis.eq_generate (h : l.has_basis p s) : l = generate { U | ∃ i, p i ∧ s i = U } :=
+by rw [← h.is_basis.filter_eq_generate, h.filter_eq]
+
+lemma generate_eq_generate_inter (s : set (set α)) : generate s = generate (sInter '' { t | finite t ∧ t ⊆ s}) :=
+by erw [(filter_basis.of_sets s).generate, ← (has_basis_generate s).filter_eq] ; refl
+
+lemma of_sets_filter_eq_generate (s : set (set α)) : (filter_basis.of_sets s).filter = generate s :=
+by rw [← (filter_basis.of_sets s).generate, generate_eq_generate_inter s] ; refl
+
+lemma has_basis.eventually_iff (hl : l.has_basis p s) {q : α → Prop} :
+  (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x :=
+by simpa using hl.mem_iff
+
 lemma has_basis.forall_nonempty_iff_ne_bot (hl : l.has_basis p s) :
   (∀ {i}, p i → (s i).nonempty) ↔ l ≠ ⊥ :=
 ⟨λ H, forall_sets_nonempty_iff_ne_bot.1 $
-  λ s hs, let ⟨i, hi, his⟩ := (hl s).1 hs in (H hi).mono his,
+  λ s hs, let ⟨i, hi, his⟩ := hl.mem_iff.1 hs in (H hi).mono his,
   λ H i hi, nonempty_of_mem_sets H (hl.mem_of_mem hi)⟩
 
 lemma basis_sets (l : filter α) : l.has_basis (λ s : set α, s ∈ l) id :=
-λ t, exists_sets_subset_iff.symm
+⟨λ t, exists_sets_subset_iff.symm⟩
 
 lemma at_top_basis [nonempty α] [semilattice_sup α] :
   (@at_top α _).has_basis (λ _, true) Ici :=
-λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t
+⟨λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t⟩
 
 lemma at_top_basis' [semilattice_sup α] (a : α) :
   (@at_top α _).has_basis (λ x, a ≤ x) Ici :=
-λ t, (@at_top_basis α ⟨a⟩ _ t).trans
+⟨λ t, (@at_top_basis α ⟨a⟩ _).mem_iff.trans
   ⟨λ ⟨x, _, hx⟩, ⟨x ⊔ a, le_sup_right, λ y hy, hx (le_trans le_sup_left hy)⟩,
-    λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩
+    λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩⟩
 
 theorem has_basis.ge_iff (hl' : l'.has_basis p' s')  : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l :=
 ⟨λ h i' hi', h $ hl'.mem_of_mem hi',
-  λ h s hs, let ⟨i', hi', hs⟩ := (hl' s).1 hs in mem_sets_of_superset (h _ hi') hs⟩
+  λ h s hs, let ⟨i', hi', hs⟩ := hl'.mem_iff.1 hs in mem_sets_of_superset (h _ hi') hs⟩
 
 theorem has_basis.le_iff (hl : l.has_basis p s) : l ≤ l' ↔ ∀ t ∈ l', ∃ i (hi : p i), s i ⊆ t :=
 by simp only [le_def, hl.mem_iff]
@@ -101,7 +271,7 @@ by simp only [hl'.ge_iff, hl.mem_iff]
 
 lemma has_basis.inf (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
   (l ⊓ l').has_basis (λ i : ι × ι', p i.1 ∧ p' i.2) (λ i, s i.1 ∩ s' i.2) :=
-begin
+⟨begin
   intro t,
   simp only [mem_inf_sets, exists_prop, hl.mem_iff, hl'.mem_iff],
   split,
@@ -109,12 +279,12 @@ begin
     use [(i, i'), ⟨hi, hi'⟩, subset.trans (inter_subset_inter ht ht') H] },
   { rintros ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩,
     use [s i, i, hi, subset.refl _, s' i', i', hi', subset.refl _, H] }
-end
+end⟩
 
 lemma has_basis.inf_principal (hl : l.has_basis p s) (s' : set α) :
   (l ⊓ principal s').has_basis p (λ i, s i ∩ s') :=
-λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq,
-  mem_inter_iff, and_imp]
+⟨λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq,
+  mem_inter_iff, and_imp]⟩
 
 lemma has_basis.eq_binfi (h : l.has_basis p s) :
   l = ⨅ i (_ : p i), principal (s i) :=
@@ -127,30 +297,30 @@ by simpa only [infi_true] using h.eq_binfi
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma has_basis_infi_principal {s : ι → set α} (h : directed (≥) s) (ne : nonempty ι) :
   (⨅ i, principal (s i)).has_basis (λ _, true) s :=
-begin
+⟨begin
   refine λ t, (mem_infi (h.mono_comp _ _) ne t).trans $
     by simp only [exists_prop, true_and, mem_principal_sets],
   exact λ _ _, principal_mono.2
-end
+end⟩
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma has_basis_binfi_principal {s : β → set α} {S : set β} (h : directed_on (s ⁻¹'o (≥)) S)
   (ne : S.nonempty) :
   (⨅ i ∈ S, principal (s i)).has_basis (λ i, i ∈ S) s :=
-begin
+⟨begin
   refine λ t, (mem_binfi _ ne).trans $ by simp only [mem_principal_sets],
   rw [directed_on_iff_directed, ← directed_comp, (∘)] at h ⊢,
   apply h.mono_comp _ _,
   exact λ _ _, principal_mono.2
-end
+end⟩
 
 lemma has_basis.map (f : α → β) (hl : l.has_basis p s) :
   (l.map f).has_basis p (λ i, f '' (s i)) :=
-λ t, by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]
+⟨λ t, by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]⟩
 
 lemma has_basis.comap (f : β → α) (hl : l.has_basis p s) :
   (l.comap f).has_basis p (λ i, f ⁻¹' (s i)) :=
-begin
+⟨begin
   intro t,
   simp only [mem_comap_sets, exists_prop, hl.mem_iff],
   split,
@@ -158,11 +328,11 @@ begin
     exact ⟨i, hi, subset.trans (preimage_mono ht') H⟩ },
   { rintros ⟨i, hi, H⟩,
     exact ⟨s i, ⟨i, hi, subset.refl _⟩, H⟩ }
-end
+end⟩
 
 lemma has_basis.prod_self (hl : l.has_basis p s) :
   (l.prod l).has_basis p (λ i, (s i).prod (s i)) :=
-begin
+⟨begin
   intro t,
   apply mem_prod_iff.trans,
   split,
@@ -171,8 +341,22 @@ begin
     exact ⟨i, hi, λ p ⟨hp₁, hp₂⟩, H ⟨(ht hp₁).1, (ht hp₂).2⟩⟩ },
   { rintros ⟨i, hi, H⟩,
     exact ⟨s i, hl.mem_of_mem hi, s i, hl.mem_of_mem hi, H⟩ }
-end
-
+end⟩
+variables [preorder ι] (l p s)
+
+/-- `is_antimono_basis p s` means the image of `s` bounded by `p` is a filter basis
+such that `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/
+structure is_antimono_basis extends is_basis p s : Prop :=
+(decreasing : ∀ {i j}, p i → p j → i ≤ j → s j ⊆ s i)
+(mono : monotone p)
+
+/-- We say that a filter `l` has a antimono basis `s : ι → set α` bounded by `p : ι → Prop`,
+if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`,
+and `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/
+structure has_antimono_basis [preorder ι] (l : filter α) (p : ι → Prop) (s : ι → set α)
+  extends has_basis l p s : Prop :=
+(decreasing : ∀ {i j}, p i → p j → i ≤ j → s j ⊆ s i)
+(mono : monotone p)
 end same_type
 
 section two_types
@@ -190,7 +374,7 @@ by simp only [tendsto, hlb.ge_iff, mem_map, filter.eventually]
 
 lemma has_basis.tendsto_iff (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
   tendsto f la lb ↔ ∀ ib (hib : pb ib), ∃ ia (hia : pa ia), ∀ x ∈ sa ia, f x ∈ sb ib :=
-by simp only [hlb.tendsto_right_iff, hla.eventually_iff, subset_def, mem_set_of_eq]
+by simp [hlb.tendsto_right_iff, hla.eventually_iff]
 
 lemma tendsto.basis_left (H : tendsto f la lb) (hla : la.has_basis pa sa) :
   ∀ t ∈ lb, ∃ i (hi : pa i), ∀ x ∈ sa i, f x ∈ t :=
@@ -209,6 +393,257 @@ lemma has_basis.prod (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
   (la.prod lb).has_basis (λ i : ι × ι', pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) :=
 (hla.comap prod.fst).inf (hlb.comap prod.snd)
 
+lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α}
+  {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α}
+  (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l  :=
+begin
+  rw hl.to_has_basis.tendsto_right_iff,
+  intros i hi,
+  rw eventually_at_top,
+  exact ⟨i, λ j hij, hl.decreasing hi (hl.mono hij hi) hij (h j)⟩,
+end
+
 end two_types
 
+/-- `is_countably_generated f` means `f = generate s` for some countable `s`. -/
+def is_countably_generated (f : filter α) : Prop :=
+∃ s : set (set α), countable s ∧ f = generate s
+
+/-- `is_countable_basis p s` means the image of `s` bounded by `p` is a countable filter basis. -/
+structure is_countable_basis (p : ι → Prop) (s : ι → set α) extends is_basis p s : Prop :=
+(countable : countable $ set_of p)
+
+/-- We say that a filter `l` has a countable basis `s : ι → set α` bounded by `p : ι → Prop`,
+if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`, and the set
+defined by `p` is countable. -/
+structure has_countable_basis (l : filter α) (p : ι → Prop) (s : ι → set α) extends has_basis l p s : Prop :=
+(countable : countable $ set_of p)
+
+/-- A countable filter basis `B` on a type `α` is a nonempty countable collection of sets of `α`
+such that the intersection of two elements of this collection contains some element
+of the collection. -/
+structure countable_filter_basis (α : Type*) extends filter_basis α :=
+(countable : countable sets)
+
+-- For illustration purposes, the countable filter basis defining (at_top : filter ℕ)
+instance nat.inhabited_countable_filter_basis : inhabited (countable_filter_basis ℕ) :=
+⟨{ countable := countable_range (λ n, Ici n),
+   ..(default $ filter_basis ℕ),}⟩
+
+lemma antimono_seq_of_seq (s : ℕ → set α) :
+  ∃ t : ℕ → set α, (∀ i j, i ≤ j → t j ⊆ t i) ∧ (⨅ i, principal $ s i) = ⨅ i, principal (t i) :=
+begin
+  use λ n, ⋂ m ≤ n, s m, split,
+  { intros i j hij a, simp, intros h i' hi'i, apply h, transitivity; assumption },
+    apply le_antisymm; rw le_infi_iff; intro i,
+  { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _),
+    intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ },
+  { apply infi_le_of_le i _, rw principal_mono, intro a, simp, intro h, apply h, refl },
+end
+
+lemma countable_binfi_eq_infi_seq [complete_lattice α] {B : set ι} (Bcbl : countable B) (Bne : B.nonempty) (f : ι → α)
+ : ∃ (x : ℕ → ι), (⨅ t ∈ B, f t) = ⨅ i, f (x i) :=
+begin
+  rw countable_iff_exists_surjective_to_subtype Bne at Bcbl,
+  rcases Bcbl with ⟨g, gsurj⟩,
+  rw infi_subtype',
+  use (λ n, g n), apply le_antisymm; rw le_infi_iff,
+  { intro i, apply infi_le_of_le (g i) _, apply le_refl _ },
+  { intros a, rcases gsurj a with i, apply infi_le_of_le i _, subst h, apply le_refl _ }
+end
+
+lemma countable_binfi_eq_infi_seq' [complete_lattice α] {B : set ι} (Bcbl : countable B) (f : ι → α)
+{i₀ : ι} (h : f i₀ = ⊤) :
+  ∃ (x : ℕ → ι), (⨅ t ∈ B, f t) = ⨅ i, f (x i) :=
+begin
+  cases B.eq_empty_or_nonempty with hB Bnonempty,
+  { rw [hB, infi_emptyset],
+    use λ n, i₀,
+    simp [h] },
+  { exact countable_binfi_eq_infi_seq Bcbl Bnonempty f }
+end
+
+lemma countable_binfi_principal_eq_seq_infi {B : set (set α)} (Bcbl : countable B) :
+  ∃ (x : ℕ → set α), (⨅ t ∈ B, principal t) = ⨅ i, principal (x i) :=
+countable_binfi_eq_infi_seq' Bcbl principal principal_univ
+
+namespace is_countably_generated
+
+/-- A set generating a countably generated filter. -/
+def generating_set {f : filter α} (h : is_countably_generated f) :=
+classical.some h
+
+lemma countable_generating_set {f : filter α} (h : is_countably_generated f) :
+  countable h.generating_set :=
+(classical.some_spec h).1
+
+lemma eq_generate {f : filter α} (h : is_countably_generated f) :
+  f = generate h.generating_set :=
+(classical.some_spec h).2
+
+/-- A countable filter basis for a countably generated filter. -/
+def countable_filter_basis {l : filter α} (h : is_countably_generated l) : countable_filter_basis α :=
+{ countable := countable_image _ (countable_set_of_finite_subset h.countable_generating_set),
+  ..filter_basis.of_sets (h.generating_set) }
+
+lemma filter_basis_filter {l : filter α} (h : is_countably_generated l) :
+h.countable_filter_basis.to_filter_basis.filter = l :=
+begin
+  conv_rhs { rw h.eq_generate },
+  apply of_sets_filter_eq_generate,
+end
+
+lemma has_countable_basis {l : filter α} (h : is_countably_generated l) :
+  l.has_countable_basis (λ t, finite t ∧ t ⊆ h.generating_set) (λ t, ⋂₀ t) :=
+⟨by convert has_basis_generate _ ; exact h.eq_generate,
+ countable_set_of_finite_subset h.countable_generating_set⟩
+
+lemma exists_countable_infi_principal {f : filter α} (h : f.is_countably_generated) :
+∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t :=
+begin
+  let B := h.countable_filter_basis,
+  use [B.sets, B.countable],
+  rw ← h.filter_basis_filter,
+  rw B.to_filter_basis.eq_infi_principal,
+  rw infi_subtype''
+end
+
+lemma exists_seq {f : filter α} (cblb : f.is_countably_generated) :
+    ∃ x : ℕ → set α, f = ⨅ i, principal (x i) :=
+begin
+  rcases cblb.exists_countable_infi_principal with ⟨B, Bcbl, rfl⟩,
+  exact countable_binfi_principal_eq_seq_infi Bcbl,
+end
+
+lemma exists_antimono_seq {f : filter α} (cblb : f.is_countably_generated) :
+  ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ f = ⨅ i, principal (x i) :=
+begin
+  rcases cblb.exists_seq with ⟨x', hx'⟩,
+  let x := λ n, ⋂ m ≤ n, x' m,
+  use x, split,
+  { intros i j hij a, simp [x], intros h i' hi'i, apply h, transitivity; assumption },
+  subst hx', apply le_antisymm; rw le_infi_iff; intro i,
+  { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _),
+    intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ },
+  { apply infi_le_of_le i _, rw principal_mono, intro a, simp [x], intro h, apply h, refl },
+end
+
+lemma has_antimono_basis {f : filter α} (h : f.is_countably_generated) :
+ ∃ x : ℕ → set α, f.has_antimono_basis (λ _, true) x :=
+begin
+  rcases h.exists_antimono_seq with ⟨x, x_dec, rfl⟩,
+  use x,
+  constructor,
+  apply has_basis_infi_principal,
+  apply directed_of_mono, apply x_dec,
+  use 0,
+  simpa using x_dec,
+  exact monotone_const
+end
+
+end is_countably_generated
+
+lemma is_countably_generated_seq (x : ℕ → set α) : is_countably_generated (⨅ i, principal $ x i) :=
+begin
+  rcases antimono_seq_of_seq x with ⟨y, am, h⟩,
+  rw h,
+  use [range y, countable_range _],
+  rw (has_basis_infi_principal _ _).eq_generate,
+  { simp [range] },
+  { apply directed_of_mono, apply am },
+  { use 0 },
+end
+
+lemma is_countably_generated_of_seq {f : filter α} (h : ∃ x : ℕ → set α, f = ⨅ i, principal $ x i) :
+  f.is_countably_generated  :=
+let ⟨x, h⟩ := h in by rw h ; apply is_countably_generated_seq
+
+lemma is_countably_generated_binfi_principal {B : set $ set α} (h : countable B) :
+  is_countably_generated (⨅ (s ∈ B), principal s) :=
+is_countably_generated_of_seq (countable_binfi_principal_eq_seq_infi h)
+
+lemma is_countably_generated_iff_exists_antimono_basis {f : filter α} : is_countably_generated f ↔
+  ∃ x : ℕ → set α, f.has_antimono_basis (λ _, true) x :=
+begin
+  split,
+  { intro h,
+    exact h.has_antimono_basis },
+  { rintros ⟨x, h⟩,
+    rw h.to_has_basis.eq_infi,
+    exact is_countably_generated_seq x },
+end
+
+namespace is_countably_generated
+
+lemma exists_antimono_seq' {f : filter α} (cblb : f.is_countably_generated) :
+  ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ ∀ {s}, (s ∈ f ↔ ∃ i, x i ⊆ s) :=
+let ⟨x, hx⟩ := is_countably_generated_iff_exists_antimono_basis.mp cblb in
+⟨x, λ i j, hx.decreasing trivial trivial, λ s, by simp [hx.to_has_basis.mem_iff]⟩
+
+protected lemma comap {l : filter β} (h : l.is_countably_generated) (f : α → β) :
+  (comap f l).is_countably_generated :=
+begin
+  rcases h.exists_seq with ⟨x, hx⟩,
+  apply is_countably_generated_of_seq,
+  use λ i, f ⁻¹' x i,
+  calc
+    comap f l = comap f (⨅ i, principal (x i))   : by rw hx
+          ... = (⨅ i, comap f $ principal $ x i) : comap_infi
+          ... = (⨅ i, principal $ f ⁻¹' x i)     : by simp_rw comap_principal,
+end
+
+/-- An abstract version of continuity of sequentially continuous functions on metric spaces:
+if a filter `k` is countably generated then `tendsto f k l` iff for every sequence `u`
+converging to `k`, `f ∘ u` tends to `l`. -/
+lemma tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
+  (hcb : k.is_countably_generated) :
+  tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) :=
+suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l,
+  from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩,
+begin
+  rcases hcb.exists_antimono_seq with ⟨g, gmon, gbasis⟩,
+  have gbasis : ∀ A, A ∈ k ↔ ∃ i, g i ⊆ A,
+  { intro A,
+    subst gbasis,
+    rw mem_infi,
+    { simp only [set.mem_Union, iff_self, filter.mem_principal_sets] },
+    { exact directed_of_mono _ (λ i j h, principal_mono.mpr $ gmon _ _ h) },
+    { apply_instance } },
+  classical, contrapose,
+  simp only [not_forall, not_imp, not_exists, subset_def, @tendsto_def _ _ f, gbasis],
+  rintro ⟨B, hBl, hfBk⟩,
+  choose x h using hfBk,
+  use x, split,
+  { simp only [tendsto_at_top', gbasis],
+    rintros A ⟨i, hgiA⟩,
+    use i,
+    refine (λ j hj, hgiA $ gmon _ _ hj _),
+    simp only [h] },
+  { simp only [tendsto_at_top', (∘), not_forall, not_exists],
+    use [B, hBl],
+    intro i, use [i, (le_refl _)],
+    apply (h i).right },
+end
+
+lemma tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
+  (hcb : k.is_countably_generated) :
+  (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l :=
+hcb.tendsto_iff_seq_tendsto.2
+
+end is_countably_generated
+
+-- TODO : prove this for a encodable type
+lemma is_countably_generated_at_top_finset_nat : (at_top : filter $ finset ℕ).is_countably_generated :=
+begin
+  apply is_countably_generated_of_seq,
+  use λ N, Ici (finset.range N),
+  apply eq_infi_of_mem_sets_iff_exists_mem,
+  assume s,
+  rw mem_at_top_sets,
+  refine ⟨_, λ ⟨N, hN⟩, ⟨finset.range N, hN⟩⟩,
+  rintros ⟨t, ht⟩,
+  rcases mem_at_top_sets.1 (tendsto_finset_range (mem_at_top t)) with ⟨N, hN⟩,
+  simp only [preimage, mem_set_of_eq] at hN,
+  exact ⟨N, mem_principal_sets.2 $ λ t' ht', ht t' $ le_trans (hN _ $ le_refl N) ht'⟩
+end
 end filter
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
index 46df0c3b8b266..32e355c070a14 100644
--- a/src/order/filter/basic.lean
+++ b/src/order/filter/basic.lean
@@ -10,52 +10,77 @@ import data.set.finite
 
 ## Main definitions
 
-* `filter` : filter on a set;
+* `filter` : filters on a set;
 * `at_top`, `at_bot`, `cofinite`, `principal` : specific filters;
-* `map`, `comap`, `join` : operations on filters;
-* `filter_upwards [h₁, ..., hₙ]` : takes a list of proofs `hᵢ : sᵢ ∈ f`, and replaces a goal `s ∈ f`
-  with `∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s`;
+* `map`, `comap`, `prod` : operations on filters;
+* `tendsto` : limit with respect to filters;
 * `eventually` : `f.eventually p` means `{x | p x} ∈ f`;
 * `frequently` : `f.frequently p` means `{x | ¬p x} ∉ f`.
+* `filter_upwards [h₁, ..., hₙ]` : takes a list of proofs `hᵢ : sᵢ ∈ f`, and replaces a goal `s ∈ f`
+  with `∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s`;
+
+Filters on a type `X` are sets of sets of `X` satisfying three conditions. They are mostly used to
+abstract two related kinds of ideas:
+* *limits*, including finite or infinite limits of sequences, finite or infinite limits of functions
+  at a point or at infinity, etc...
+* *things happening eventually*, including things happening for large enough `n : ℕ`, or near enough
+  a point `x`, or for close enough pairs of points, or things happening almost everywhere in the
+  sense of measure theory. Dually, filters can also express the idea of *things happening often*:
+  for arbitrarily large `n`, or at a point in any neighborhood of given a point etc...
+
+In this file, we define the type `filter X` of filters on `X`, and endow it with a complete lattice
+structure. This structure is lifted from the lattice structure on `set (set X)` using the Galois
+insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to
+the smallest filter containing it in the other direction.
+We also prove `filter` is a monadic functor, with a push-forward operation
+`filter.map` and a pull-back operation `filter.comap` that form a Galois connections for the
+order on filters.
+Finally we describe a product operation `filter X → filter Y → filter (X × Y)`.
+
+The examples of filters appearing in the description of the two motivating ideas are:
+* `(at_top : filter ℕ)` : made of sets of `ℕ` containing `{n | n ≥ N}` for some `N`
+* `𝓝 x` : made of neighborhoods of `x` in a topological space (defined in topology.basic)
+* `𝓤 X` : made of entourages of a uniform space (those space are generalizations of metric spaces
+  defined in topology.uniform_space.basic)
+* `μ.a_e` : made of sets whose complement has zero measure with respect to `μ` (defined in
+  measure_theory.measure_space)
+
+The general notion of limit of a map with respect to filters on the source and target types
+is `filter.tendsto`. It is defined in terms of the order and the push-forward operation.
+The predicate "happening eventually" is `filter.eventually`, and "happening often" is
+`filter.frequently`, whose definitions are immediate after `filter` is defined (but they come
+rather late in this file in order to immediately relate them to the lattice structure).
+
+For instance, anticipating on topology.basic, the statement: "if a sequence `u` converges to
+some `x` and `u n` belongs to a set `M` for `n` large enough then `x` is in the closure of
+`M`" is formalized as: `tendsto u at_top (𝓝 x) → (∀ᶠ n in at_top, u n ∈ M) → x ∈ closure M`,
+which is a special case of `mem_closure_of_tendsto` from topology.basic.
 
 ## Notations
 
 * `∀ᶠ x in f, p x` : `f.eventually p`;
 * `∃ᶠ x in f, p x` : `f.frequently p`.
 * `f ×ᶠ g` : `filter.prod f g`, localized in `filter`.
+
+## References
+
+*  [N. Bourbaki, *General Topology*][bourbaki1966]
+
+Important note: Bourbaki requires that a filter on `X` cannot contain all sets of `X`, which
+we do *not* require. This gives `filter X` better formal properties, in particular a bottom element
+`⊥` for its lattice structure, at the cost of including the assumption
+`f ≠ ⊥` in a number of lemmas and definitions.
 -/
+
 open set
 
 universes u v w x y
 
 open_locale classical
 
-section order
-variables {α : Type u} (r : α → α → Prop)
-local infix ` ≼ ` : 50 := r
-
-lemma directed_on_Union {r} {ι : Sort v} {f : ι → set α} (hd : directed (⊆) f)
-  (h : ∀x, directed_on r (f x)) : directed_on r (⋃x, f x) :=
-by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact
-assume a₁ b₁ fb₁ a₂ b₂ fb₂,
-let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂,
-    ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in
-⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
-
-end order
-
-theorem directed_of_chain {α β r} [is_refl β r] {f : α → β} {c : set α}
-  (h : zorn.chain (f ⁻¹'o r) c) :
-  directed r (λx:{a:α // a ∈ c}, f (x.val)) :=
-assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases
-  (assume : a = b, by simp only [this, exists_prop, and_self, subtype.exists];
-    exact ⟨b, hb, refl _⟩)
-  (assume : a ≠ b, (h a ha b hb this).elim
-    (λ h : r (f a) (f b), ⟨⟨b, hb⟩, h, refl _⟩)
-    (λ h : r (f b) (f a), ⟨⟨a, ha⟩, refl _, h⟩))
-
 /-- A filter `F` on a type `α` is a collection of sets of `α` which contains the whole `α`,
-is upwards-closed, and is stable under intersection, -/
+is upwards-closed, and is stable under intersection. We do not forbid this collection to be
+all sets of `α`. -/
 structure filter (α : Type*) :=
 (sets                   : set (set α))
 (univ_sets              : set.univ ∈ sets)
@@ -110,6 +135,10 @@ finite.induction_on hf
     have h₂ : (⋂x∈is, s x) ∈ f, from hi $ assume a ha, hs _ $ by simp only [ha, mem_insert_iff, or_true],
     by simp [inter_mem_sets h₁ h₂])
 
+lemma sInter_mem_sets_of_finite {s : set (set α)} (hfin : finite s) (h_in : ∀ U ∈ s, U ∈ f) :
+  ⋂₀ s ∈ f :=
+by { rw sInter_eq_bInter, exact Inter_mem_sets hfin h_in }
+
 lemma Inter_mem_sets_of_fintype {β : Type v} {s : β → set α} [fintype β] (h : ∀i, s i ∈ f) :
   (⋂i, s i) ∈ f :=
 by simpa using Inter_mem_sets finite_univ (λi hi, h i)
@@ -211,6 +240,37 @@ iff.intro
     (assume x y _ hxy hx, mem_sets_of_superset hx hxy)
     (assume x y _ _ hx hy, inter_mem_sets hx hy))
 
+
+lemma mem_generate_iff (s : set $ set α) {U : set α} : U ∈ generate s ↔ ∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U :=
+begin
+  split ; intro h,
+  { induction h with V V_in V W V_in hVW hV V W V_in W_in hV hW,
+    { use {V},
+      simp [V_in] },
+    { use ∅,
+      simp [subset.refl, univ] },
+    { rcases hV with ⟨t, hts, htfin, hinter⟩,
+      exact ⟨t, hts, htfin, subset.trans hinter hVW⟩ },
+    { rcases hV with ⟨t, hts, htfin, htinter⟩,
+      rcases hW with ⟨z, hzs, hzfin, hzinter⟩,
+      refine ⟨t ∪ z, union_subset hts hzs, finite_union htfin hzfin, _⟩,
+      rw sInter_union,
+      exact inter_subset_inter htinter hzinter } },
+  { rcases h with ⟨t, ts, tfin, h⟩,
+    apply generate_sets.superset _ h,
+    revert ts,
+    apply finite.induction_on tfin,
+    { intro h,
+      rw sInter_empty,
+      exact generate_sets.univ },
+    { intros V r hV rfin hinter h,
+      cases insert_subset.mp h with V_in r_sub,
+      rw [insert_eq V r, sInter_union],
+      apply generate_sets.inter _ (hinter r_sub),
+      rw sInter_singleton,
+      exact generate_sets.basic V_in } },
+end
+
 /-- `mk_of_closure s hs` constructs a filter on `α` whose elements set is exactly
 `s : set (set α)`, provided one gives the assumption `hs : (generate s).sets = s`. -/
 protected def mk_of_closure (s : set (set α)) (hs : (generate s).sets = s) : filter α :=
@@ -340,6 +400,32 @@ iff.rfl
   x ∈ supr f ↔ (∀i, x ∈ f i) :=
 by simp only [supr_sets_eq, iff_self, mem_Inter]
 
+lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s i).sets) :=
+show generate _ = generate _, from congr_arg _ supr_range
+
+lemma mem_infi_iff {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔
+  ∃ I : set ι, finite I ∧ ∃ V : {i | i ∈ I} → set α, (∀ i, V i ∈ s i) ∧ (⋂ i, V i) ⊆ U :=
+begin
+  rw [infi_eq_generate, mem_generate_iff],
+  split,
+  { rintro ⟨t, tsub, tfin, tinter⟩,
+    rcases eq_finite_Union_of_finite_subset_Union tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩,
+    rw sInter_Union at tinter,
+    let V := λ i, ⋂₀ σ i,
+    have V_in : ∀ i, V i ∈ s i,
+    { rintro ⟨i, i_in⟩,
+      apply sInter_mem_sets_of_finite (σfin _),
+      apply σsub },
+    exact ⟨I, Ifin, V, V_in, tinter⟩ },
+  { rintro ⟨I, Ifin, V, V_in, h⟩,
+    refine ⟨range V, _, _, h⟩,
+    { rintro _ ⟨i, rfl⟩,
+      rw mem_Union,
+      use [i, V_in i] },
+    { haveI : fintype {i : ι | i ∈ I} := finite.fintype Ifin,
+      exact finite_range _ } },
+end
+
 @[simp] lemma le_principal_iff {s : set α} {f : filter α} : f ≤ principal s ↔ s ∈ f :=
 show (∀{t}, s ⊆ t → t ∈ f) ↔ s ∈ f,
   from ⟨assume h, h (subset.refl s), assume hs t ht, mem_sets_of_superset hs ht⟩
@@ -355,6 +441,12 @@ by simp only [le_antisymm_iff, le_principal_iff, mem_principal_sets]; refl
 
 @[simp] lemma join_principal_eq_Sup {s : set (filter α)} : join (principal s) = Sup s := rfl
 
+lemma principal_univ : principal (univ : set α) = ⊤ :=
+top_unique $ by simp only [le_principal_iff, mem_top_sets, eq_self_iff_true]
+
+lemma principal_empty : principal (∅ : set α) = ⊥ :=
+bot_unique $ assume s _, empty_subset _
+
 /-! ### Lattice equations -/
 
 lemma empty_in_sets_eq_bot {f : filter α} : ∅ ∈ f ↔ f = ⊥ :=
@@ -532,6 +624,118 @@ begin
     exact ⟨p a, hpa, (s.inf p), ⟨⟨p, hp, le_refl _⟩, ht⟩⟩ }
 end
 
+/-- If `f : ι → filter α` is directed, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`.
+See also `infi_ne_bot_of_directed` for a version assuming `nonempty α` instead of `nonempty ι`. -/
+lemma infi_ne_bot_of_directed' {f : ι → filter α} (hn : nonempty ι)
+  (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ :=
+begin
+  intro h,
+  have he: ∅  ∈ (infi f), from h.symm ▸ (mem_bot_sets : ∅ ∈ (⊥ : filter α)),
+  obtain ⟨i, hi⟩ : ∃i, ∅ ∈ f i,
+    from (mem_infi hd hn ∅).1 he,
+  exact hb i (empty_in_sets_eq_bot.1 hi)
+end
+
+/-- If `f : ι → filter α` is directed, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`.
+See also `infi_ne_bot_of_directed'` for a version assuming `nonempty ι` instead of `nonempty α`. -/
+lemma infi_ne_bot_of_directed {f : ι → filter α}
+  (hn : nonempty α) (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ :=
+if hι : nonempty ι then infi_ne_bot_of_directed' hι hd hb else
+assume h : infi f = ⊥,
+have univ ⊆ (∅ : set α),
+begin
+  rw [←principal_mono, principal_univ, principal_empty, ←h],
+  exact (le_infi $ assume i, false.elim $ hι ⟨i⟩)
+end,
+let ⟨x⟩ := hn in this (mem_univ x)
+
+lemma infi_ne_bot_iff_of_directed' {f : ι → filter α}
+  (hn : nonempty ι) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) :=
+⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i),
+  infi_ne_bot_of_directed' hn hd⟩
+
+lemma infi_ne_bot_iff_of_directed {f : ι → filter α}
+  (hn : nonempty α) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) :=
+⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i),
+  infi_ne_bot_of_directed hn hd⟩
+
+lemma mem_infi_sets {f : ι → filter α} (i : ι) : ∀{s}, s ∈ f i → s ∈ ⨅i, f i :=
+show (⨅i, f i) ≤ f i, from infi_le _ _
+
+@[elab_as_eliminator]
+lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop}
+  (uni : p univ)
+  (ins : ∀{i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂))
+  (upw : ∀{s₁ s₂}, s₁ ⊆ s₂ → p s₁ → p s₂) : p s :=
+begin
+  rw [mem_infi_finite] at hs,
+  simp only [mem_Union, (finset.inf_eq_infi _ _).symm] at hs,
+  rcases hs with ⟨is, his⟩,
+  revert s,
+  refine finset.induction_on is _ _,
+  { assume s hs, rwa [mem_top_sets.1 hs] },
+  { rintros ⟨i⟩ js his ih s hs,
+    rw [finset.inf_insert, mem_inf_sets] at hs,
+    rcases hs with ⟨s₁, hs₁, s₂, hs₂, hs⟩,
+    exact upw hs (ins hs₁ (ih hs₂)) }
+end
+
+/- principal equations -/
+
+@[simp] lemma inf_principal {s t : set α} : principal s ⊓ principal t = principal (s ∩ t) :=
+le_antisymm
+  (by simp; exact ⟨s, subset.refl s, t, subset.refl t, by simp⟩)
+  (by simp [le_inf_iff, inter_subset_left, inter_subset_right])
+
+@[simp] lemma sup_principal {s t : set α} : principal s ⊔ principal t = principal (s ∪ t) :=
+filter_eq $ set.ext $
+  by simp only [union_subset_iff, union_subset_iff, mem_sup_sets, forall_const, iff_self, mem_principal_sets]
+
+@[simp] lemma supr_principal {ι : Sort w} {s : ι → set α} : (⨆x, principal (s x)) = principal (⋃i, s i) :=
+filter_eq $ set.ext $ assume x, by simp only [supr_sets_eq, mem_principal_sets, mem_Inter];
+exact (@supr_le_iff (set α) _ _ _ _).symm
+
+@[simp] lemma principal_eq_bot_iff {s : set α} : principal s = ⊥ ↔ s = ∅ :=
+empty_in_sets_eq_bot.symm.trans $ mem_principal_sets.trans subset_empty_iff
+
+lemma principal_ne_bot_iff {s : set α} : principal s ≠ ⊥ ↔ s.nonempty :=
+(not_congr principal_eq_bot_iff).trans ne_empty_iff_nonempty
+
+lemma inf_principal_eq_bot {f : filter α} {s : set α} (hs : -s ∈ f) : f ⊓ principal s = ⊥ :=
+empty_in_sets_eq_bot.mp ⟨_, hs, s, mem_principal_self s, assume x ⟨h₁, h₂⟩, h₁ h₂⟩
+
+theorem mem_inf_principal (f : filter α) (s t : set α) :
+  s ∈ f ⊓ principal t ↔ {x | x ∈ t → x ∈ s} ∈ f :=
+begin
+  simp only [mem_inf_sets, mem_principal_sets, exists_prop], split,
+  { rintros ⟨u, ul, v, tsubv, uvinter⟩,
+    apply filter.mem_sets_of_superset ul,
+    intros x xu xt, exact uvinter ⟨xu, tsubv xt⟩ },
+  intro h, refine ⟨_, h, t, set.subset.refl t, _⟩,
+  rintros x ⟨hx, xt⟩,
+  exact hx xt
+end
+
+@[simp] lemma infi_principal_finset {ι : Type w} (s : finset ι) (f : ι → set α) :
+  (⨅i∈s, principal (f i)) = principal (⋂i∈s, f i) :=
+begin
+  ext t,
+  simp [mem_infi_sets_finset],
+  split,
+  { rintros ⟨p, hp, ht⟩,
+    calc (⋂ (i : ι) (H : i ∈ s), f i) ≤ (⋂ (i : ι) (H : i ∈ s), p i) :
+      infi_le_infi (λi, infi_le_infi (λhi, mem_principal_sets.1 (hp i hi)))
+    ... ≤ t : ht },
+  { assume h,
+    exact ⟨f, λi hi, subset.refl _, h⟩ }
+end
+
+@[simp] lemma infi_principal_fintype {ι : Type w} [fintype ι] (f : ι → set α) :
+  (⨅i, principal (f i)) = principal (⋂i, f i) :=
+by simpa using infi_principal_finset finset.univ f
+
+end lattice
+
 /-! ### Eventually -/
 
 /-- `f.eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in at_top, p x`
@@ -777,67 +981,7 @@ lemma frequently_supr {p : α → Prop} {fs : β → filter α} :
   (∃ᶠ x in (⨆ b, fs b), p x) ↔ (∃ b, ∃ᶠ x in fs b, p x) :=
 by simp [filter.frequently, -not_eventually, not_forall]
 
-/- principal equations -/
-
-@[simp] lemma inf_principal {s t : set α} : principal s ⊓ principal t = principal (s ∩ t) :=
-le_antisymm
-  (by simp; exact ⟨s, subset.refl s, t, subset.refl t, by simp⟩)
-  (by simp [le_inf_iff, inter_subset_left, inter_subset_right])
-
-@[simp] lemma sup_principal {s t : set α} : principal s ⊔ principal t = principal (s ∪ t) :=
-filter_eq $ set.ext $
-  by simp only [union_subset_iff, union_subset_iff, mem_sup_sets, forall_const, iff_self, mem_principal_sets]
-
-@[simp] lemma supr_principal {ι : Sort w} {s : ι → set α} : (⨆x, principal (s x)) = principal (⋃i, s i) :=
-filter_eq $ set.ext $ assume x, by simp only [supr_sets_eq, mem_principal_sets, mem_Inter];
-exact (@supr_le_iff (set α) _ _ _ _).symm
-
-lemma principal_univ : principal (univ : set α) = ⊤ :=
-top_unique $ by simp only [le_principal_iff, mem_top_sets, eq_self_iff_true]
-
-lemma principal_empty : principal (∅ : set α) = ⊥ :=
-bot_unique $ assume s _, empty_subset _
-
-@[simp] lemma principal_eq_bot_iff {s : set α} : principal s = ⊥ ↔ s = ∅ :=
-empty_in_sets_eq_bot.symm.trans $ mem_principal_sets.trans subset_empty_iff
-
-lemma principal_ne_bot_iff {s : set α} : principal s ≠ ⊥ ↔ s.nonempty :=
-(not_congr principal_eq_bot_iff).trans ne_empty_iff_nonempty
-
-lemma inf_principal_eq_bot {f : filter α} {s : set α} (hs : -s ∈ f) : f ⊓ principal s = ⊥ :=
-empty_in_sets_eq_bot.mp ⟨_, hs, s, mem_principal_self s, assume x ⟨h₁, h₂⟩, h₁ h₂⟩
-
-theorem mem_inf_principal (f : filter α) (s t : set α) :
-  s ∈ f ⊓ principal t ↔ { x | x ∈ t → x ∈ s } ∈ f :=
-begin
-  simp only [mem_inf_sets, mem_principal_sets, exists_prop], split,
-  { rintros ⟨u, ul, v, tsubv, uvinter⟩,
-    apply filter.mem_sets_of_superset ul,
-    intros x xu xt, exact uvinter ⟨xu, tsubv xt⟩ },
-  intro h, refine ⟨_, h, t, set.subset.refl t, _⟩,
-  rintros x ⟨hx, xt⟩,
-  exact hx xt
-end
-
-@[simp] lemma infi_principal_finset {ι : Type w} (s : finset ι) (f : ι → set α) :
-  (⨅i∈s, principal (f i)) = principal (⋂i∈s, f i) :=
-begin
-  ext t,
-  simp [mem_infi_sets_finset],
-  split,
-  { rintros ⟨p, hp, ht⟩,
-    calc (⋂ (i : ι) (H : i ∈ s), f i) ≤ (⋂ (i : ι) (H : i ∈ s), p i) :
-      infi_le_infi (λi, infi_le_infi (λhi, mem_principal_sets.1 (hp i hi)))
-    ... ≤ t : ht },
-  { assume h,
-    exact ⟨f, λi hi, subset.refl _, h⟩ }
-end
-
-@[simp] lemma infi_principal_fintype {ι : Type w} [fintype ι] (f : ι → set α) :
-  (⨅i, principal (f i)) = principal (⋂i, f i) :=
-by simpa using infi_principal_finset finset.univ f
-
-end lattice
+/-! ### Push-forwards, pull-backs, and the monad structure -/
 
 section map
 
@@ -918,25 +1062,6 @@ end
 
 end comap
 
-/-- The cofinite filter is the filter of subsets whose complements are finite. -/
-def cofinite : filter α :=
-{ sets             := {s | finite (- s)},
-  univ_sets        := by simp only [compl_univ, finite_empty, mem_set_of_eq],
-  sets_of_superset := assume s t (hs : finite (-s)) (st: s ⊆ t),
-    finite_subset hs $ compl_subset_compl.2 st,
-  inter_sets       := assume s t (hs : finite (-s)) (ht : finite (-t)),
-    by simp only [compl_inter, finite_union, ht, hs, mem_set_of_eq] }
-
-@[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite (-s) := iff.rfl
-
-lemma cofinite_ne_bot [infinite α] : @cofinite α ≠ ⊥ :=
-mt empty_in_sets_eq_bot.mpr $ by { simp only [mem_cofinite, compl_empty], exact infinite_univ }
-
-lemma frequently_cofinite_iff_infinite {p : α → Prop} :
-  (∃ᶠ x in cofinite, p x) ↔ set.infinite {x | p x} :=
-by simp only [filter.frequently, filter.eventually, mem_cofinite, compl_set_of, not_not,
-  set.infinite]
-
 /-- The monadic bind operation on filter is defined the usual way in terms of `map` and `join`.
 
 Unfortunately, this `bind` does not result in the expected applicative. See `filter.seq` for the
@@ -1432,63 +1557,46 @@ show join (map f (principal s)) = (⨆x ∈ s, f x),
 
 end bind
 
-/-- If `f : ι → filter α` is derected, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`.
-See also `infi_ne_bot_of_directed` for a version assuming `nonempty α` instead of `nonempty ι`. -/
-lemma infi_ne_bot_of_directed' {f : ι → filter α} (hn : nonempty ι)
-  (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ :=
-begin
-  intro h,
-  have he: ∅  ∈ (infi f), from h.symm ▸ (mem_bot_sets : ∅ ∈ (⊥ : filter α)),
-  obtain ⟨i, hi⟩ : ∃i, ∅ ∈ f i,
-    from (mem_infi hd hn ∅).1 he,
-  exact hb i (empty_in_sets_eq_bot.1 hi)
-end
+section list_traverse
+/- This is a separate section in order to open `list`, but mostly because of universe
+   equality requirements in `traverse` -/
 
-/-- If `f : ι → filter α` is derected, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`.
-See also `infi_ne_bot_of_directed'` for a version assuming `nonempty ι` instead of `nonempty α`. -/
-lemma infi_ne_bot_of_directed {f : ι → filter α}
-  (hn : nonempty α) (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ :=
-if hι : nonempty ι then infi_ne_bot_of_directed' hι hd hb else
-assume h : infi f = ⊥,
-have univ ⊆ (∅ : set α),
-begin
-  rw [←principal_mono, principal_univ, principal_empty, ←h],
-  exact (le_infi $ assume i, false.elim $ hι ⟨i⟩)
-end,
-let ⟨x⟩ := hn in this (mem_univ x)
+open list
 
-lemma infi_ne_bot_iff_of_directed' {f : ι → filter α}
-  (hn : nonempty ι) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) :=
-⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i),
-  infi_ne_bot_of_directed' hn hd⟩
+lemma sequence_mono :
+  ∀(as bs : list (filter α)), forall₂ (≤) as bs → sequence as ≤ sequence bs
+| []      []      forall₂.nil         := le_refl _
+| (a::as) (b::bs) (forall₂.cons h hs) := seq_mono (map_mono h) (sequence_mono as bs hs)
 
-lemma infi_ne_bot_iff_of_directed {f : ι → filter α}
-  (hn : nonempty α) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) :=
-⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i),
-  infi_ne_bot_of_directed hn hd⟩
+variables {α' β' γ' : Type u} {f : β' → filter α'} {s : γ' → set α'}
 
-lemma mem_infi_sets {f : ι → filter α} (i : ι) : ∀{s}, s ∈ f i → s ∈ ⨅i, f i :=
-show (⨅i, f i) ≤ f i, from infi_le _ _
+lemma mem_traverse_sets :
+  ∀(fs : list β') (us : list γ'),
+    forall₂ (λb c, s c ∈ f b) fs us → traverse s us ∈ traverse f fs
+| []      []      forall₂.nil         := mem_pure_sets.2 $ mem_singleton _
+| (f::fs) (u::us) (forall₂.cons h hs) := seq_mem_seq_sets (image_mem_map h) (mem_traverse_sets fs us hs)
 
-@[elab_as_eliminator]
-lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop}
-  (uni : p univ)
-  (ins : ∀{i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂))
-  (upw : ∀{s₁ s₂}, s₁ ⊆ s₂ → p s₁ → p s₂) : p s :=
+lemma mem_traverse_sets_iff (fs : list β') (t : set (list α')) :
+  t ∈ traverse f fs ↔
+    (∃us:list (set α'), forall₂ (λb (s : set α'), s ∈ f b) fs us ∧ sequence us ⊆ t) :=
 begin
-  rw [mem_infi_finite] at hs,
-  simp only [mem_Union, (finset.inf_eq_infi _ _).symm] at hs,
-  rcases hs with ⟨is, his⟩,
-  revert s,
-  refine finset.induction_on is _ _,
-  { assume s hs, rwa [mem_top_sets.1 hs] },
-  { rintros ⟨i⟩ js his ih s hs,
-    rw [finset.inf_insert, mem_inf_sets] at hs,
-    rcases hs with ⟨s₁, hs₁, s₂, hs₂, hs⟩,
-    exact upw hs (ins hs₁ (ih hs₂)) }
+  split,
+  { induction fs generalizing t,
+    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⟩,
+      rcases mem_map_sets_iff.1 hu with ⟨w, hw, hwu⟩,
+      rcases ih v hv with ⟨us, hus, hu⟩,
+      exact ⟨w :: us, forall₂.cons hw hus, subset.trans (set.seq_mono hwu hu) ht⟩ } },
+  { rintros ⟨us, hus, hs⟩,
+    exact mem_sets_of_superset (mem_traverse_sets _ _ hus) hs }
 end
 
-/- tendsto -/
+end list_traverse
+
+/-! ### Limits -/
 
 /-- `tendsto` is the generic "limit of a function" predicate.
   `tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
@@ -1641,6 +1749,7 @@ begin
   rw if_neg h, exact hp₁ h
 end
 
+/-! ### Products of filters -/
 
 section prod
 variables {s : set α} {t : set β} {f : filter α} {g : filter β}
@@ -1791,7 +1900,7 @@ by simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff
 
 end prod
 
-/- at_top and at_bot -/
+/-! ### at_top and at_bot filters on preorded sets, monoids and groups. -/
 
 /-- `at_top` is the filter representing the limit `→ ∞` on an ordered set.
   It is generated by the collection of up-sets `{b | a ≤ b}`.
@@ -1879,6 +1988,11 @@ lemma tendsto_at_top_mono [preorder β] (l : filter α) :
   monotone (λ f : α → β, tendsto f l at_top) :=
 λ f₁ f₂ h, tendsto_at_top_mono' l $ univ_mem_sets' h
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma map_at_top_inf_ne_bot_iff [semilattice_sup α] [nonempty α] {F : filter β} {u : α → β} :
+  (map u at_top) ⊓ F ≠ ⊥ ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U :=
+by simp_rw [inf_ne_bot_iff_frequently_right, frequently_map, frequently_at_top] ; trivial
+
 section ordered_add_monoid
 
 variables [ordered_cancel_add_comm_monoid β] (l : filter α) {f g : α → β}
@@ -2083,7 +2197,51 @@ map_at_top_eq_of_gc (λb, b * k + (k - 1)) 1
     calc b = (b * k) / k : by rw [nat.mul_div_cancel b hk]
       ... ≤ (b * k + (k - 1)) / k : nat.div_le_div_right $ nat.le_add_right _ _)
 
-/- ultrafilter -/
+/-! ### The cofinite filter -/
+
+/-- The cofinite filter is the filter of subsets whose complements are finite. -/
+def cofinite : filter α :=
+{ sets             := {s | finite (- s)},
+  univ_sets        := by simp only [compl_univ, finite_empty, mem_set_of_eq],
+  sets_of_superset := assume s t (hs : finite (-s)) (st: s ⊆ t),
+    finite_subset hs $ compl_subset_compl.2 st,
+  inter_sets       := assume s t (hs : finite (-s)) (ht : finite (-t)),
+    by simp only [compl_inter, finite_union, ht, hs, mem_set_of_eq] }
+
+@[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite (-s) := iff.rfl
+
+lemma cofinite_ne_bot [infinite α] : @cofinite α ≠ ⊥ :=
+mt empty_in_sets_eq_bot.mpr $ by { simp only [mem_cofinite, compl_empty], exact infinite_univ }
+
+lemma frequently_cofinite_iff_infinite {p : α → Prop} :
+  (∃ᶠ x in cofinite, p x) ↔ set.infinite {x | p x} :=
+by simp only [filter.frequently, filter.eventually, mem_cofinite, compl_set_of, not_not,
+  set.infinite]
+
+lemma set.infinite_iff_frequently_cofinite {α : Type u} {s : set α} :
+  set.infinite s ↔ (∃ᶠ x in cofinite, x ∈ s) :=
+frequently_cofinite_iff_infinite.symm
+
+/-- For natural numbers the filters `cofinite` and `at_top` coincide. -/
+lemma nat.cofinite_eq_at_top : @cofinite ℕ = at_top :=
+begin
+  ext s,
+  simp only [mem_cofinite, mem_at_top_sets],
+  split,
+  { assume hs,
+    use (hs.to_finset.sup id) + 1,
+    assume b hb,
+    by_contradiction hbs,
+    have := hs.to_finset.subset_range_sup_succ (finite.mem_to_finset.2 hbs),
+    exact not_lt_of_le hb (finset.mem_range.1 this) },
+  { rintros ⟨N, hN⟩,
+    apply finite_subset (finite_lt_nat N),
+    assume n hn,
+    change n < N,
+    exact lt_of_not_ge (λ hn', hn $ hN n hn') }
+end
+
+/-! ### Ultrafilters -/
 
 section ultrafilter
 open zorn
@@ -2314,63 +2472,3 @@ lemma exists_ultrafilter_iff (f : filter α) : (∃ (u : ultrafilter α), u.val
 end ultrafilter
 
 end filter
-
-namespace filter
-variables {α β γ : Type u} {f : β → filter α} {s : γ → set α}
-open list
-
-lemma mem_traverse_sets :
-  ∀(fs : list β) (us : list γ),
-    forall₂ (λb c, s c ∈ f b) fs us → traverse s us ∈ traverse f fs
-| []      []      forall₂.nil         := mem_pure_sets.2 $ mem_singleton _
-| (f::fs) (u::us) (forall₂.cons h hs) := seq_mem_seq_sets (image_mem_map h) (mem_traverse_sets fs us hs)
-
-lemma mem_traverse_sets_iff (fs : list β) (t : set (list α)) :
-  t ∈ traverse f fs ↔
-    (∃us:list (set α), forall₂ (λb (s : set α), s ∈ f b) fs us ∧ sequence us ⊆ t) :=
-begin
-  split,
-  { induction fs generalizing t,
-    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⟩,
-      rcases mem_map_sets_iff.1 hu with ⟨w, hw, hwu⟩,
-      rcases ih v hv with ⟨us, hus, hu⟩,
-      exact ⟨w :: us, forall₂.cons hw hus, subset.trans (set.seq_mono hwu hu) ht⟩ } },
-  { rintros ⟨us, hus, hs⟩,
-    exact mem_sets_of_superset (mem_traverse_sets _ _ hus) hs }
-end
-
-lemma sequence_mono :
-  ∀(as bs : list (filter α)), forall₂ (≤) as bs → sequence as ≤ sequence bs
-| []      []      forall₂.nil         := le_refl _
-| (a::as) (b::bs) (forall₂.cons h hs) := seq_mono (map_mono h) (sequence_mono as bs hs)
-
-end filter
-
-open filter
-
-lemma set.infinite_iff_frequently_cofinite {α : Type u} {s : set α} :
-  set.infinite s ↔ (∃ᶠ x in cofinite, x ∈ s) :=
-frequently_cofinite_iff_infinite.symm
-
-/-- For natural numbers the filters `cofinite` and `at_top` coincide. -/
-lemma nat.cofinite_eq_at_top : @cofinite ℕ = at_top :=
-begin
-  ext s,
-  simp only [mem_cofinite, mem_at_top_sets],
-  split,
-  { assume hs,
-    use (hs.to_finset.sup id) + 1,
-    assume b hb,
-    by_contradiction hbs,
-    have := hs.to_finset.subset_range_sup_succ (finite.mem_to_finset.2 hbs),
-    exact not_lt_of_le hb (finset.mem_range.1 this) },
-  { rintros ⟨N, hN⟩,
-    apply finite_subset (finite_lt_nat N),
-    assume n hn,
-    change n < N,
-    exact lt_of_not_ge (λ hn', hn $ hN n hn') }
-end
diff --git a/src/order/zorn.lean b/src/order/zorn.lean
index 82591bf9c8b72..4d2c924f2f159 100644
--- a/src/order/zorn.lean
+++ b/src/order/zorn.lean
@@ -287,3 +287,13 @@ theorem chain.image {α β : Type*} (r : α → α → Prop)
     (or.inl ∘ h _ _) (or.inr ∘ h _ _)
 
 end zorn
+
+theorem directed_of_chain {α β r} [is_refl β r] {f : α → β} {c : set α}
+  (h : zorn.chain (f ⁻¹'o r) c) :
+  directed r (λx:{a:α // a ∈ c}, f (x.val)) :=
+assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases
+  (assume : a = b, by simp only [this, exists_prop, and_self, subtype.exists];
+    exact ⟨b, hb, refl _⟩)
+  (assume : a ≠ b, (h a ha b hb this).elim
+    (λ h : r (f a) (f b), ⟨⟨b, hb⟩, h, refl _⟩)
+    (λ h : r (f b) (f a), ⟨⟨a, ha⟩, refl _, h⟩))
diff --git a/src/topology/bases.lean b/src/topology/bases.lean
index a810eb0fc81e6..6ca09b9b86e70 100644
--- a/src/topology/bases.lean
+++ b/src/topology/bases.lean
@@ -6,151 +6,11 @@ Authors: Johannes Hölzl, Mario Carneiro
 Bases of topologies. Countability axioms.
 -/
 
-import topology.constructions data.set.countable
+import topology.constructions order.filter.bases
 
 open set filter classical
 open_locale topological_space
 
-namespace filter
-universes u v
-variables {α : Type u} {β : Type v}
-
-/--
-A filter has a countable basis iff it is generated by a countable collection
-of subsets of α. (A filter is a generated by a collection of sets iff it is
-the infimum of the principal filters.)
-
-Note: we do not require the collection to be closed under finite intersections.
--/
-def has_countable_basis (f : filter α) : Prop :=
-∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t
-
-lemma has_countable_basis_of_seq (f : filter α) (x : ℕ → set α) (h : f = ⨅ i, principal (x i)) :
-  f.has_countable_basis :=
-⟨range x, countable_range _, by rwa infi_range⟩
-
-lemma seq_of_has_countable_basis (f : filter α) (cblb : f.has_countable_basis) :
-    ∃ x : ℕ → set α, f = ⨅ i, principal (x i) :=
-begin
-  rcases cblb with ⟨B, Bcbl, gen⟩, subst gen,
-  cases B.eq_empty_or_nonempty with hB Bnonempty, { use λ n, set.univ, simp [principal_univ, *] },
-  rw countable_iff_exists_surjective_to_subtype Bnonempty at Bcbl,
-  rcases Bcbl with ⟨g, gsurj⟩,
-  rw infi_subtype',
-  use (λ n, g n), apply le_antisymm; rw le_infi_iff,
-  { intro i, apply infi_le_of_le (g i) _, apply le_refl _ },
-  { intros a, rcases gsurj a with i, apply infi_le_of_le i _, subst h, apply le_refl _ }
-end
-
-/--
-Different characterization of countable basis. A filter has a countable basis
-iff it is generated by a sequence of sets.
--/
-lemma has_countable_basis_iff_seq (f : filter α) :
-  f.has_countable_basis ↔
-    ∃ x : ℕ → set α, f = ⨅ i, principal (x i) :=
-⟨seq_of_has_countable_basis _, λ ⟨x, xgen⟩, has_countable_basis_of_seq _ x xgen⟩
-
-lemma mono_seq_of_has_countable_basis (f : filter α) (cblb : f.has_countable_basis) :
-  ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ f = ⨅ i, principal (x i) :=
-begin
-  rcases (seq_of_has_countable_basis f cblb) with ⟨x', hx'⟩,
-  let x := λ n, ⋂ m ≤ n, x' m,
-  use x, split,
-  { intros i j hij a, simp [x], intros h i' hi'i, apply h, transitivity; assumption },
-  subst hx', apply le_antisymm; rw le_infi_iff; intro i,
-  { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _),
-    intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ },
-  { apply infi_le_of_le i _, rw principal_mono, intro a, simp [x], intro h, apply h, refl },
-end
-
-/--
-Different characterization of countable basis. A filter has a countable basis
-iff it is generated by a monotonically decreasing sequence of sets.
--/
-lemma has_countable_basis_iff_mono_seq (f : filter α) :
-  f.has_countable_basis ↔
-    ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ f = ⨅ i, principal (x i) :=
-⟨mono_seq_of_has_countable_basis _, λ ⟨x, _, xgen⟩, has_countable_basis_of_seq _ x xgen⟩
-
-/--
-Different characterization of countable basis. A filter has a countable basis
-iff there exists a monotonically decreasing sequence of sets `x i`
-such that `s ∈ f ↔ ∃ i, x i ⊆ s`. -/
-lemma has_countable_basis_iff_mono_seq' (f : filter α) :
-  f.has_countable_basis ↔
-    ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ (∀ {s}, s ∈ f ↔ ∃ i, x i ⊆ s) :=
-begin
-  refine (has_countable_basis_iff_mono_seq f).trans (exists_congr $ λ x, and_congr_right _),
-  intro hmono,
-  have : directed (≥) (λ i, principal (x i)),
-    from directed_of_mono _ (λ i j hij, principal_mono.2 (hmono _ _ hij)),
-  simp only [filter.ext_iff, mem_infi this ⟨0⟩, mem_Union, mem_principal_sets]
-end
-
-lemma has_countable_basis.comap {l : filter β} (h : has_countable_basis l) (f : α → β) :
-  has_countable_basis (l.comap f) :=
-begin
-  rcases h with ⟨S, h₁, h₂⟩,
-  refine ⟨preimage f '' S, countable_image _ h₁, _⟩,
-  calc comap f l = ⨅ s ∈ S, principal (f ⁻¹' s) : by simp [h₂]
-  ... = ⨅ s ∈ S, ⨅ (t : set α) (H : f ⁻¹' s = t), principal t : by simp
-  ... = ⨅ (t : set α) (s ∈ S) (h₂ : f ⁻¹' s = t), principal t :
-    by { rw [infi_comm], congr' 1, ext t, rw [infi_comm] }
-  ... = _ : by simp [-infi_infi_eq_right, infi_and]
-end
-
--- TODO : prove this for a encodable type
-lemma has_countable_basis_at_top_finset_nat : has_countable_basis (@at_top (finset ℕ) _) :=
-begin
-  refine has_countable_basis_of_seq _ (λN, Ici (finset.range N)) (eq_infi_of_mem_sets_iff_exists_mem _),
-  assume s,
-  rw mem_at_top_sets,
-  refine ⟨_, λ ⟨N, hN⟩, ⟨finset.range N, hN⟩⟩,
-  rintros ⟨t, ht⟩,
-  rcases mem_at_top_sets.1 (tendsto_finset_range (mem_at_top t)) with ⟨N, hN⟩,
-  simp only [preimage, mem_set_of_eq] at hN,
-  exact ⟨N, mem_principal_sets.2 $ λ t' ht', ht t' $ le_trans (hN _ $ le_refl N) ht'⟩
-end
-
-lemma has_countable_basis.tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
-  (hcb : k.has_countable_basis) :
-  tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) :=
-suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l,
-  from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩,
-begin
-  rw filter.has_countable_basis_iff_mono_seq at hcb,
-  rcases hcb with ⟨g, gmon, gbasis⟩,
-  have gbasis : ∀ A, A ∈ k ↔ ∃ i, g i ⊆ A,
-  { intro A,
-    subst gbasis,
-    rw mem_infi,
-    { simp only [set.mem_Union, iff_self, filter.mem_principal_sets] },
-    { exact directed_of_mono _ (λ i j h, principal_mono.mpr $ gmon _ _ h) },
-    { apply_instance } },
-  classical, contrapose,
-  simp only [not_forall, not_imp, not_exists, subset_def, @tendsto_def _ _ f, gbasis],
-  rintro ⟨B, hBl, hfBk⟩,
-  choose x h using hfBk,
-  use x, split,
-  { simp only [tendsto_at_top', gbasis],
-    rintros A ⟨i, hgiA⟩,
-    use i,
-    refine (λ j hj, hgiA $ gmon _ _ hj _),
-    simp only [h] },
-  { simp only [tendsto_at_top', (∘), not_forall, not_exists],
-    use [B, hBl],
-    intro i, use [i, (le_refl _)],
-    apply (h i).right },
-end
-
-lemma has_countable_basis.tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
-  (hcb : k.has_countable_basis) :
-  (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l :=
-hcb.tendsto_iff_seq_tendsto.2
-
-end filter
-
 namespace topological_space
 /- countability axioms
 
@@ -255,7 +115,7 @@ class separable_space : Prop :=
 /-- A first-countable space is one in which every point has a
   countable neighborhood basis. -/
 class first_countable_topology : Prop :=
-(nhds_generated_countable : ∀a:α, (𝓝 a).has_countable_basis)
+(nhds_generated_countable : ∀a:α, (𝓝 a).is_countably_generated)
 
 /-- A second-countable space is one with a countable basis. -/
 class second_countable_topology : Prop :=
@@ -265,8 +125,11 @@ class second_countable_topology : Prop :=
 instance second_countable_topology.to_first_countable_topology
   [second_countable_topology α] : first_countable_topology α :=
 let ⟨b, hb, eq⟩ := second_countable_topology.is_open_generated_countable α in
-⟨assume a, ⟨{s | a ∈ s ∧ s ∈ b},
-  countable_subset (assume x ⟨_, hx⟩, hx) hb, by rw [eq, nhds_generate_from]⟩⟩
+⟨begin
+   intros,
+   rw [eq, nhds_generate_from],
+   exact is_countably_generated_binfi_principal (countable_subset (assume x ⟨_, hx⟩, hx) hb),
+ end⟩
 
 lemma second_countable_topology_induced (β)
   [t : topological_space β] [second_countable_topology β] (f : α → β) :
diff --git a/src/topology/basic.lean b/src/topology/basic.lean
index f649938cab594..371f24725434e 100644
--- a/src/topology/basic.lean
+++ b/src/topology/basic.lean
@@ -525,7 +525,7 @@ theorem mem_closure_iff_nhds_basis {a : α} {p : β → Prop} {s : β → set α
   a ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i :=
 mem_closure_iff_nhds.trans
   ⟨λ H i hi, let ⟨x, hx⟩ := (H _ $ h.mem_of_mem hi) in ⟨x, hx.2, hx.1⟩,
-    λ H t' ht', let ⟨i, hi, hit⟩ := (h t').1 ht', ⟨x, xt, hx⟩ := H i hi in
+    λ H t' ht', let ⟨i, hi, hit⟩ := h.mem_iff.1 ht', ⟨x, xt, hx⟩ := H i hi in
     ⟨x, hit hx, xt⟩⟩
 
 /-- `x` belongs to the closure of `s` if and only if some ultrafilter
diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean
index 0a3c6b24c34ef..f8d76edec792a 100644
--- a/src/topology/continuous_on.lean
+++ b/src/topology/continuous_on.lean
@@ -52,11 +52,11 @@ nhds_within_has_basis (nhds_basis_opens a) t
 
 theorem mem_nhds_within {t : set α} {a : α} {s : set α} :
   t ∈ nhds_within a s ↔ ∃ u, is_open u ∧ a ∈ u ∧ u ∩ s ⊆ t  :=
-by simpa only [exists_prop, and_assoc, and_comm] using nhds_within_basis_open a s t
+by simpa only [exists_prop, and_assoc, and_comm] using (nhds_within_basis_open a s).mem_iff
 
 lemma mem_nhds_within_iff_exists_mem_nhds_inter {t : set α} {a : α} {s : set α} :
   t ∈ nhds_within a s ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t :=
-nhds_within_has_basis (𝓝 a).basis_sets s t
+(nhds_within_has_basis (𝓝 a).basis_sets s).mem_iff
 
 lemma mem_nhds_within_of_mem_nhds {s t : set α} {a : α} (h : s ∈ 𝓝 a) :
   s ∈ nhds_within a t :=
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 9b2d9904744c2..5c8d9554f1044 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -320,7 +320,7 @@ protected theorem mk_uniformity_basis {β : Type*} {p : β → Prop} {f : β →
   (hf₀ : ∀ i, p i → 0 < f i) (hf : ∀ ⦃ε⦄, 0 < ε → ∃ i (hi : p i), f i ≤ ε) :
   (𝓤 α).has_basis p (λ i, {p:α×α | dist p.1 p.2 < f i}) :=
 begin
-  refine λ s, uniformity_basis_dist.mem_iff.trans _,
+  refine ⟨λ s, uniformity_basis_dist.mem_iff.trans _⟩,
   split,
   { rintros ⟨ε, ε₀, hε⟩,
     obtain ⟨i, hi, H⟩ : ∃ i (hi : p i), f i ≤ ε, from hf ε₀,
@@ -348,7 +348,7 @@ protected theorem mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β
   (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x (hx : p x), f x ≤ ε) :
   (𝓤 α).has_basis p (λ x, {p:α×α | dist p.1 p.2 ≤ f x}) :=
 begin
-  refine λ s, uniformity_basis_dist.mem_iff.trans _,
+  refine ⟨λ s, uniformity_basis_dist.mem_iff.trans _⟩,
   split,
   { rintros ⟨ε, ε₀, hε⟩,
     rcases dense ε₀ with ⟨ε', hε'⟩,
@@ -606,7 +606,7 @@ distance coincide. -/
 /-- Expressing the uniformity in terms of `edist` -/
 protected lemma metric.uniformity_basis_edist :
   (𝓤 α).has_basis (λ ε:ennreal, 0 < ε) (λ ε, {p | edist p.1 p.2 < ε}) :=
-begin
+⟨begin
   intro t,
   refine mem_uniformity_dist.trans ⟨_, _⟩; rintro ⟨ε, ε0, Hε⟩,
   { use [ennreal.of_real ε, ennreal.of_real_pos.2 ε0],
@@ -617,7 +617,7 @@ begin
     rw [ennreal.of_real_pos] at ε0',
     refine ⟨ε', ε0', λ a b h, Hε (lt_trans _ hε)⟩,
     rwa [edist_dist, ennreal.of_real_lt_of_real_iff ε0'] }
-end
+end⟩
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem metric.uniformity_edist : 𝓤 α = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
index c8e126652ed16..0ede137586a59 100644
--- a/src/topology/metric_space/emetric_space.lean
+++ b/src/topology/metric_space/emetric_space.lean
@@ -214,7 +214,7 @@ protected theorem emetric.mk_uniformity_basis {β : Type*} {p : β → Prop} {f
   (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x (hx : p x), f x ≤ ε) :
   (𝓤 α).has_basis p (λ x, {p:α×α | edist p.1 p.2 < f x}) :=
 begin
-  refine λ s, uniformity_basis_edist.mem_iff.trans _,
+  refine ⟨λ s, uniformity_basis_edist.mem_iff.trans _⟩,
   split,
   { rintros ⟨ε, ε₀, hε⟩,
     rcases hf ε ε₀ with ⟨i, hi, H⟩,
@@ -230,7 +230,7 @@ protected theorem emetric.mk_uniformity_basis_le {β : Type*} {p : β → Prop}
   (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x (hx : p x), f x ≤ ε) :
   (𝓤 α).has_basis p (λ x, {p:α×α | edist p.1 p.2 ≤ f x}) :=
 begin
-  refine λ s, uniformity_basis_edist.mem_iff.trans _,
+  refine ⟨λ s, uniformity_basis_edist.mem_iff.trans _⟩,
   split,
   { rintros ⟨ε, ε₀, hε⟩,
     rcases dense ε₀ with ⟨ε', hε'⟩,
@@ -274,8 +274,8 @@ mem_uniformity_edist.2 ⟨ε, ε0, λ a b, id⟩
 
 namespace emetric
 
-theorem uniformity_has_countable_basis : has_countable_basis (𝓤 α) :=
-has_countable_basis_of_seq _ _ uniformity_basis_edist_inv_nat.eq_infi
+theorem uniformity_has_countable_basis : is_countably_generated (𝓤 α) :=
+is_countably_generated_of_seq ⟨_, uniformity_basis_edist_inv_nat.eq_infi⟩
 
 /-- ε-δ characterization of uniform continuity on emetric spaces -/
 theorem uniform_continuous_iff [emetric_space β] {f : α → β} :
@@ -574,7 +574,7 @@ nhds_basis_uniformity uniformity_basis_edist
 theorem nhds_eq : 𝓝 x = (⨅ε>0, principal (ball x ε)) :=
 nhds_basis_eball.eq_binfi
 
-theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s := nhds_basis_eball s
+theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s := nhds_basis_eball.mem_iff
 
 theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s :=
 by simp [is_open_iff_nhds, mem_nhds_iff]
diff --git a/src/topology/sequences.lean b/src/topology/sequences.lean
index 3fcaed05ad9ca..ace615504da43 100644
--- a/src/topology/sequences.lean
+++ b/src/topology/sequences.lean
@@ -1,11 +1,12 @@
 /-
 Copyright (c) 2018 Jan-David Salchow. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jan-David Salchow
+Authors: Jan-David Salchow, Patrick Massot
 -/
 
 import topology.basic
 import topology.bases
+import topology.subset_properties
 
 /-!
 # Sequences in topological spaces
@@ -29,15 +30,16 @@ variables {α : Type*} {β : Type*}
 
 local notation f ` ⟶ ` limit := tendsto f at_top (𝓝 limit)
 
-/-! ### Statements about sequences in general topological spaces. -/
+/-! ### Sequential closures, sequential continuity, and sequential spaces. -/
 section topological_space
 variables [topological_space α] [topological_space β]
 
 /-- A sequence converges in the sence of topological spaces iff the associated statement for filter
 holds. -/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma topological_space.seq_tendsto_iff {x : ℕ → α} {limit : α} :
   tendsto x at_top (𝓝 limit) ↔
-    ∀ U : set α, limit ∈ U → is_open U → ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U :=
+    ∀ U : set α, limit ∈ U → is_open U → ∃ N, ∀ n ≥ N, (x n) ∈ U :=
 (at_top_basis.tendsto_iff (nhds_basis_opens limit)).trans $
   by simp only [and_imp, exists_prop, true_and, set.mem_Ici, ge_iff_le, id]
 
@@ -142,39 +144,31 @@ namespace topological_space
 
 namespace first_countable_topology
 
+variables [topological_space α] [first_countable_topology α]
+
 /-- Every first-countable space is sequential. -/
 @[priority 100] -- see Note [lower instance priority]
-instance [topological_space α] [first_countable_topology α] : sequential_space α :=
+instance : sequential_space α :=
 ⟨show ∀ M, sequential_closure M = closure M, from assume M,
   suffices closure M ⊆ sequential_closure M,
     from set.subset.antisymm (sequential_closure_subset_closure M) this,
   -- For every p ∈ closure M, we need to construct a sequence x in M that converges to p:
   assume (p : α) (hp : p ∈ closure M),
-  -- Since we are in a first-countable space, there exists a monotonically decreasing
-  -- sequence g of sets generating the neighborhood filter around p:
-  exists.elim (mono_seq_of_has_countable_basis _
-    (nhds_generated_countable p)) $ assume g ⟨gmon, gbasis⟩,
-  -- (g i) is a neighborhood of p and hence intersects M.
-  -- Via choice we obtain the sequence x such that (x i).val ∈ g i ∩ M:
-  have x : Π i, g i ∩ M,
-  { rw mem_closure_iff_nhds at hp,
-    intro i, apply classical.indefinite_description,
-    apply hp, rw gbasis, rw ← le_principal_iff, apply infi_le_of_le i _, apply le_refl _ },
-  -- It remains to show that x converges to p. Intuitively this is the case
-  -- because x i ∈ g i, and the g i get "arbitrarily small" around p. Formally:
-  have gssnhds : ∀ s ∈ 𝓝 p, ∃ i, g i ⊆ s,
-  { intro s, rw gbasis, rw mem_infi,
-    { simp, intros i hi, use i, assumption },
-    { apply directed_of_mono, intros, apply principal_mono.mpr, apply gmon, assumption },
-    { apply_instance } },
-  -- For the sequence (x i) we can now show that a) it lies in M, and b) converges to p.
-  ⟨λ i, (x i).val, by intro i; simp [(x i).property.right],
-    begin
-      rw tendsto_at_top', intros s nhdss,
-      rcases gssnhds s nhdss with ⟨i, hi⟩,
-      use i, intros j hij, apply hi, apply gmon _ _ hij,
-      simp [(x j).property.left]
-    end⟩⟩
+  -- Since we are in a first-countable space, the neighborhood filter around `p` has a decreasing
+  -- basis `U` indexed by `ℕ`.
+  let ⟨U, hU ⟩ := (nhds_generated_countable p).has_antimono_basis in
+  -- Since `p ∈ closure M`, there is an element in each `M ∩ U i`
+  have hp : ∀ (i : ℕ), ∃ (y : α), y ∈ M ∧ y ∈ U i,
+    by simpa using (mem_closure_iff_nhds_basis hU.1).mp hp,
+  begin
+    -- The axiom of (countable) choice builds our sequence from the later fact
+    choose u hu using hp,
+    rw forall_and_distrib at hu,
+    -- It clearly takes values in `M`
+    use [u, hu.1],
+    -- and converges to `p` because the basis is decreasing.
+    apply hU.tendsto hu.2,
+  end⟩
 
 end first_countable_topology
 
diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean
index 9bb4bc46af601..c8afcb37a398b 100644
--- a/src/topology/uniform_space/cauchy.lean
+++ b/src/topology/uniform_space/cauchy.lean
@@ -484,7 +484,7 @@ namespace uniform_space
 
 open sequentially_complete
 
-variables (H : has_countable_basis (𝓤 α))
+variables (H : is_countably_generated (𝓤 α))
 
 include H
 
@@ -494,7 +494,7 @@ theorem complete_of_convergent_controlled_sequences (U : ℕ → set (α × α))
   (HU : ∀ u : ℕ → α, (∀ N m n, N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, tendsto u at_top (𝓝 a)) :
   complete_space α :=
 begin
-  rcases (𝓤 α).has_countable_basis_iff_mono_seq'.1 H with ⟨U', U'_mono, hU'⟩,
+  rcases H.exists_antimono_seq' with ⟨U', U'_mono, hU'⟩,
   have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α,
     from λ n, inter_mem_sets (U_mem n) (hU'.2 ⟨n, subset.refl _⟩),
   refine ⟨λ f hf, (HU (seq hf Hmem) (λ N m n hm hn, _)).imp $
@@ -509,7 +509,7 @@ complete. -/
 theorem complete_of_cauchy_seq_tendsto
   (H' : ∀ u : ℕ → α, cauchy_seq u → ∃a, tendsto u at_top (𝓝 a)) :
   complete_space α :=
-let ⟨U', U'_mono, hU'⟩ := (𝓤 α).has_countable_basis_iff_mono_seq'.1 H in
+let ⟨U', U'_mono, hU'⟩ := H.exists_antimono_seq' in
 complete_of_convergent_controlled_sequences H U' (λ n, hU'.2 ⟨n, subset.refl _⟩)
   (λ u hu, H' u $ cauchy_seq_of_controlled U' (λ s hs, hU'.1 hs) hu)