chore(order/filter/small_sets): redefine, golf (#13672)

The new definition is defeq to the old one.

Author: urkud

src/order/filter/small_sets.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Floris van Doorn
 -/
-import order.filter.bases
+import order.filter.lift
 
 /-!
 # The filter of small sets
@@ -25,44 +25,19 @@ variables {α β : Type*} {ι : Sort*}
 
 namespace filter
 
-/-- The filter `f.small_sets` is the largest filter containing all powersets of members of `f`.
-  Note: `𝓟` is the principal filter and `𝒫` is the powerset. -/
-def small_sets (f : filter α) : filter (set α) :=
-⨅ t ∈ f, 𝓟 (𝒫 t)
+/-- The filter `f.small_sets` is the largest filter containing all powersets of members of `f`. -/
+def small_sets (f : filter α) : filter (set α) := f.lift' powerset
 
 lemma small_sets_eq_generate {f : filter α} : f.small_sets = generate (powerset '' f.sets) :=
-by simp_rw [generate_eq_binfi, small_sets, infi_image, filter.mem_sets]
-
-lemma has_basis_small_sets (f : filter α) :
-  has_basis f.small_sets (λ t : set α, t ∈ f) powerset :=
-begin
-  apply has_basis_binfi_principal _ _,
-  { rintros u (u_in : u ∈ f) v (v_in : v ∈ f),
-    use [u ∩ v, inter_mem u_in v_in],
-    split,
-    rintros w (w_sub : w ⊆ u ∩ v),
-    exact w_sub.trans (inter_subset_left u v),
-    rintros w (w_sub : w ⊆ u ∩ v),
-    exact w_sub.trans (inter_subset_right u v) },
-  { use univ,
-    exact univ_mem },
-end
+by { simp_rw [generate_eq_binfi, small_sets, infi_image], refl }
 
 lemma has_basis.small_sets {f : filter α} {p : ι → Prop} {s : ι → set α}
   (h : has_basis f p s) : has_basis f.small_sets p (λ i, 𝒫 (s i)) :=
-⟨begin
-  intros t,
-  rw f.has_basis_small_sets.mem_iff,
-  split,
-  { rintro ⟨u, u_in, hu : {v : set α | v ⊆ u} ⊆ t⟩,
-    rcases h.mem_iff.mp u_in with ⟨i, hpi, hiu⟩,
-    use [i, hpi],
-    apply subset.trans _ hu,
-    intros v hv x hx,
-    exact hiu (hv hx) },
-  { rintro ⟨i, hi, hui⟩,
-    exact ⟨s i, h.mem_of_mem hi, hui⟩ }
-end⟩
+h.lift' monotone_powerset
+
+lemma has_basis_small_sets (f : filter α) :
+  has_basis f.small_sets (λ t : set α, t ∈ f) powerset :=
+f.basis_sets.small_sets
 
 /-- `g` converges to `f.small_sets` if for all `s ∈ f`, eventually we have `g x ⊆ s`. -/
 lemma tendsto_small_sets_iff {la : filter α} {lb : filter β} {f : α → set β} :