From 530e7e320b3703447d7702f320ec4bd71fd26e0c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 5 Apr 2021 01:27:16 +0000
Subject: [PATCH] chore(data/quot): rename `nonempty_of_trunc` to enable dot
 notation (#7034)

---
 src/data/fintype/basic.lean | 2 +-
 src/data/quot.lean          | 6 +++---
 src/data/set/countable.lean | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index 5ae732ee34b36..8083ebdb8a120 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -210,7 +210,7 @@ quot.rec_on_subsingleton (@univ α _).1
   mem_univ_val univ.2
 
 theorem exists_equiv_fin (α) [fintype α] : ∃ n, nonempty (α ≃ fin n) :=
-by haveI := classical.dec_eq α; exact ⟨card α, nonempty_of_trunc (equiv_fin α)⟩
+by haveI := classical.dec_eq α; exact ⟨card α, (equiv_fin α).nonempty⟩
 
 instance (α : Type*) : subsingleton (fintype α) :=
 ⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext_iff, h₁, h₂]⟩
diff --git a/src/data/quot.lean b/src/data/quot.lean
index 6c7f35343a55f..8d39c0779b049 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -326,10 +326,10 @@ noncomputable def out : trunc α → α := quot.out
 
 @[simp] theorem out_eq (q : trunc α) : mk q.out = q := trunc.eq _ _
 
-end trunc
+protected theorem nonempty (q : trunc α) : nonempty α :=
+nonempty_of_exists q.exists_rep
 
-theorem nonempty_of_trunc (q : trunc α) : nonempty α :=
-let ⟨a, _⟩ := q.exists_rep in ⟨a⟩
+end trunc
 
 namespace quotient
 variables {γ : Sort*} {φ : Sort*}
diff --git a/src/data/set/countable.lean b/src/data/set/countable.lean
index 3e61269bf5e84..2230b86a11e22 100644
--- a/src/data/set/countable.lean
+++ b/src/data/set/countable.lean
@@ -166,7 +166,7 @@ lemma countable.insert {s : set α} (a : α) (h : countable s) : countable (inse
 by { rw [set.insert_eq], exact (countable_singleton _).union h }
 
 lemma finite.countable {s : set α} : finite s → countable s
-| ⟨h⟩ := nonempty_of_trunc (by exactI trunc_encodable_of_fintype s)
+| ⟨h⟩ := trunc.nonempty (by exactI trunc_encodable_of_fintype s)
 
 /-- The set of finite subsets of a countable set is countable. -/
 lemma countable_set_of_finite_subset {s : set α} : countable s →