feat(data/{finset,set}/basic): A nonempty set of a subsingleton is univ (#16965)

Also provide `nonempty.coe_sort` and `nontrivial.coe_sort` aliases for dot notation.

Author: YaelDillies

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -515,6 +515,6 @@ begin
   intros n hn s hfin h2 hd hU hinj,
   cases n,
   { cases hn },
-  exact @not_correct n s coe hfin.to_subtype ((nontrivial_coe _).2 h2)
+  exact @not_correct n s coe hfin.to_subtype h2.coe_sort
     ⟨hd.subtype _ _, (Union_subtype _ _).trans hU, hinj.injective, hn⟩
 end

src/analysis/normed_space/is_R_or_C.lean

@@ -98,5 +98,5 @@ lemma normed_space.sphere_nonempty_is_R_or_C [nontrivial E] {r : ℝ} (hr : 0 
   nonempty (sphere (0:E) r) :=
 begin
   letI : normed_space ℝ E := normed_space.restrict_scalars ℝ 𝕜 E,
-  exact set.nonempty_coe_sort.mpr (normed_space.sphere_nonempty.mpr hr),
+  exact (normed_space.sphere_nonempty.mpr hr).coe_sort,
 end

src/analysis/seminorm.lean

@@ -417,7 +417,7 @@ noncomputable instance : has_Sup (seminorm 𝕜 E) :=
       rcases h with ⟨q, hq⟩,
       obtain rfl | h := s.eq_empty_or_nonempty,
       { simp [real.csupr_empty] },
-      haveI : nonempty ↥s := nonempty_coe_sort.mpr h,
+      haveI : nonempty ↥s := h.coe_sort,
       simp only [supr_apply],
       refine csupr_le (λ i, ((i : seminorm 𝕜 E).add_le' x y).trans $
         add_le_add (le_csupr ⟨q x, _⟩ i) (le_csupr ⟨q y, _⟩ i));
@@ -465,7 +465,7 @@ private lemma seminorm.is_lub_Sup (s : set (seminorm 𝕜 E)) (hs₁ : bdd_above
   is_lub s (Sup s) :=
 begin
   refine ⟨λ p hp x, _, λ p hp x, _⟩;
-  haveI : nonempty ↥s := nonempty_coe_sort.mpr hs₂;
+  haveI : nonempty ↥s := hs₂.coe_sort;
   rw [seminorm.coe_Sup_eq hs₁, supr_apply],
   { rcases hs₁ with ⟨q, hq⟩,
     exact le_csupr ⟨q x, forall_range_iff.mpr $ λ i : s, hq i.2 x⟩ ⟨p, hp⟩ },

src/data/finset/basic.lean

@@ -339,6 +339,7 @@ decidable_of_iff (∃ a ∈ s, true) $ by simp_rw [exists_prop, and_true, finset
 @[simp] lemma nonempty_coe_sort {s : finset α} : nonempty ↥s ↔ s.nonempty := nonempty_subtype
 
 alias coe_nonempty ↔ _ nonempty.to_set
+alias nonempty_coe_sort ↔ _ nonempty.coe_sort
 
 lemma nonempty.bex {s : finset α} (h : s.nonempty) : ∃ x : α, x ∈ s := h
 
@@ -918,7 +919,7 @@ lemma _root_.directed_on.exists_mem_subset_of_finset_subset_bUnion {α ι : Type
   {s : finset α} (hs : (s : set α) ⊆ ⋃ i ∈ c, f i) : ∃ i ∈ c, (s : set α) ⊆ f i :=
 begin
   rw set.bUnion_eq_Union at hs,
-  haveI := set.nonempty_coe_sort.2 hn,
+  haveI := hn.coe_sort,
   obtain ⟨⟨i, hic⟩, hi⟩ :=
     (directed_comp.2 hc.directed_coe).exists_mem_subset_of_finset_subset_bUnion hs,
   exact ⟨i, hic, hi⟩

src/data/fintype/basic.lean

@@ -103,6 +103,9 @@ lemma eq_univ_of_forall  : (∀ x, x ∈ s) → s = univ := eq_univ_iff_forall.2
 @[simp, norm_cast] lemma coe_eq_univ : (s : set α) = set.univ ↔ s = univ :=
 by rw [←coe_univ, coe_inj]
 
+lemma nonempty.eq_univ [subsingleton α] : s.nonempty → s = univ :=
+by { rintro ⟨x, hx⟩, refine eq_univ_of_forall (λ y, by rwa subsingleton.elim y x) }
+
 lemma univ_nonempty_iff : (univ : finset α).nonempty ↔ nonempty α :=
 by rw [← coe_nonempty, coe_univ, set.nonempty_iff_univ_nonempty]
 

src/data/set/basic.lean

@@ -289,6 +289,8 @@ protected def nonempty (s : set α) : Prop := ∃ x, x ∈ s
 
 @[simp] lemma nonempty_coe_sort {s : set α} : nonempty ↥s ↔ s.nonempty := nonempty_subtype
 
+alias nonempty_coe_sort ↔ _ nonempty.coe_sort
+
 lemma nonempty_def : s.nonempty ↔ ∃ x, x ∈ s := iff.rfl
 
 lemma nonempty_of_mem {x} (h : x ∈ s) : s.nonempty := ⟨x, h⟩
@@ -433,6 +435,9 @@ univ_subset_iff.symm.trans $ forall_congr $ λ x, imp_iff_right trivial
 
 theorem eq_univ_of_forall {s : set α} : (∀ x, x ∈ s) → s = univ := eq_univ_iff_forall.2
 
+lemma nonempty.eq_univ [subsingleton α] : s.nonempty → s = univ :=
+by { rintro ⟨x, hx⟩, refine eq_univ_of_forall (λ y, by rwa subsingleton.elim y x) }
+
 lemma eq_univ_of_subset {s t : set α} (h : s ⊆ t) (hs : s = univ) : t = univ :=
 eq_univ_of_univ_subset $ hs ▸ h
 
@@ -1930,17 +1935,19 @@ lemma nontrivial_of_nontrivial (hs : s.nontrivial) : nontrivial α :=
 let ⟨x, _, y, _, hxy⟩ := hs in ⟨⟨x, y, hxy⟩⟩
 
 /-- `s`, coerced to a type, is a nontrivial type if and only if `s` is a nontrivial set. -/
-@[simp, norm_cast] lemma nontrivial_coe (s : set α) : nontrivial s ↔ s.nontrivial :=
+@[simp, norm_cast] lemma nontrivial_coe_sort {s : set α} : nontrivial s ↔ s.nontrivial :=
 by simp_rw [← nontrivial_univ_iff, set.nontrivial, mem_univ,
             exists_true_left, set_coe.exists, subtype.mk_eq_mk]
 
+alias nontrivial_coe_sort ↔ _ nontrivial.coe_sort
+
 /-- A type with a set `s` whose `coe_sort` is a nontrivial type is nontrivial.
 For the corresponding result for `subtype`, see `subtype.nontrivial_iff_exists_ne`. -/
 lemma nontrivial_of_nontrivial_coe (hs : nontrivial s) : nontrivial α :=
-by { rw [s.nontrivial_coe] at hs, exact nontrivial_of_nontrivial hs }
+nontrivial_of_nontrivial $ nontrivial_coe_sort.1 hs
 
 theorem nontrivial_mono {α : Type*} {s t : set α} (hst : s ⊆ t) (hs : nontrivial s) :
-  nontrivial t := (nontrivial_coe _).2 $ (s.nontrivial_coe.1 hs).mono hst
+  nontrivial t := nontrivial.coe_sort $ (nontrivial_coe_sort.1 hs).mono hst
 
 /-- The preimage of a nontrivial set under a surjective map is nontrivial. -/
 theorem nontrivial.preimage {s : set β} (hs : s.nontrivial) {f : α → β}

src/measure_theory/function/jacobian.lean

@@ -220,7 +220,7 @@ begin
       { rcases hs with ⟨x, xs⟩,
         rcases s_subset x xs with ⟨n, z, hnz⟩,
         exact false.elim z.2 },
-      { exact nonempty_coe_sort.2 hT } },
+      { exact hT.coe_sort } },
     inhabit (ℕ × T × ℕ),
     exact ⟨_, encodable.surjective_decode_iget _⟩ },
   -- these sets `t q = K n z p` will do

src/topology/algebra/semigroup.lean

@@ -55,8 +55,8 @@ that this holds for all `m' ∈ N`. -/
     λ s hs, set.sInter_subset_of_mem hs⟩,
   { obtain rfl | hcnemp := c.eq_empty_or_nonempty,
     { rw set.sInter_empty, apply set.univ_nonempty },
-    convert @is_compact.nonempty_Inter_of_directed_nonempty_compact_closed _ _ _
-      (set.nonempty_coe_sort.mpr hcnemp) (coe : c → set M) _ _ _ _,
+    convert @is_compact.nonempty_Inter_of_directed_nonempty_compact_closed _ _ _ hcnemp.coe_sort
+      (coe : c → set M) _ _ _ _,
     { simp only [subtype.range_coe_subtype, set.set_of_mem_eq] } ,
     { refine directed_on.directed_coe (is_chain.directed_on hc.symm) },
     exacts [λ i, (hcs i.prop).2.1, λ i, (hcs i.prop).1.is_compact, λ i, (hcs i.prop).1] },