diff --git a/Mathlib/Data/Analysis/Topology.lean b/Mathlib/Data/Analysis/Topology.lean
index 7d4816bb6b480..3928945bb7367 100644
--- a/Mathlib/Data/Analysis/Topology.lean
+++ b/Mathlib/Data/Analysis/Topology.lean
@@ -247,7 +247,7 @@ structure LocallyFinite.Realizer [TopologicalSpace α] (F : Ctop.Realizer α) (f
 
 theorem LocallyFinite.Realizer.to_locallyFinite [TopologicalSpace α] {F : Ctop.Realizer α}
     {f : β → Set α} (R : LocallyFinite.Realizer F f) : LocallyFinite f := fun a ↦
-  ⟨_, F.mem_nhds.2 ⟨(R.bas a).1, (R.bas a).2, Subset.refl _⟩, ⟨R.sets a⟩⟩
+  ⟨_, F.mem_nhds.2 ⟨(R.bas a).1, (R.bas a).2, Subset.rfl⟩, have := R.sets a; Set.toFinite _⟩
 #align locally_finite.realizer.to_locally_finite LocallyFinite.Realizer.to_locallyFinite
 
 theorem locallyFinite_iff_exists_realizer [TopologicalSpace α] (F : Ctop.Realizer α)
diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean
index 72d72cc237776..c0be3366a1dfd 100644
--- a/Mathlib/Data/Finset/LocallyFinite.lean
+++ b/Mathlib/Data/Finset/LocallyFinite.lean
@@ -312,11 +312,12 @@ def _root_.Set.fintypeOfMemBounds {s : Set α} [DecidablePred (· ∈ s)] (ha :
   Set.fintypeSubset (Set.Icc a b) fun _ hx => ⟨ha hx, hb hx⟩
 #align set.fintype_of_mem_bounds Set.fintypeOfMemBounds
 
+-- TODO: move to `Order/LocallyFinite`
 theorem _root_.BddBelow.finite_of_bddAbove {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) :
-    s.Finite := by
+    s.Finite :=
   let ⟨a, ha⟩ := h₀
   let ⟨b, hb⟩ := h₁
-  classical exact ⟨Set.fintypeOfMemBounds ha hb⟩
+  (Set.finite_Icc a b).subset fun _x hx ↦ ⟨ha hx, hb hx⟩
 #align bdd_below.finite_of_bdd_above BddBelow.finite_of_bddAbove
 
 section Filter
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 09b2182221dac..182318fe6b38d 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -26,9 +26,7 @@ about finite sets and gives ways to manipulate `Set.Finite` expressions.
 
 ## Implementation
 
-A finite set is defined to be a set whose coercion to a type has a `Fintype` instance.
-Since `Set.Finite` is `Prop`-valued, this is the mere fact that the `Fintype` instance
-exists.
+A finite set is defined to be a set whose coercion to a type has a `Finite` instance.
 
 There are two components to finiteness constructions. The first is `Fintype` instances for each
 construction. This gives a way to actually compute a `Finset` that represents the set, and these
@@ -51,15 +49,9 @@ variable {α : Type u} {β : Type v} {ι : Sort w} {γ : Type x}
 
 namespace Set
 
-/-- A set is finite if there is a `Finset` with the same elements.
-This is represented as there being a `Fintype` instance for the set
-coerced to a type.
-
-Note: this is a custom inductive type rather than `Nonempty (Fintype s)`
-so that it won't be frozen as a local instance. -/
-protected
-inductive Finite (s : Set α) : Prop
-  | intro : Fintype s → s.Finite
+/-- A set is finite if the corresponding `Subtype` is finite,
+i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`. -/
+protected def Finite (s : Set α) : Prop := Finite s
 #align set.finite Set.Finite
 
 -- The `protected` attribute does not take effect within the same namespace block.
@@ -68,31 +60,28 @@ end Set
 namespace Set
 
 theorem finite_def {s : Set α} : s.Finite ↔ Nonempty (Fintype s) :=
-  ⟨fun ⟨h⟩ => ⟨h⟩, fun ⟨h⟩ => ⟨h⟩⟩
+  finite_iff_nonempty_fintype s
 #align set.finite_def Set.finite_def
 
 protected alias ⟨Finite.nonempty_fintype, _⟩ := finite_def
 #align set.finite.nonempty_fintype Set.Finite.nonempty_fintype
 
-theorem finite_coe_iff {s : Set α} : Finite s ↔ s.Finite := by
-  rw [finite_iff_nonempty_fintype, finite_def]
+theorem finite_coe_iff {s : Set α} : Finite s ↔ s.Finite := .rfl
 #align set.finite_coe_iff Set.finite_coe_iff
 
 /-- Constructor for `Set.Finite` using a `Finite` instance. -/
-theorem toFinite (s : Set α) [Finite s] : s.Finite :=
-  finite_coe_iff.mp ‹_›
+theorem toFinite (s : Set α) [Finite s] : s.Finite := ‹_›
 #align set.to_finite Set.toFinite
 
 /-- Construct a `Finite` instance for a `Set` from a `Finset` with the same elements. -/
 protected theorem Finite.ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : p.Finite :=
-  ⟨Fintype.ofFinset s H⟩
+  have := Fintype.ofFinset s H; p.toFinite
 #align set.finite.of_finset Set.Finite.ofFinset
 
 /-- Projection of `Set.Finite` to its `Finite` instance.
 This is intended to be used with dot notation.
 See also `Set.Finite.Fintype` and `Set.Finite.nonempty_fintype`. -/
-protected theorem Finite.to_subtype {s : Set α} (h : s.Finite) : Finite s :=
-  finite_coe_iff.mpr h
+protected theorem Finite.to_subtype {s : Set α} (h : s.Finite) : Finite s := h
 #align set.finite.to_subtype Set.Finite.to_subtype
 
 /-- A finite set coerced to a type is a `Fintype`.
@@ -124,12 +113,12 @@ theorem toFinite_toFinset (s : Set α) [Fintype s] : s.toFinite.toFinset = s.toF
 
 theorem Finite.exists_finset {s : Set α} (h : s.Finite) :
     ∃ s' : Finset α, ∀ a : α, a ∈ s' ↔ a ∈ s := by
-  cases h
+  cases h.nonempty_fintype
   exact ⟨s.toFinset, fun _ => mem_toFinset⟩
 #align set.finite.exists_finset Set.Finite.exists_finset
 
 theorem Finite.exists_finset_coe {s : Set α} (h : s.Finite) : ∃ s' : Finset α, ↑s' = s := by
-  cases h
+  cases h.nonempty_fintype
   exact ⟨s.toFinset, s.coe_toFinset⟩
 #align set.finite.exists_finset_coe Set.Finite.exists_finset_coe
 
@@ -735,16 +724,19 @@ theorem finite_univ [Finite α] : (@univ α).Finite :=
   Set.toFinite _
 #align set.finite_univ Set.finite_univ
 
-theorem finite_univ_iff : (@univ α).Finite ↔ Finite α :=
-  finite_coe_iff.symm.trans (Equiv.Set.univ α).finite_iff
+theorem finite_univ_iff : (@univ α).Finite ↔ Finite α := (Equiv.Set.univ α).finite_iff
 #align set.finite_univ_iff Set.finite_univ_iff
 
 alias ⟨_root_.Finite.of_finite_univ, _⟩ := finite_univ_iff
 #align finite.of_finite_univ Finite.of_finite_univ
 
+theorem Finite.subset {s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) : t.Finite := by
+  have := hs.to_subtype
+  exact Finite.Set.subset _ ht
+#align set.finite.subset Set.Finite.subset
+
 theorem Finite.union {s t : Set α} (hs : s.Finite) (ht : t.Finite) : (s ∪ t).Finite := by
-  cases hs
-  cases ht
+  rw [Set.Finite] at hs ht
   apply toFinite
 #align set.finite.union Set.Finite.union
 
@@ -757,19 +749,16 @@ theorem Finite.sup {s t : Set α} : s.Finite → t.Finite → (s ⊔ t).Finite :
   Finite.union
 #align set.finite.sup Set.Finite.sup
 
-theorem Finite.sep {s : Set α} (hs : s.Finite) (p : α → Prop) : { a ∈ s | p a }.Finite := by
-  cases hs
-  apply toFinite
+theorem Finite.sep {s : Set α} (hs : s.Finite) (p : α → Prop) : { a ∈ s | p a }.Finite :=
+  hs.subset <| sep_subset _ _
 #align set.finite.sep Set.Finite.sep
 
-theorem Finite.inter_of_left {s : Set α} (hs : s.Finite) (t : Set α) : (s ∩ t).Finite := by
-  cases hs
-  apply toFinite
+theorem Finite.inter_of_left {s : Set α} (hs : s.Finite) (t : Set α) : (s ∩ t).Finite :=
+  hs.subset <| inter_subset_left _ _
 #align set.finite.inter_of_left Set.Finite.inter_of_left
 
-theorem Finite.inter_of_right {s : Set α} (hs : s.Finite) (t : Set α) : (t ∩ s).Finite := by
-  cases hs
-  apply toFinite
+theorem Finite.inter_of_right {s : Set α} (hs : s.Finite) (t : Set α) : (t ∩ s).Finite :=
+  hs.subset <| inter_subset_right _ _
 #align set.finite.inter_of_right Set.Finite.inter_of_right
 
 theorem Finite.inf_of_left {s : Set α} (h : s.Finite) (t : Set α) : (s ⊓ t).Finite :=
@@ -780,53 +769,41 @@ theorem Finite.inf_of_right {s : Set α} (h : s.Finite) (t : Set α) : (t ⊓ s)
   h.inter_of_right t
 #align set.finite.inf_of_right Set.Finite.inf_of_right
 
-theorem Finite.subset {s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) : t.Finite := by
-  cases hs
-  haveI := Finite.Set.subset _ ht
-  apply toFinite
-#align set.finite.subset Set.Finite.subset
-
 protected lemma Infinite.mono {s t : Set α} (h : s ⊆ t) : s.Infinite → t.Infinite :=
   mt fun ht ↦ ht.subset h
 #align set.infinite.mono Set.Infinite.mono
 
-theorem Finite.diff {s : Set α} (hs : s.Finite) (t : Set α) : (s \ t).Finite := by
-  cases hs
-  apply toFinite
+theorem Finite.diff {s : Set α} (hs : s.Finite) (t : Set α) : (s \ t).Finite :=
+  hs.subset <| diff_subset _ _
 #align set.finite.diff Set.Finite.diff
 
 theorem Finite.of_diff {s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) : s.Finite :=
   (hd.union ht).subset <| subset_diff_union _ _
 #align set.finite.of_diff Set.Finite.of_diff
 
-theorem finite_iUnion [Finite ι] {f : ι → Set α} (H : ∀ i, (f i).Finite) : (⋃ i, f i).Finite := by
-  haveI := fun i => (H i).fintype
-  apply toFinite
+theorem finite_iUnion [Finite ι] {f : ι → Set α} (H : ∀ i, (f i).Finite) : (⋃ i, f i).Finite :=
+  haveI := fun i => (H i).to_subtype
+  toFinite _
 #align set.finite_Union Set.finite_iUnion
 
-theorem Finite.sUnion {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, Set.Finite t) :
-    (⋃₀ s).Finite := by
-  cases hs
-  haveI := fun i : s => (H i i.2).to_subtype
-  apply toFinite
-#align set.finite.sUnion Set.Finite.sUnion
-
-theorem Finite.biUnion {ι} {s : Set ι} (hs : s.Finite) {t : ι → Set α}
-    (ht : ∀ i ∈ s, (t i).Finite) : (⋃ i ∈ s, t i).Finite := by
-  classical
-    cases hs
-    haveI := fintypeBiUnion s t fun i hi => (ht i hi).fintype
-    apply toFinite
-#align set.finite.bUnion Set.Finite.biUnion
-
 /-- Dependent version of `Finite.biUnion`. -/
 theorem Finite.biUnion' {ι} {s : Set ι} (hs : s.Finite) {t : ∀ i ∈ s, Set α}
     (ht : ∀ i (hi : i ∈ s), (t i hi).Finite) : (⋃ i ∈ s, t i ‹_›).Finite := by
-  cases hs
+  have := hs.to_subtype
   rw [biUnion_eq_iUnion]
   apply finite_iUnion fun i : s => ht i.1 i.2
 #align set.finite.bUnion' Set.Finite.biUnion'
 
+theorem Finite.biUnion {ι} {s : Set ι} (hs : s.Finite) {t : ι → Set α}
+    (ht : ∀ i ∈ s, (t i).Finite) : (⋃ i ∈ s, t i).Finite :=
+  hs.biUnion' ht
+#align set.finite.bUnion Set.Finite.biUnion
+
+theorem Finite.sUnion {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, Set.Finite t) :
+    (⋃₀ s).Finite := by
+  simpa only [sUnion_eq_biUnion] using hs.biUnion H
+#align set.finite.sUnion Set.Finite.sUnion
+
 theorem Finite.sInter {α : Type*} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) :
     (⋂₀ s).Finite :=
   hf.subset (sInter_subset_of_mem ht)
@@ -875,13 +852,12 @@ theorem finite_pure (a : α) : (pure a : Set α).Finite :=
 #align set.finite_pure Set.finite_pure
 
 @[simp]
-protected theorem Finite.insert (a : α) {s : Set α} (hs : s.Finite) : (insert a s).Finite := by
-  cases hs
-  apply toFinite
+protected theorem Finite.insert (a : α) {s : Set α} (hs : s.Finite) : (insert a s).Finite :=
+  (finite_singleton a).union hs
 #align set.finite.insert Set.Finite.insert
 
 theorem Finite.image {s : Set α} (f : α → β) (hs : s.Finite) : (f '' s).Finite := by
-  cases hs
+  have := hs.to_subtype
   apply toFinite
 #align set.finite.image Set.Finite.image
 
@@ -894,8 +870,8 @@ lemma Finite.of_surjOn {s : Set α} {t : Set β} (f : α → β) (hf : SurjOn f
 
 theorem Finite.dependent_image {s : Set α} (hs : s.Finite) (F : ∀ i ∈ s, β) :
     {y : β | ∃ x hx, F x hx = y}.Finite := by
-  cases hs
-  simpa [range, eq_comm] using finite_range fun x : s => F x x.2
+  have := hs.to_subtype
+  simpa [range] using finite_range fun x : s => F x x.2
 #align set.finite.dependent_image Set.Finite.dependent_image
 
 theorem Finite.map {α β} {s : Set α} : ∀ f : α → β, s.Finite → (f <$> s).Finite :=
@@ -903,11 +879,9 @@ theorem Finite.map {α β} {s : Set α} : ∀ f : α → β, s.Finite → (f <$>
 #align set.finite.map Set.Finite.map
 
 theorem Finite.of_finite_image {s : Set α} {f : α → β} (h : (f '' s).Finite) (hi : Set.InjOn f s) :
-    s.Finite := by
-  cases h
-  exact
-    ⟨Fintype.ofInjective (fun a => (⟨f a.1, mem_image_of_mem f a.2⟩ : f '' s)) fun a b eq =>
-        Subtype.eq <| hi a.2 b.2 <| Subtype.ext_iff_val.1 eq⟩
+    s.Finite :=
+  have := h.to_subtype
+  .of_injective _ hi.bijOn_image.bijective.injective
 #align set.finite.of_finite_image Set.Finite.of_finite_image
 
 section preimage
@@ -967,8 +941,8 @@ section Prod
 variable {s : Set α} {t : Set β}
 
 protected theorem Finite.prod (hs : s.Finite) (ht : t.Finite) : (s ×ˢ t : Set (α × β)).Finite := by
-  cases hs
-  cases ht
+  have := hs.to_subtype
+  have := ht.to_subtype
   apply toFinite
 #align set.finite.prod Set.Finite.prod
 
@@ -1003,27 +977,22 @@ theorem finite_prod : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite
   simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]
 #align set.finite_prod Set.finite_prod
 
-protected theorem Finite.offDiag {s : Set α} (hs : s.Finite) : s.offDiag.Finite := by
-  classical
-    cases hs
-    apply Set.toFinite
+protected theorem Finite.offDiag {s : Set α} (hs : s.Finite) : s.offDiag.Finite :=
+  (hs.prod hs).subset s.offDiag_subset_prod
 #align set.finite.off_diag Set.Finite.offDiag
 
 protected theorem Finite.image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) :
     (image2 f s t).Finite := by
-  cases hs
-  cases ht
+  have := hs.to_subtype
+  have := ht.to_subtype
   apply toFinite
 #align set.finite.image2 Set.Finite.image2
 
 end Prod
 
 theorem Finite.seq {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
-    (f.seq s).Finite := by
-  classical
-    cases hf
-    cases hs
-    apply toFinite
+    (f.seq s).Finite :=
+  hf.image2 _ hs
 #align set.finite.seq Set.Finite.seq
 
 theorem Finite.seq' {α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
@@ -1052,10 +1021,11 @@ theorem exists_finite_iff_finset {p : Set α → Prop} :
 #align set.exists_finite_iff_finset Set.exists_finite_iff_finset
 
 /-- There are finitely many subsets of a given finite set -/
-theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b | b ⊆ a }.Finite :=
-  ⟨Fintype.ofFinset ((Finset.powerset h.toFinset).map Finset.coeEmb.1) fun s => by
-      simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset, ←
-        and_assoc, Finset.coeEmb] using h.subset⟩
+theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b | b ⊆ a }.Finite := by
+  convert ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet
+  ext s
+  simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset,
+    ← and_assoc, Finset.coeEmb] using h.subset
 #align set.finite.finite_subsets Set.Finite.finite_subsets
 
 section Pi
@@ -1097,7 +1067,6 @@ end SetFiniteConstructors
 
 /-! ### Properties -/
 
-
 instance Finite.inhabited : Inhabited { s : Set α // s.Finite } :=
   ⟨⟨∅, finite_empty⟩⟩
 #align set.finite.inhabited Set.Finite.inhabited
@@ -1174,7 +1143,7 @@ theorem forall_finite_image_eval_iff {δ : Type*} [Finite δ] {κ : δ → Type*
 
 theorem finite_subset_iUnion {s : Set α} (hs : s.Finite) {ι} {t : ι → Set α} (h : s ⊆ ⋃ i, t i) :
     ∃ I : Set ι, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i := by
-  cases hs
+  have := hs.to_subtype
   choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
   refine' ⟨range f, finite_range f, fun x hx => _⟩
   rw [biUnion_range, mem_iUnion]
diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
index 9048927ed868a..084ab9e220fcf 100644
--- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
@@ -321,12 +321,11 @@ theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension {n} A B] :
 #align is_cyclotomic_extension.finite_of_singleton IsCyclotomicExtension.finite_of_singleton
 
 /-- If `S` is finite and `IsCyclotomicExtension S A B`, then `B` is a finite `A`-algebra. -/
-protected
-theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] :
+protected theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] :
     Module.Finite A B := by
   cases' nonempty_fintype S with h
   revert h₂ A B
-  refine' Set.Finite.induction_on (Set.Finite.intro h) (fun A B => _) @fun n S _ _ H A B => _
+  refine' Set.Finite.induction_on h₁ (fun A B => _) @fun n S _ _ H A B => _
   · intro _ _ _ _ _
     refine' Module.finite_def.2 ⟨({1} : Finset B), _⟩
     simp [← top_toSubmodule, ← empty, toSubmodule_bot, Submodule.one_eq_span]
diff --git a/Mathlib/RingTheory/Artinian.lean b/Mathlib/RingTheory/Artinian.lean
index 4108c7e9f5c52..a8b2bb773ac74 100644
--- a/Mathlib/RingTheory/Artinian.lean
+++ b/Mathlib/RingTheory/Artinian.lean
@@ -508,7 +508,7 @@ lemma primeSpectrum_finite : {I : Ideal R | I.IsPrime}.Finite := by
   set Spec := {I : Ideal R | I.IsPrime}
   obtain ⟨_, ⟨s, rfl⟩, H⟩ := set_has_minimal
     (range (Finset.inf · Subtype.val : Finset Spec → Ideal R)) ⟨⊤, ∅, by simp⟩
-  refine ⟨⟨s, fun p ↦ ?_⟩⟩
+  refine Set.finite_def.2 ⟨s, fun p ↦ ?_⟩
   classical
   obtain ⟨q, hq1, hq2⟩ := p.2.inf_le'.mp <| inf_eq_right.mp <|
     inf_le_right.eq_of_not_lt (H (p ⊓ s.inf Subtype.val) ⟨insert p s, by simp⟩)
diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean
index f0a59a2309102..3a6a396f5db5e 100644
--- a/Mathlib/Topology/Compactness/Compact.lean
+++ b/Mathlib/Topology/Compactness/Compact.lean
@@ -522,7 +522,7 @@ theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis (b : ι → Se
     subst this
     obtain ⟨t, ht⟩ :=
       h₁.elim_finite_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) (by rw [e])
-    refine' ⟨t.image f', Set.Finite.intro inferInstance, le_antisymm _ _⟩
+    refine' ⟨t.image f', Set.toFinite _, le_antisymm _ _⟩
     · refine' Set.Subset.trans ht _
       simp only [Set.iUnion_subset_iff]
       intro i hi
diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean
index c653c42280393..d110dce11a120 100644
--- a/Mathlib/Topology/ContinuousFunction/Bounded.lean
+++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean
@@ -544,9 +544,11 @@ theorem arzela_ascoli₁ [CompactSpace β] (A : Set (α →ᵇ β)) (closed : Is
     We extract finitely many of these sets that cover the whole space, by compactness. -/
   rcases isCompact_univ.elim_finite_subcover_image (fun x _ => (hU x).2.1) fun x _ =>
       mem_biUnion (mem_univ _) (hU x).1 with
-    ⟨tα, _, ⟨_⟩, htα⟩
+    ⟨tα, _, hfin, htα⟩
+  rcases hfin.nonempty_fintype with ⟨_⟩
   -- `tα: Set α`, `htα : univ ⊆ ⋃x ∈ tα, U x`
-  rcases @finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0 with ⟨tβ, _, ⟨_⟩, htβ⟩
+  rcases @finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0 with ⟨tβ, _, hfin, htβ⟩
+  rcases hfin.nonempty_fintype with ⟨_⟩
   -- `tβ : Set β`, `htβ : univ ⊆ ⋃y ∈ tβ, ball y ε₂`
   -- Associate to every point `y` in the space a nearby point `F y` in `tβ`
   choose F hF using fun y => show ∃ z ∈ tβ, dist y z < ε₂ by simpa using htβ (mem_univ y)