refactor(order/filter): move some proofs to bases (#3478)

Move some proofs to `order/filter/bases` and add `filter.has_basis` versions.

Non-bc API changes:

* `filter.inf_ne_bot_iff`; change `∀ {U V}, U ∈ f → V ∈ g → ...` to `∀ ⦃U⦄, U ∈ f → ∀ ⦃V⦄, V ∈ g → ...`
  so that `simp` lemmas about `∀ U ∈ f` can further simplify the result;
* `filter.inf_eq_bot_iff`: similarly, change `∃ U V, ...` to `∃ (U ∈ f) (V ∈ g), ...`
* `cluster_pt_iff`: similarly, change `∀ {U V : set α}, U ∈ 𝓝 x → V ∈ F → ...` to
  `∀ ⦃U : set α⦄ (hU : U ∈ 𝓝 x) ⦃V⦄ (hV : V ∈ F), ...`

src/order/filter/bases.lean

@@ -388,6 +388,62 @@ lemma has_basis.inf_principal (hl : l.has_basis p s) (s' : set α) :
 ⟨λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq,
   mem_inter_iff, and_imp]⟩
 
+lemma has_basis.inf_basis_ne_bot_iff (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
+  ne_bot (l ⊓ l') ↔ ∀ ⦃i⦄ (hi : p i) ⦃i'⦄ (hi' : p' i'), (s i ∩ s' i').nonempty :=
+(hl.inf hl').ne_bot_iff.trans $ by simp [@forall_swap _ ι']
+
+lemma has_basis.inf_ne_bot_iff (hl : l.has_basis p s) :
+  ne_bot (l ⊓ l') ↔ ∀ ⦃i⦄ (hi : p i) ⦃s'⦄ (hs' : s' ∈ l'), (s i ∩ s').nonempty :=
+hl.inf_basis_ne_bot_iff l'.basis_sets
+
+lemma has_basis.inf_principal_ne_bot_iff (hl : l.has_basis p s) {t : set α} :
+  ne_bot (l ⊓ 𝓟 t) ↔ ∀ ⦃i⦄ (hi : p i), (s i ∩ t).nonempty :=
+(hl.inf_principal t).ne_bot_iff
+
+lemma inf_ne_bot_iff :
+  ne_bot (l ⊓ l') ↔ ∀ ⦃s : set α⦄ (hs : s ∈ l) ⦃s'⦄ (hs' : s' ∈ l'), (s ∩ s').nonempty :=
+l.basis_sets.inf_ne_bot_iff
+
+lemma inf_principal_ne_bot_iff {s : set α} :
+  ne_bot (l ⊓ 𝓟 s) ↔ ∀ U ∈ l, (U ∩ s).nonempty :=
+l.basis_sets.inf_principal_ne_bot_iff
+
+lemma inf_eq_bot_iff {f g : filter α} :
+  f ⊓ g = ⊥ ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=
+not_iff_not.1 $ inf_ne_bot_iff.trans $ by simp [← ne_empty_iff_nonempty]
+
+protected lemma disjoint_iff {f g : filter α} :
+  disjoint f g ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=
+disjoint_iff.trans inf_eq_bot_iff
+
+lemma mem_iff_inf_principal_compl {f : filter α} {s : set α} :
+  s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥ :=
+begin
+  refine not_iff_not.1 (inf_principal_ne_bot_iff.trans _).symm,
+  exact ⟨λ h hs, by simpa [empty_not_nonempty] using h s hs,
+    λ hs t ht, inter_compl_nonempty_iff.2 $ λ hts, hs $ mem_sets_of_superset ht hts⟩,
+end
+
+lemma mem_iff_disjoint_principal_compl {f : filter α} {s : set α} :
+  s ∈ f ↔ disjoint f (𝓟 sᶜ) :=
+mem_iff_inf_principal_compl.trans disjoint_iff.symm
+
+lemma le_iff_forall_disjoint_principal_compl {f g : filter α} :
+  f ≤ g ↔ ∀ V ∈ g, disjoint f (𝓟 Vᶜ) :=
+forall_congr $ λ _, forall_congr $ λ _, mem_iff_disjoint_principal_compl
+
+lemma le_iff_forall_inf_principal_compl {f g : filter α} :
+  f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=
+forall_congr $ λ _, forall_congr $ λ _, mem_iff_inf_principal_compl
+
+lemma inf_ne_bot_iff_frequently_left {f g : filter α} :
+  ne_bot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in f, p x) → ∃ᶠ x in g, p x :=
+by simpa only [inf_ne_bot_iff, frequently_iff, exists_prop, and_comm]
+
+lemma inf_ne_bot_iff_frequently_right {f g : filter α} :
+  ne_bot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in g, p x) → ∃ᶠ x in f, p x :=
+by { rw inf_comm, exact inf_ne_bot_iff_frequently_left }
+
 lemma has_basis.eq_binfi (h : l.has_basis p s) :
   l = ⨅ i (_ : p i), 𝓟 (s i) :=
 eq_binfi_of_mem_sets_iff_exists_mem $ λ t, by simp only [h.mem_iff, mem_principal_sets]

src/order/filter/basic.lean

@@ -521,46 +521,6 @@ have ∅ ∈ f ⊓ 𝓟 sᶜ, from h.symm ▸ mem_bot_sets,
 let ⟨s₁, hs₁, s₂, (hs₂ : sᶜ ⊆ s₂), (hs : s₁ ∩ s₂ ⊆ ∅)⟩ := this in
 by filter_upwards [hs₁] assume a ha, classical.by_contradiction $ assume ha', hs ⟨ha, hs₂ ha'⟩
 
-lemma inf_ne_bot_iff {f g : filter α} :
-  ne_bot (f ⊓ g) ↔ ∀ {U V}, U ∈ f → V ∈ g → set.nonempty (U ∩ V) :=
-begin
-  rw ← forall_sets_nonempty_iff_ne_bot,
-  simp_rw mem_inf_sets,
-  split ; intro h,
-  { intros U V U_in V_in,
-    exact h (U ∩ V) ⟨U, U_in, V, V_in, subset.refl _⟩ },
-  { rintros S ⟨U, U_in, V, V_in, hUV⟩,
-    cases h U_in V_in with a ha,
-    use [a, hUV ha] }
-end
-
-lemma inf_principal_ne_bot_iff {f : filter α} {s : set α} :
-  ne_bot (f ⊓ 𝓟 s) ↔ ∀ U ∈ f, (U ∩ s).nonempty :=
-begin
-  rw inf_ne_bot_iff,
-  apply forall_congr,
-  intros U,
-  split,
-  { intros h U_in,
-    exact h U_in (mem_principal_self s) },
-  { intros h V U_in V_in,
-    rw mem_principal_sets at V_in,
-    cases h U_in with x hx,
-    exact ⟨x, hx.1, V_in hx.2⟩ },
-end
-
-lemma inf_eq_bot_iff {f g : filter α} :
-  f ⊓ g = ⊥ ↔ ∃ U V, (U ∈ f) ∧ (V ∈ g) ∧ U ∩ V = ∅ :=
-begin
-  rw ← not_iff_not,
-  apply inf_ne_bot_iff.trans,
-  simp only [not_exists, not_and, ← ne.def, ne_empty_iff_nonempty]
-end
-
-protected lemma disjoint_iff {f g : filter α} :
-  disjoint f g ↔ ∃ U V, (U ∈ f) ∧ (V ∈ g) ∧ U ∩ V = ∅ :=
-disjoint_iff.trans inf_eq_bot_iff
-
 lemma eq_Inf_of_mem_sets_iff_exists_mem {S : set (filter α)} {l : filter α}
   (h : ∀ {s}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) : l = Inf S :=
 le_antisymm (le_Inf $ λ f hf s hs, h.2 ⟨f, hf, hs⟩)
@@ -808,31 +768,6 @@ begin
   exact ⟨has, hat⟩
 end
 
-lemma mem_iff_inf_principal_compl {f : filter α} {V : set α} :
-  V ∈ f ↔ f ⊓ 𝓟 Vᶜ = ⊥ :=
-begin
-  rw inf_eq_bot_iff,
-  split,
-  { intro h,
-    use [V, Vᶜ],
-    simp [h, subset.refl] },
-  { rintros ⟨U, W, U_in, W_in, UW⟩,
-    rw [mem_principal_sets, compl_subset_comm] at W_in,
-    apply mem_sets_of_superset U_in,
-    intros x x_in,
-    apply W_in,
-    intro H,
-    have : x ∈ U ∩ W := ⟨x_in, H⟩,
-    rwa UW at this },
-end
-
-lemma le_iff_forall_inf_principal_compl {f g : filter α} :
-  f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=
-begin
-  change (∀ V ∈ g, V ∈ f) ↔ _,
-  simp_rw [mem_iff_inf_principal_compl],
-end
-
 lemma principal_le_iff {s : set α} {f : filter α} :
   𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V :=
 begin
@@ -1098,24 +1033,6 @@ by simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]
 lemma frequently_top {p : α → Prop} : (∃ᶠ x in ⊤, p x) ↔ (∃ x, p x) :=
 by simp [filter.frequently]
 
-lemma inf_ne_bot_iff_frequently_left {f g : filter α} :
-  ne_bot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in f, p x) → ∃ᶠ x in g, p x :=
-begin
-  rw filter.inf_ne_bot_iff,
-  split ; intro h,
-  { intros U U_in H,
-    rcases h U_in H with ⟨x, hx, hx'⟩,
-    exact hx' hx},
-  { intros U V U_in V_in,
-    classical,
-    by_contra H,
-    exact h U_in (mem_sets_of_superset V_in $ λ v v_in v_in', H ⟨v, v_in', v_in⟩) }
-end
-
-lemma inf_ne_bot_iff_frequently_right {f g : filter α} :
-  ne_bot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in g, p x) → ∃ᶠ x in f, p x :=
-by { rw inf_comm, exact filter.inf_ne_bot_iff_frequently_left }
-
 @[simp]
 lemma frequently_principal {a : set α} {p : α → Prop} :
   (∃ᶠ x in 𝓟 a, p x) ↔ (∃ x ∈ a, p x) :=

src/topology/algebra/ordered.lean

@@ -981,7 +981,7 @@ lemma disjoint_nhds_at_top [no_top_order α] (x : α) :
 begin
   rw filter.disjoint_iff,
   cases no_top x with a ha,
-  use [Iio a, Ici a, Iio_mem_nhds ha, mem_at_top a],
+  use [Iio a, Iio_mem_nhds ha, Ici a, mem_at_top a],
   rw [inter_comm, Ici_inter_Iio, Ico_self]
 end
 

src/topology/basic.lean

@@ -634,7 +634,7 @@ def cluster_pt (x : α) (F : filter α) : Prop := ne_bot (𝓝 x ⊓ F)
 lemma cluster_pt.ne_bot {x : α} {F : filter α} (h : cluster_pt x F) : ne_bot (𝓝 x ⊓ F) := h
 
 lemma cluster_pt_iff {x : α} {F : filter α} :
-  cluster_pt x F ↔ ∀ {U V : set α}, U ∈ 𝓝 x → V ∈ F → (U ∩ V).nonempty :=
+  cluster_pt x F ↔ ∀ ⦃U : set α⦄ (hU : U ∈ 𝓝 x) ⦃V⦄ (hV : V ∈ F), (U ∩ V).nonempty :=
 inf_ne_bot_iff
 
 /-- `x` is a cluster point of a set `s` if every neighbourhood of `x` meets `s` on a nonempty

src/topology/uniform_space/separation.lean

@@ -159,8 +159,8 @@ begin
     { rw t2_iff_nhds at h,
       by_contra H,
       exact hxy (h H) },
-    rcases inf_eq_bot_iff.mp this with ⟨U, V, U_in, V_in, H⟩,
-    rcases mem_nhds_iff_symm.mp U_in with ⟨S, S_in, S_symm, S_sub⟩,
+    rcases inf_eq_bot_iff.mp this with ⟨U, U_in, V, V_in, H⟩,
+    rcases mem_nhds_iff.mp U_in with ⟨S, S_in, S_sub⟩,
     use [S, S_in],
     change y ∉ ball x S,
     intro y_in,