feat: a type with a non trivial filter has to be nonempty (#10145)

Preliminaries for #6844

Mathlib/Order/Filter/Basic.lean

@@ -776,6 +776,9 @@ instance unique [IsEmpty α] : Unique (Filter α) where
   uniq := filter_eq_bot_of_isEmpty
 #align filter.unique Filter.unique
 
+theorem NeBot.nonempty (f : Filter α) [hf : f.NeBot] : Nonempty α :=
+  not_isEmpty_iff.mp fun _ ↦ hf.ne (Subsingleton.elim _ _)
+
 /-- There are only two filters on a `subsingleton`: `⊥` and `⊤`. If the type is empty, then they are
 equal. -/
 theorem eq_top_of_neBot [Subsingleton α] (l : Filter α) [NeBot l] : l = ⊤ := by