From db305fb5546e787dcb2582eefe10c89ef283285e Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 11 Feb 2021 23:33:03 +0000
Subject: [PATCH] feat(data/set/finite): fintype_of_univ_finite (#6164)

From `lean-liquid`
---
 src/data/set/finite.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index 7ac64ec5d17e0..f0aa565c54794 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -187,6 +187,24 @@ fintype.of_equiv α $ (equiv.set.univ α).symm
 
 theorem finite_univ [fintype α] : finite (@univ α) := ⟨set.fintype_univ⟩
 
+/-- If `(set.univ : set α)` is finite then `α` is a finite type. -/
+noncomputable
+def fintype_of_univ_finite (H : (univ : set α).finite ) :
+  fintype α :=
+begin
+  choose t ht using H.exists_finset,
+  refine ⟨t, _⟩,
+  simpa only [set.mem_univ, iff_true] using ht
+end
+
+lemma univ_finite_iff_nonempty_fintype :
+  (univ : set α).finite ↔ nonempty (fintype α) :=
+begin
+  split,
+  { intro h, exact ⟨fintype_of_univ_finite h⟩ },
+  { rintro ⟨_i⟩, exactI finite_univ }
+end
+
 theorem infinite_univ_iff : (@univ α).infinite ↔ _root_.infinite α :=
 ⟨λ h₁, ⟨λ h₂, h₁ $ @finite_univ α h₂⟩,
   λ ⟨h₁⟩ ⟨h₂⟩, h₁ $ @fintype.of_equiv _ _ h₂ $ equiv.set.univ _⟩