chore(*): use ne_ instead of neq_ in lemma names (#1878)

One exception: `mem_sets_of_neq_bot` is now `mem_sets_of_eq_bot`
because it has an equality as an assumption.

Also add `filter.infi_ne_bot_(iff_?)of_directed'` with a different
`nonempty` assumption, and use it to simplify the proof of
`lift_ne_bot_iff`.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

scripts/nolints.txt

@@ -1004,8 +1004,10 @@ filter.filter_product.of_seq_one
 filter.filter_product.of_seq_zero
 filter.gi_generate
 filter.hyperfilter
-filter.infi_neq_bot_iff_of_directed
-filter.infi_neq_bot_of_directed
+filter.infi_ne_bot_iff_of_directed
+filter.infi_ne_bot_of_directed
+filter.infi_ne_bot_iff_of_directed'
+filter.infi_ne_bot_of_directed'
 filter.infi_sets_eq
 filter.infi_sets_eq'
 filter.is_bounded_default

src/order/bounded_lattice.lean

@@ -109,7 +109,7 @@ theorem eq_bot_iff : a = ⊥ ↔ a ≤ ⊥ :=
 @[simp] theorem not_lt_bot : ¬ a < ⊥ :=
 assume h, lt_irrefl a (lt_of_lt_of_le h bot_le)
 
-theorem neq_bot_of_le_neq_bot {a b : α} (hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥ :=
+theorem ne_bot_of_le_ne_bot {a b : α} (hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥ :=
 assume ha, hb $ bot_unique $ ha ▸ hab
 
 theorem eq_bot_mono (h : a ≤ b) (h₂ : b = ⊥) : a = ⊥ :=

src/order/filter/basic.lean

@@ -401,13 +401,13 @@ exists_mem_of_ne_empty this
 lemma filter_eq_bot_of_not_nonempty {f : filter α} (ne : ¬ nonempty α) : f = ⊥ :=
 empty_in_sets_eq_bot.mp $ univ_mem_sets' $ assume x, false.elim (ne ⟨x⟩)
 
-lemma forall_sets_neq_empty_iff_neq_bot {f : filter α} :
+lemma forall_sets_ne_empty_iff_ne_bot {f : filter α} :
   (∀ (s : set α), s ∈ f → s ≠ ∅) ↔ f ≠ ⊥ :=
 by
   simp only [(@empty_in_sets_eq_bot α f).symm, ne.def];
   exact ⟨assume h hs, h _ hs rfl, assume h s hs eq, h $ eq ▸ hs⟩
 
-lemma mem_sets_of_neq_bot {f : filter α} {s : set α} (h : f ⊓ principal (-s) = ⊥) : s ∈ f :=
+lemma mem_sets_of_eq_bot {f : filter α} {s : set α} (h : f ⊓ principal (-s) = ⊥) : s ∈ f :=
 have ∅ ∈ f ⊓ principal (- 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'⟩
@@ -757,7 +757,7 @@ def cofinite : filter α :=
     by simp only [compl_inter, finite_union, ht, hs, mem_set_of_eq] }
 
 lemma cofinite_ne_bot (hi : set.infinite (@set.univ α)) : @cofinite α ≠ ⊥ :=
-forall_sets_neq_empty_iff_neq_bot.mp
+forall_sets_ne_empty_iff_ne_bot.mp
   $ λ s hs hn, by change set.finite _ at hs;
     rw [hn, set.compl_empty] at hs; exact hi hs
 
@@ -957,28 +957,28 @@ theorem map_comap_of_surjective {f : α → β} (hf : function.surjective f) (l
   map f (comap f l) = l :=
 le_antisymm map_comap_le (le_map_comap_of_surjective hf l)
 
-lemma comap_neq_bot {f : filter β} {m : α → β}
+lemma comap_ne_bot {f : filter β} {m : α → β}
   (hm : ∀t∈ f, ∃a, m a ∈ t) : comap m f ≠ ⊥ :=
-forall_sets_neq_empty_iff_neq_bot.mp $ assume s ⟨t, ht, t_s⟩,
+forall_sets_ne_empty_iff_ne_bot.mp $ assume s ⟨t, ht, t_s⟩,
   let ⟨a, (ha : a ∈ preimage m t)⟩ := hm t ht in
-  neq_bot_of_le_neq_bot (ne_empty_of_mem ha) t_s
+  ne_bot_of_le_ne_bot (ne_empty_of_mem ha) t_s
 
 lemma comap_ne_bot_of_range_mem {f : filter β} {m : α → β}
   (hf : f ≠ ⊥) (hm : range m ∈ f) : comap m f ≠ ⊥ :=
-comap_neq_bot $ assume t ht,
+comap_ne_bot $ assume t ht,
   let ⟨_, ha, a, rfl⟩ := inhabited_of_mem_sets hf (inter_mem_sets ht hm)
   in ⟨a, ha⟩
 
 lemma comap_inf_principal_ne_bot_of_image_mem {f : filter β} {m : α → β}
   (hf : f ≠ ⊥) {s : set α} (hs : m '' s ∈ f) : (comap m f ⊓ principal s) ≠ ⊥ :=
 begin
-  refine compl_compl s ▸ mt mem_sets_of_neq_bot _,
+  refine compl_compl s ▸ mt mem_sets_of_eq_bot _,
   rintros ⟨t, ht, hts⟩,
   rcases inhabited_of_mem_sets hf (inter_mem_sets hs ht) with ⟨_, ⟨x, hxs, rfl⟩, hxt⟩,
   exact absurd hxs (hts hxt)
 end
 
-lemma comap_neq_bot_of_surj {f : filter β} {m : α → β}
+lemma comap_ne_bot_of_surj {f : filter β} {m : α → β}
   (hf : f ≠ ⊥) (hm : function.surjective m) : comap m f ≠ ⊥ :=
 comap_ne_bot_of_range_mem hf $ univ_mem_sets' hm
 
@@ -1090,7 +1090,7 @@ by simp only [iff_self, pure_def, mem_principal_sets, singleton_subset_iff]
 lemma singleton_mem_pure_sets {a : α} : {a} ∈ (pure a : filter α) :=
 by simp only [mem_singleton, pure_def, mem_principal_sets, singleton_subset_iff]
 
-@[simp] lemma pure_neq_bot {α : Type u} {a : α} : pure a ≠ (⊥ : filter α) :=
+@[simp] lemma pure_ne_bot {α : Type u} {a : α} : pure a ≠ (⊥ : filter α) :=
 by simp only [pure, has_pure.pure, ne.def, not_false_iff, singleton_ne_empty, principal_eq_bot_iff]
 
 lemma mem_seq_sets_def {f : filter (α → β)} {g : filter α} {s : set β} :
@@ -1224,29 +1224,40 @@ show join (map f (principal s)) = (⨆x ∈ s, f x),
 
 end bind
 
-lemma infi_neq_bot_of_directed {f : ι → filter α}
+/-- 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,
+    by rwa [mem_infi hd hn, mem_Union] at he,
+  exact hb i (empty_in_sets_eq_bot.1 hi)
+end
+
+/-- 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) ≠ ⊥ :=
-let ⟨x⟩ := hn in
-assume h, have he: ∅  ∈ (infi f), from h.symm ▸ (mem_bot_sets : ∅ ∈ (⊥ : filter α)),
-classical.by_cases
-  (assume : nonempty ι,
-    have ∃i, ∅ ∈ f i,
-      by rw [mem_infi hd this] at he; simp only [mem_Union] at he; assumption,
-    let ⟨i, hi⟩ := this in
-    hb i $ bot_unique $
-    assume s _, (f i).sets_of_superset hi $ empty_subset _)
-  (assume : ¬ nonempty ι,
-    have univ ⊆ (∅ : set α),
-    begin
-      rw [←principal_mono, principal_univ, principal_empty, ←h],
-      exact (le_infi $ assume i, false.elim $ this ⟨i⟩)
-    end,
-    this $ mem_univ x)
+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_neq_bot_iff_of_directed {f : ι → filter α}
+lemma infi_ne_bot_iff_of_directed {f : ι → filter α}
   (hn : nonempty α) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) :=
-⟨assume neq_bot i eq_bot, neq_bot $ bot_unique $ infi_le_of_le i $ eq_bot ▸ le_refl _,
-  infi_neq_bot_of_directed hn hd⟩
+⟨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 _ _
@@ -1320,7 +1331,7 @@ le_trans h₂ h₁
 
 lemma tendsto.ne_bot {f : α → β} {x : filter α} {y : filter β} (h : tendsto f x y) (hx : x ≠ ⊥) :
   y ≠ ⊥ :=
-neq_bot_of_le_neq_bot (map_ne_bot hx) h
+ne_bot_of_le_ne_bot (map_ne_bot hx) h
 
 lemma tendsto_map {f : α → β} {x : filter α} : tendsto f x (map f x) := le_refl (map f x)
 
@@ -1539,7 +1550,7 @@ begin
     exact prod_bot }
 end
 
-lemma prod_neq_bot {f : filter α} {g : filter β} : filter.prod f g ≠ ⊥ ↔ (f ≠ ⊥ ∧ g ≠ ⊥) :=
+lemma prod_ne_bot {f : filter α} {g : filter β} : filter.prod f g ≠ ⊥ ↔ (f ≠ ⊥ ∧ g ≠ ⊥) :=
 by rw [(≠), prod_eq_bot, not_or_distrib]
 
 lemma tendsto_prod_iff {f : α × β → γ} {x : filter α} {y : filter β} {z : filter γ} :
@@ -1567,7 +1578,7 @@ lemma mem_at_top [preorder α] (a : α) : {b : α | a ≤ b} ∈ @at_top α _ :=
 mem_infi_sets a $ subset.refl _
 
 @[simp] lemma at_top_ne_bot [nonempty α] [semilattice_sup α] : (at_top : filter α) ≠ ⊥ :=
-infi_neq_bot_of_directed (by apply_instance)
+infi_ne_bot_of_directed (by apply_instance)
   (assume a b, ⟨a ⊔ b, by simp only [ge, le_principal_iff, forall_const, set_of_subset_set_of,
     mem_principal_sets, and_self, sup_le_iff, forall_true_iff] {contextual := tt}⟩)
   (assume a, by simp only [principal_eq_bot_iff, ne.def, principal_eq_bot_iff]; exact ne_empty_of_mem (le_refl a))
@@ -1828,7 +1839,7 @@ lemma ultrafilter_iff_compl_mem_iff_not_mem :
       hf.1 $ empty_in_sets_eq_bot.mp $ by convert f.inter_sets hs hns; rw [inter_compl_self],
     assume hs,
       have f ≤ principal (-s), from
-        le_of_ultrafilter hf $ assume h, hs $ mem_sets_of_neq_bot $
+        le_of_ultrafilter hf $ assume h, hs $ mem_sets_of_eq_bot $
           by simp only [h, eq_self_iff_true, lattice.neg_neg],
       by simp only [le_principal_iff] at this; assumption⟩,
  assume hf,
@@ -1889,7 +1900,7 @@ let
   top : τ          := ⟨f, h, le_refl f⟩,
   sup : Π(c:set τ), chain r c → τ :=
     λc hc, ⟨⨅a:{a:τ // a ∈ insert top c}, a.val.val,
-      infi_neq_bot_of_directed ⟨a⟩
+      infi_ne_bot_of_directed ⟨a⟩
         (directed_of_chain $ chain_insert hc $ assume ⟨b, _, hb⟩ _ _, or.inl hb)
         (assume ⟨⟨a, ha, _⟩, _⟩, ha),
       infi_le_of_le ⟨top, mem_insert _ _⟩ (le_refl _)⟩
@@ -2020,7 +2031,7 @@ lemma ultrafilter.eq_iff_val_le_val {u v : ultrafilter α} : u = v ↔ u.val ≤
  assume h, by rw subtype.ext; apply ultrafilter_unique v.property u.property.1 h⟩
 
 lemma exists_ultrafilter_iff (f : filter α) : (∃ (u : ultrafilter α), u.val ≤ f) ↔ f ≠ ⊥ :=
-⟨assume ⟨u, uf⟩, lattice.neq_bot_of_le_neq_bot u.property.1 uf,
+⟨assume ⟨u, uf⟩, lattice.ne_bot_of_le_ne_bot u.property.1 uf,
  assume h, let ⟨u, uf, hu⟩ := exists_ultrafilter h in ⟨⟨u, hu⟩, uf⟩⟩
 
 end ultrafilter

src/order/filter/lift.lean

@@ -135,22 +135,13 @@ theorem monotone_lift [preorder γ] {f : γ → filter α} {g : γ → set α 
   (hf : monotone f) (hg : monotone g) : monotone (λc, (f c).lift (g c)) :=
 assume a b h, lift_mono (hf h) (hg h)
 
-lemma lift_neq_bot_iff (hm : monotone g) : (f.lift g ≠ ⊥) ↔ (∀s∈f.sets, g s ≠ ⊥) :=
-classical.by_cases
-  (assume hn : nonempty β,
-    calc f.lift g ≠ ⊥ ↔ (⨅s : { s // s ∈ f.sets}, g s.val) ≠ ⊥ :
-      by simp only [filter.lift, infi_subtype, iff_self, ne.def]
-      ... ↔ (∀s:{ s // s ∈ f.sets}, g s.val ≠ ⊥) :
-        infi_neq_bot_iff_of_directed hn
-          (assume ⟨a, ha⟩ ⟨b, hb⟩, ⟨⟨a ∩ b, inter_mem_sets ha hb⟩,
-            hm $ inter_subset_left _ _, hm $ inter_subset_right _ _⟩)
-      ... ↔ (∀s∈f.sets, g s ≠ ⊥) : ⟨assume h s hs, h ⟨s, hs⟩, assume h ⟨s, hs⟩, h s hs⟩)
-  (assume hn : ¬ nonempty β,
-    have h₁ : f.lift g = ⊥, from filter_eq_bot_of_not_nonempty hn,
-    have h₂ : ∀s, g s = ⊥, from assume s, filter_eq_bot_of_not_nonempty hn,
-    calc (f.lift g ≠ ⊥) ↔ false : by simp only [h₁, iff_self, eq_self_iff_true, not_true, ne.def]
-      ... ↔ (∀s∈f.sets, false) : ⟨false.elim, assume h, h univ univ_mem_sets⟩
-      ... ↔ (∀s∈f.sets, g s ≠ ⊥) : by simp only [h₂, iff_self, eq_self_iff_true, not_true, ne.def])
+lemma lift_ne_bot_iff (hm : monotone g) : (f.lift g ≠ ⊥) ↔ (∀s∈f, g s ≠ ⊥) :=
+begin
+  rw [filter.lift, infi_subtype', infi_ne_bot_iff_of_directed', subtype.forall'],
+  { exact ⟨⟨univ, univ_mem_sets⟩⟩ },
+  { rintros ⟨s, hs⟩ ⟨t, ht⟩,
+    exact ⟨⟨s ∩ t, inter_mem_sets hs ht⟩, hm (inter_subset_left s t), hm (inter_subset_right s t)⟩ }
+end
 
 @[simp] lemma lift_const {f : filter α} {g : filter β} : f.lift (λx, g) = g :=
 le_antisymm (lift_le univ_mem_sets $ le_refl g) (le_lift $ assume s hs, le_refl g)
@@ -286,10 +277,10 @@ le_antisymm
     (infi_le_of_le univ $ infi_le_of_le univ_mem_sets $
     by simp only [le_principal_iff, inter_subset_right, mem_principal_sets, function.comp_app]; exact inter_subset_left _ _))
 
-lemma lift'_neq_bot_iff (hh : monotone h) : (f.lift' h ≠ ⊥) ↔ (∀s∈f.sets, h s ≠ ∅) :=
-calc (f.lift' h ≠ ⊥) ↔ (∀s∈f.sets, principal (h s) ≠ ⊥) :
-    lift_neq_bot_iff (monotone_principal.comp hh)
-  ... ↔ (∀s∈f.sets, h s ≠ ∅) : by simp only [principal_eq_bot_iff, iff_self, ne.def, principal_eq_bot_iff]
+lemma lift'_ne_bot_iff (hh : monotone h) : (f.lift' h ≠ ⊥) ↔ (∀s∈f, h s ≠ ∅) :=
+calc (f.lift' h ≠ ⊥) ↔ (∀s∈f, principal (h s) ≠ ⊥) :
+    lift_ne_bot_iff (monotone_principal.comp hh)
+  ... ↔ (∀s∈f, h s ≠ ∅) : by simp only [principal_eq_bot_iff, iff_self, ne.def, principal_eq_bot_iff]
 
 @[simp] lemma lift'_id {f : filter α} : f.lift' id = f :=
 lift_principal2

src/order/filter/pointwise.lean

@@ -75,7 +75,7 @@ lemma pointwise_mul_le_mul [monoid α] {f₁ f₂ g₁ g₂ : filter α} (hf : f
 @[to_additive]
 lemma pointwise_mul_ne_bot [monoid α] {f g : filter α} : f ≠ ⊥ → g ≠ ⊥ → f * g ≠ ⊥ :=
 begin
-  simp only [forall_sets_neq_empty_iff_neq_bot.symm],
+  simp only [forall_sets_ne_empty_iff_ne_bot.symm],
   rintros hf hg s ⟨a, ha, b, hb, ab⟩,
   rcases ne_empty_iff_exists_mem.1 (pointwise_mul_ne_empty (hf a ha) (hg b hb)) with ⟨x, hx⟩,
   exact ne_empty_iff_exists_mem.2 ⟨x, ab hx⟩

src/topology/algebra/infinite_sum.lean

@@ -174,7 +174,7 @@ mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
     from tendsto_finset_sum bs $
       assume c hc, tendsto_infi' c $ tendsto_infi' hc $ by apply tendsto.comp (hf c) tendsto_comap,
   have bs.sum g ∈ s,
-    from mem_of_closed_of_tendsto' this hsc $ forall_sets_neq_empty_iff_neq_bot.mp $
+    from mem_of_closed_of_tendsto' this hsc $ forall_sets_ne_empty_iff_ne_bot.mp $
       by simp [mem_inf_sets, exists_imp_distrib, and_imp, forall_and_distrib,
                filter.mem_infi_sets_finset, mem_comap_sets, skolem, mem_at_top_sets,
                and_comm];
@@ -183,7 +183,7 @@ mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
         have (⋂b (h : b ∈ bs), (λp:(Πb, finset (γ b)), p b) ⁻¹' {cs' | cs b h ⊆ cs' }) ≤ (⨅b∈bs, p b),
           from infi_le_infi $ assume b, infi_le_infi $ assume hb,
             le_trans (set.preimage_mono $ hp' b hb) (hp b hb),
-        neq_bot_of_le_neq_bot (h _) (le_trans (set.inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
+        ne_bot_of_le_ne_bot (h _) (le_trans (set.inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
   hss' this
 
 lemma summable_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}

src/topology/algebra/ordered.lean

@@ -861,7 +861,7 @@ variables [topological_space α] [topological_space β]
 lemma nhds_principal_ne_bot_of_is_lub {a : α} {s : set α} (ha : is_lub s a) (hs : s ≠ ∅) :
   𝓝 a ⊓ principal s ≠ ⊥ :=
 let ⟨a', ha'⟩ := exists_mem_of_ne_empty hs in
-forall_sets_neq_empty_iff_neq_bot.mp $ assume t ht,
+forall_sets_ne_empty_iff_ne_bot.mp $ assume t ht,
   let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := mem_inf_sets.mp ht in
   by_cases
     (assume h : a = a',
@@ -1373,7 +1373,7 @@ is_bounded_of_le h (is_bounded_le_nhds a)
 
 @[nolint] -- see Note [nolint_ge]
 lemma is_cobounded_ge_nhds (a : α) : (𝓝 a).is_cobounded (≥) :=
-is_cobounded_of_is_bounded nhds_neq_bot (is_bounded_le_nhds a)
+is_cobounded_of_is_bounded nhds_ne_bot (is_bounded_le_nhds a)
 
 @[nolint] -- see Note [nolint_ge]
 lemma is_cobounded_under_ge_of_tendsto {f : filter β} {u : β → α} {a : α}
@@ -1398,7 +1398,7 @@ lemma is_bounded_under_ge_of_tendsto {f : filter β} {u : β → α} {a : α}
 is_bounded_of_le h (is_bounded_ge_nhds a)
 
 lemma is_cobounded_le_nhds (a : α) : (𝓝 a).is_cobounded (≤) :=
-is_cobounded_of_is_bounded nhds_neq_bot (is_bounded_ge_nhds a)
+is_cobounded_of_is_bounded nhds_ne_bot (is_bounded_ge_nhds a)
 
 lemma is_cobounded_under_le_of_tendsto {f : filter β} {u : β → α} {a : α}
   (hf : f ≠ ⊥) (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≤) u :=

src/topology/algebra/uniform_group.lean

@@ -400,11 +400,11 @@ begin
   rcases this with ⟨U₁, U₁_nhd, V₁, V₁_nhd, H⟩,
 
   have : ∃ x₁, x₁ ∈ U₁ := exists_mem_of_ne_empty
-    (forall_sets_neq_empty_iff_neq_bot.2 de.comap_nhds_neq_bot U₁ U₁_nhd),
+    (forall_sets_ne_empty_iff_ne_bot.2 de.comap_nhds_ne_bot U₁ U₁_nhd),
   rcases this with ⟨x₁, x₁_in⟩,
 
   have : ∃ y₁, y₁ ∈ V₁ := exists_mem_of_ne_empty
-    (forall_sets_neq_empty_iff_neq_bot.2 df.comap_nhds_neq_bot V₁ V₁_nhd),
+    (forall_sets_ne_empty_iff_ne_bot.2 df.comap_nhds_ne_bot V₁ V₁_nhd),
   rcases this with ⟨y₁, y₁_in⟩,
 
   rcases (extend_Z_bilin_aux de df hφ W_nhd x₀ y₁) with ⟨U₂, U₂_nhd, HU⟩,
@@ -441,7 +441,7 @@ begin
   rintro ⟨x₀, y₀⟩,
   split,
   { apply map_ne_bot,
-    apply comap_neq_bot,
+    apply comap_ne_bot,
 
     intros U h,
     rcases exists_mem_of_ne_empty (mem_closure_iff_nhds.1 ((de.prod df).dense (x₀, y₀)) U h)

src/topology/bases.lean

@@ -288,7 +288,7 @@ let ⟨f, hf⟩ := this in
   have w : {s : set α // a ∈ s ∧ s ∈ b}, from ⟨t, ht₂, ht₁⟩,
   suffices (⨅ (x : {s // a ∈ s ∧ s ∈ b}), principal (x.val ∩ ⋃s (h₁ h₂ : s ∈ b), {f s h₂})) ≠ ⊥,
     by simpa only [closure_eq_nhds, nhds_eq, infi_inf w, inf_principal, mem_set_of_eq, mem_univ, iff_true],
-  infi_neq_bot_of_directed ⟨a⟩
+  infi_ne_bot_of_directed ⟨a⟩
     (assume ⟨s₁, has₁, hs₁⟩ ⟨s₂, has₂, hs₂⟩,
       have a ∈ s₁ ∩ s₂, from ⟨has₁, has₂⟩,
       let ⟨s₃, hs₃, has₃, hs⟩ := hb₃ _ hs₁ _ hs₂ _ this in