chore(data/quot): rename nonempty_of_trunc to enable dot notation (#…

…7034)

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₂]⟩

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*}

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 →