chore(*): rename filter.inhabited_of_mem_sets to nonempty_of_mem_sets (#1943)

In other names `inhabited` means that we have a `default` element.

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

Author: urkud

src/analysis/calculus/mean_value.lean

@@ -96,7 +96,7 @@ begin
   change f x ≤ B x at hxB,
   cases lt_or_eq_of_le hxB with hxB hxB,
   { -- If `f x < B x`, then all we need is continuity of both sides
-    apply inhabited_of_mem_sets (nhds_within_Ioi_self_ne_bot x),
+    apply nonempty_of_mem_sets (nhds_within_Ioi_self_ne_bot x),
     refine inter_mem_sets _ (Ioc_mem_nhds_within_Ioi ⟨le_refl x, hy⟩),
     have : ∀ᶠ x in nhds_within x (Icc a b), f x < B x,
       from A x (Ico_subset_Icc_self xab)

src/order/filter/bases.lean

@@ -69,7 +69,7 @@ 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,
-  λ H i hi, inhabited_of_mem_sets H (hl.mem_of_mem hi)⟩
+  λ 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

src/order/filter/basic.lean

@@ -392,7 +392,7 @@ lemma empty_in_sets_eq_bot {f : filter α} : ∅ ∈ f ↔ f = ⊥ :=
 ⟨assume h, bot_unique $ assume s _, mem_sets_of_superset h (empty_subset s),
   assume : f = ⊥, this.symm ▸ mem_bot_sets⟩
 
-lemma inhabited_of_mem_sets {f : filter α} {s : set α} (hf : f ≠ ⊥) (hs : s ∈ f) :
+lemma nonempty_of_mem_sets {f : filter α} {s : set α} (hf : f ≠ ⊥) (hs : s ∈ f) :
   s.nonempty :=
 have ∅ ∉ f, from assume h, hf $ empty_in_sets_eq_bot.mp h,
 have s ≠ ∅, from assume h, this (h ▸ hs),
@@ -1054,15 +1054,15 @@ forall_sets_ne_empty_iff_ne_bot.mp $ assume s ⟨t, ht, t_s⟩,
 lemma comap_ne_bot_of_range_mem {f : filter β} {m : α → β}
   (hf : f ≠ ⊥) (hm : range m ∈ f) : comap m f ≠ ⊥ :=
 comap_ne_bot $ assume t ht,
-  let ⟨_, ha, a, rfl⟩ := inhabited_of_mem_sets hf (inter_mem_sets ht hm)
+  let ⟨_, ha, a, rfl⟩ := nonempty_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_eq_bot _,
   rintros ⟨t, ht, hts⟩,
-  rcases inhabited_of_mem_sets hf (inter_mem_sets hs ht) with ⟨_, ⟨x, hxs, rfl⟩, hxt⟩,
+  rcases nonempty_of_mem_sets hf (inter_mem_sets hs ht) with ⟨_, ⟨x, hxs, rfl⟩, hxt⟩,
   exact absurd hxs (hts hxt)
 end
 
@@ -1999,7 +1999,7 @@ lemma exists_ultrafilter (h : f ≠ ⊥) : ∃u, u ≤ f ∧ is_ultrafilter u :=
 let
   τ                := {f' // f' ≠ ⊥ ∧ f' ≤ f},
   r : τ → τ → Prop := λt₁ t₂, t₂.val ≤ t₁.val,
-  ⟨a, ha⟩          := inhabited_of_mem_sets h univ_mem_sets,
+  ⟨a, ha⟩          := nonempty_of_mem_sets h univ_mem_sets,
   top : τ          := ⟨f, h, le_refl f⟩,
   sup : Π(c:set τ), chain r c → τ :=
     λc hc, ⟨⨅a:{a:τ // a ∈ insert top c}, a.val.val,

src/order/liminf_limsup.lean

@@ -109,7 +109,7 @@ lemma is_cobounded_of_is_bounded [is_trans α r] (hf : f ≠ ⊥) :
   f.is_bounded r → f.is_cobounded (flip r)
 | ⟨a, ha⟩ := ⟨a, assume b hb,
   have ∀ᶠ x in f, r x a ∧ r b x, from ha.and hb,
-  let ⟨x, rxa, rbx⟩ := inhabited_of_mem_sets hf this in
+  let ⟨x, rxa, rbx⟩ := nonempty_of_mem_sets hf this in
   show r b a, from trans rbx rxa⟩
 
 lemma is_cobounded_bot : is_cobounded r ⊥ ↔ (∃b, ∀x, r b x) :=
@@ -190,7 +190,7 @@ theorem Liminf_le_Limsup {f : filter α}
   (hf : f ≠ ⊥) (h₁ : f.is_bounded (≤)) (h₂ : f.is_bounded (≥)) : f.Liminf ≤ f.Limsup :=
 Liminf_le_of_le h₂ $ assume a₀ ha₀, le_Limsup_of_le h₁ $ assume a₁ ha₁, show a₀ ≤ a₁, from
   have ∀ᶠ b in f, a₀ ≤ b ∧ b ≤ a₁, from ha₀.and ha₁,
-  let ⟨b, hb₀, hb₁⟩ := inhabited_of_mem_sets hf this in
+  let ⟨b, hb₀, hb₁⟩ := nonempty_of_mem_sets hf this in
   le_trans hb₀ hb₁
 
 lemma Liminf_le_Liminf {f g : filter α}

src/topology/algebra/ordered.lean

@@ -890,7 +890,7 @@ lemma is_lub_of_mem_nhds {s : set α} {a : α} {f : filter α}
   not_lt.1 $ assume hba,
   have s ∩ {a | b < a} ∈ f ⊓ 𝓝 a,
     from inter_mem_inf_sets hsf (mem_nhds_sets (is_open_lt' _) hba),
-  let ⟨x, ⟨hxs, hxb⟩⟩ := inhabited_of_mem_sets hfa this in
+  let ⟨x, ⟨hxs, hxb⟩⟩ := nonempty_of_mem_sets hfa this in
   have b < b, from lt_of_lt_of_le hxb $ hb hxs,
   lt_irrefl b this⟩
 
@@ -917,7 +917,7 @@ have ∀a'∈s, ¬ b < f a',
       have {x | a' < x} ∩ t₁ ∈ 𝓝 a, from inter_mem_sets this ht₁,
       have ({x | a' < x} ∩ t₁) ∩ s ∈ 𝓝 a ⊓ principal s,
         from inter_mem_inf_sets this (subset.refl s),
-      let ⟨x, ⟨hx₁, hx₂⟩, hx₃⟩ := inhabited_of_mem_sets hnbot this in
+      let ⟨x, ⟨hx₁, hx₂⟩, hx₃⟩ := nonempty_of_mem_sets hnbot this in
       have hxa' : f x < f a', from hs ⟨hx₂, ht₂ hx₃⟩,
       have ha'x : f a' ≤ f x, from hf _ ha' _ hx₃ $ le_of_lt hx₁,
       lt_irrefl _ (lt_of_le_of_lt ha'x hxa')),
@@ -1264,7 +1264,7 @@ begin
   rintros x ⟨hxs, hxab⟩ y hyxb,
   have : s ∩ Ioc x y ∈ nhds_within x (Ioi x),
     from inter_mem_sets (hgt x ⟨hxs, hxab⟩) (Ioc_mem_nhds_within_Ioi ⟨le_refl _, hyxb⟩),
-  exact inhabited_of_mem_sets (nhds_within_Ioi_self_ne_bot' hxab.2) this
+  exact nonempty_of_mem_sets (nhds_within_Ioi_self_ne_bot' hxab.2) this
 end
 
 /-- A closed interval is connected. -/

src/topology/dense_embedding.lean

@@ -156,7 +156,7 @@ forall_sets_ne_empty_iff_ne_bot.mp $
 assume s ⟨t, ht, (hs : i ⁻¹' t ⊆ s)⟩,
 have t ∩ range i ∈ 𝓝 b ⊓ principal (range i),
   from inter_mem_inf_sets ht (subset.refl _),
-let ⟨_, ⟨hx₁, y, rfl⟩⟩ := inhabited_of_mem_sets di.nhds_inf_ne_bot this in
+let ⟨_, ⟨hx₁, y, rfl⟩⟩ := nonempty_of_mem_sets di.nhds_inf_ne_bot this in
 subset_ne_empty hs $ ne_empty_of_mem hx₁
 
 variables [topological_space γ]

src/topology/metric_space/basic.lean

@@ -1131,7 +1131,7 @@ instance complete_of_proper [proper_space α] : complete_space α :=
   ball (therefore compact by properness) where it is nontrivial. -/
   have A : ∃ t ∈ f, ∀ x y ∈ t, dist x y < 1 := (metric.cauchy_iff.1 hf).2 1 zero_lt_one,
   rcases A with ⟨t, ⟨t_fset, ht⟩⟩,
-  rcases inhabited_of_mem_sets hf.1 t_fset with ⟨x, xt⟩,
+  rcases nonempty_of_mem_sets hf.1 t_fset with ⟨x, xt⟩,
   have : t ⊆ closed_ball x 1 := by intros y yt; simp [dist_comm]; apply le_of_lt (ht x y xt yt),
   have : closed_ball x 1 ∈ f := f.sets_of_superset t_fset this,
   rcases (compact_iff_totally_bounded_complete.1 (proper_space.compact_ball x 1)).2 f hf (le_principal_iff.2 this)

src/topology/order.lean

@@ -551,7 +551,7 @@ have comap f (𝓝 (f a) ⊓ principal (f '' s)) ≠ ⊥ ↔ 𝓝 (f a) ⊓ prin
         from mem_inf_sets_of_right $ by simp [subset.refl],
       have s₂ ∩ f '' s ∈ 𝓝 (f a) ⊓ principal (f '' s),
         from inter_mem_sets hs₂ this,
-      let ⟨b, hb₁, ⟨a, ha, ha₂⟩⟩ := inhabited_of_mem_sets h this in
+      let ⟨b, hb₁, ⟨a, ha, ha₂⟩⟩ := nonempty_of_mem_sets h this in
       ne_empty_of_mem $ hs $ by rwa [←ha₂] at hb₁⟩,
 calc a ∈ @closure α (topological_space.induced f t) s
     ↔ (@nhds α (topological_space.induced f t) a) ⊓ principal s ≠ ⊥ : by rw [closure_eq_nhds]; refl

src/topology/uniform_space/cauchy.lean

@@ -302,7 +302,7 @@ lemma totally_bounded_iff_filter {s : set α} :
   in
   have c ≤ principal s, from le_trans ‹c ≤ f› this,
   have m ∩ s ∈ c.sets, from inter_mem_sets hm $ le_principal_iff.mp this,
-  let ⟨y, hym, hys⟩ := inhabited_of_mem_sets hc₂.left this in
+  let ⟨y, hym, hys⟩ := nonempty_of_mem_sets hc₂.left this in
   let ys := (⋃y'∈({y}:set α), {x | (x, y') ∈ d}) in
   have m ⊆ ys,
     from assume y' hy',
@@ -394,10 +394,10 @@ end
 /-- A sequence of points such that `seq n ∈ set_seq n`. Here `set_seq` is a monotonically
 decreasing sequence of sets `set_seq n ∈ f` with diameters controlled by a given sequence
 of entourages. -/
-def seq (n : ℕ) : α := some $ inhabited_of_mem_sets hf.1 (set_seq_mem hf U_mem n)
+def seq (n : ℕ) : α := some $ nonempty_of_mem_sets hf.1 (set_seq_mem hf U_mem n)
 
 lemma seq_mem (n : ℕ) : seq hf U_mem n ∈ set_seq hf U_mem n :=
-some_spec $ inhabited_of_mem_sets hf.1 (set_seq_mem hf U_mem n)
+some_spec $ nonempty_of_mem_sets hf.1 (set_seq_mem hf U_mem n)
 
 lemma seq_pair_mem ⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) :
   (seq hf U_mem m, seq hf U_mem n) ∈ U N :=

src/topology/uniform_space/completion.lean

@@ -92,7 +92,7 @@ let ⟨t₃, (ht₃ : t₃ ∈ h.val), t₄, (ht₄ : t₄ ∈ g.val), (h₂ : s
 have t₂ ∩ t₃ ∈ h.val,
   from inter_mem_sets ht₂ ht₃,
 let ⟨x, xt₂, xt₃⟩ :=
-  inhabited_of_mem_sets (h.property.left) this in
+  nonempty_of_mem_sets (h.property.left) this in
 (filter.prod f.val g.val).sets_of_superset
   (prod_mem_prod ht₁ ht₄)
   (assume ⟨a, b⟩ ⟨(ha : a ∈ t₁), (hb : b ∈ t₄)⟩,
@@ -162,7 +162,7 @@ have h_ex : ∀ s ∈ 𝓤 (Cauchy α), ∃y:α, (f, pure_cauchy y) ∈ s, from
   have t' ∈ filter.prod (f.val) (f.val),
     from f.property.right ht'₁,
   let ⟨t, ht, (h : set.prod t t ⊆ t')⟩ := mem_prod_same_iff.mp this in
-  let ⟨x, (hx : x ∈ t)⟩ := inhabited_of_mem_sets f.property.left ht in
+  let ⟨x, (hx : x ∈ t)⟩ := nonempty_of_mem_sets f.property.left ht in
   have t'' ∈ filter.prod f.val (pure x),
     from mem_prod_iff.mpr ⟨t, ht, {y:α | (x, y) ∈ t'},
       h $ mk_mem_prod hx hx,