feat(logic/basic): subsingleton_of_not_nonempty (#7043)

Also generalize `not_nonempty_iff_imp_false` to `Sort *`.

Author: pechersky

src/logic/basic.lean

@@ -1216,7 +1216,7 @@ iff.intro (λ⟨a, _⟩, ⟨a⟩) (λ⟨a⟩, ⟨a, trivial⟩)
 @[simp] lemma nonempty_Prop {p : Prop} : nonempty p ↔ p :=
 iff.intro (assume ⟨h⟩, h) (assume h, ⟨h⟩)
 
-lemma not_nonempty_iff_imp_false : ¬ nonempty α ↔ α → false :=
+lemma not_nonempty_iff_imp_false {α : Sort*} : ¬ nonempty α ↔ α → false :=
 ⟨λ h a, h ⟨a⟩, λ h ⟨a⟩, h a⟩
 
 @[simp] lemma nonempty_sigma : nonempty (Σa:α, γ a) ↔ (∃a:α, nonempty (γ a)) :=
@@ -1304,6 +1304,9 @@ h.elim $ λ g, h2.elim $ λ g2, ⟨⟨g, g2⟩⟩
 
 end nonempty
 
+lemma subsingleton_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : subsingleton α :=
+⟨λ x, false.elim $ not_nonempty_iff_imp_false.mp h x⟩
+
 section ite
 
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/