feat(order/filter): reorder filter theory; add filter_upwards tactic

analysis/topology/topological_space.lean

@@ -384,7 +384,7 @@ is_closed_iff_nhds.mp hs _ $ neq_bot_of_le_neq_bot (@map_ne_bot _ _ _ f h) $
 /- locally finite family [General Topology (Bourbaki, 1995)] -/
 section locally_finite
 
-/-- A family of sets in `set α` is locally finite if at every point `x:α`, 
+/-- A family of sets in `set α` is locally finite if at every point `x:α`,
   there is a neighborhood of `x` which meets only finitely many sets in the family -/
 def locally_finite (f : β → set α) :=
 ∀x:α, ∃t∈(nhds x).sets, finite {i | f i ∩ t ≠ ∅ }
@@ -412,7 +412,7 @@ is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
   begin
     rw [le_principal_iff],
     apply @filter.inter_mem_sets _ (nhds a) _ _ h_sets,
-    apply @filter.Inter_mem_sets _ _ (nhds a) _ _ h_fin,
+    apply @filter.Inter_mem_sets _ (nhds a) _ _ _ h_fin,
     exact assume i h, this i
   end
   ... ≤ principal (- ⋃i, f i) :

analysis/topology/uniform_space.lean

@@ -100,7 +100,7 @@ lemma uniform_space.core_eq : ∀{u₁ u₂ : uniform_space.core α}, u₁.unifo
   metric space. It consists of a filter on `α × α` called the "uniformity", which
   satisfies properties analogous to the reflexivity, symmetry, and triangle properties
   of a metric.
-  
+
   A metric space has a natural uniformity, and a uniform space has a natural topology.
   A topological group also has a natural uniformity, even when it is not metrizable. -/
 class uniform_space (α : Type u) extends topological_space α, uniform_space.core α :=
@@ -999,8 +999,7 @@ let ⟨s, hs, ss_t⟩ := comp_mem_uniformity_sets ht in
     ss_t ⟨b₂, show ((b₁, a₂).1, b₂) ∈ s, from hb, ba₂⟩⟩⟩
 
 lemma vmap_quotient_eq_uniformity : vmap (λ (p : α × α), (⟦p.fst⟧, ⟦p.snd⟧)) uniformity = uniformity :=
-le_antisymm vmap_quotient_le_uniformity
-  (assume s ⟨t, ht, hs⟩, uniformity.upwards_sets ht hs)
+le_antisymm vmap_quotient_le_uniformity le_vmap_map
 
 lemma complete_space_separation [h : complete_space α] :
   complete_space (quotient (separation_setoid α)) :=