chore(topology/*): Use finite in place of fintype where possible (#…

…15891)

Satisfy the `fintype_finite` linter.

src/analysis/normed_space/add_torsor_bases.lean

@@ -72,7 +72,7 @@ begin
     have : convex_hull ℝ (range b.points) = ⋂ i, (b.coord i)⁻¹' Ici 0,
     { rw convex_hull_affine_basis_eq_nonneg_barycentric b, ext, simp, },
     ext,
-    simp only [this, interior_Inter_of_fintype, ← is_open_map.preimage_interior_eq_interior_preimage
+    simp only [this, interior_Inter, ← is_open_map.preimage_interior_eq_interior_preimage
       (is_open_map_barycentric_coord b _) (continuous_barycentric_coord b _),
       interior_Ici, mem_Inter, mem_set_of_eq, mem_Ioi, mem_preimage], },
 end

src/data/set/finite.lean

@@ -606,10 +606,11 @@ lemma finite.finite_subsets {α : Type u} {a : set α} (h : a.finite) : {b | b 
     ← and.assoc] using h.subset⟩
 
 /-- Finite product of finite sets is finite -/
-lemma finite.pi {δ : Type*} [fintype δ] {κ : δ → Type*} {t : Π d, set (κ d)}
+lemma finite.pi {δ : Type*} [finite δ] {κ : δ → Type*} {t : Π d, set (κ d)}
   (ht : ∀ d, (t d).finite) :
   (pi univ t).finite :=
 begin
+  casesI nonempty_fintype δ,
   lift t to Π d, finset (κ d) using ht,
   classical,
   rw ← fintype.coe_pi_finset,
@@ -676,7 +677,7 @@ lemma finite_image_fst_and_snd_iff {s : set (α × β)} :
 ⟨λ h, (h.1.prod h.2).subset $ λ x h, ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩,
   λ h, ⟨h.image _, h.image _⟩⟩
 
-lemma forall_finite_image_eval_iff {δ : Type*} [fintype δ] {κ : δ → Type*} {s : set (Π d, κ d)} :
+lemma forall_finite_image_eval_iff {δ : Type*} [finite δ] {κ : δ → Type*} {s : set (Π d, κ d)} :
   (∀ d, (eval d '' s).finite) ↔ s.finite :=
 ⟨λ h, (finite.pi h).subset $ subset_pi_eval_image _ _, λ h d, h.image _⟩
 
@@ -1000,46 +1001,46 @@ lemma finite.infi_bsupr_of_antitone {ι ι' α : Type*} [preorder ι'] [nonempty
   (⨅ j, ⨆ i ∈ s, f i j) = ⨆ i ∈ s, ⨅ j, f i j :=
 hs.supr_binfi_of_monotone (λ i hi, (hf i hi).dual_right)
 
-lemma _root_.supr_infi_of_monotone {ι ι' α : Type*} [fintype ι] [preorder ι'] [nonempty ι']
+lemma _root_.supr_infi_of_monotone {ι ι' α : Type*} [finite ι] [preorder ι'] [nonempty ι']
   [is_directed ι' (≤)] [order.frame α] {f : ι → ι' → α} (hf : ∀ i, monotone (f i)) :
   (⨆ j, ⨅ i, f i j) = ⨅ i, ⨆ j, f i j :=
 by simpa only [infi_univ] using finite_univ.supr_binfi_of_monotone (λ i hi, hf i)
 
-lemma _root_.supr_infi_of_antitone {ι ι' α : Type*} [fintype ι] [preorder ι'] [nonempty ι']
+lemma _root_.supr_infi_of_antitone {ι ι' α : Type*} [finite ι] [preorder ι'] [nonempty ι']
   [is_directed ι' (swap (≤))] [order.frame α] {f : ι → ι' → α} (hf : ∀ i, antitone (f i)) :
   (⨆ j, ⨅ i, f i j) = ⨅ i, ⨆ j, f i j :=
 @supr_infi_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ _ (λ i, (hf i).dual_left)
 
-lemma _root_.infi_supr_of_monotone {ι ι' α : Type*} [fintype ι] [preorder ι'] [nonempty ι']
+lemma _root_.infi_supr_of_monotone {ι ι' α : Type*} [finite ι] [preorder ι'] [nonempty ι']
   [is_directed ι' (swap (≤))] [order.coframe α] {f : ι → ι' → α} (hf : ∀ i, monotone (f i)) :
   (⨅ j, ⨆ i, f i j) = ⨆ i, ⨅ j, f i j :=
 supr_infi_of_antitone (λ i, (hf i).dual_right)
 
-lemma _root_.infi_supr_of_antitone {ι ι' α : Type*} [fintype ι] [preorder ι'] [nonempty ι']
+lemma _root_.infi_supr_of_antitone {ι ι' α : Type*} [finite ι] [preorder ι'] [nonempty ι']
   [is_directed ι' (≤)] [order.coframe α] {f : ι → ι' → α} (hf : ∀ i, antitone (f i)) :
   (⨅ j, ⨆ i, f i j) = ⨆ i, ⨅ j, f i j :=
 supr_infi_of_monotone (λ i, (hf i).dual_right)
 
 /-- An increasing union distributes over finite intersection. -/
-lemma Union_Inter_of_monotone {ι ι' α : Type*} [fintype ι] [preorder ι'] [is_directed ι' (≤)]
+lemma Union_Inter_of_monotone {ι ι' α : Type*} [finite ι] [preorder ι'] [is_directed ι' (≤)]
   [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ i, monotone (s i)) :
   (⋃ j : ι', ⋂ i : ι, s i j) = ⋂ i : ι, ⋃ j : ι', s i j :=
 supr_infi_of_monotone hs
 
 /-- A decreasing union distributes over finite intersection. -/
-lemma Union_Inter_of_antitone {ι ι' α : Type*} [fintype ι] [preorder ι'] [is_directed ι' (swap (≤))]
+lemma Union_Inter_of_antitone {ι ι' α : Type*} [finite ι] [preorder ι'] [is_directed ι' (swap (≤))]
   [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ i, antitone (s i)) :
   (⋃ j : ι', ⋂ i : ι, s i j) = ⋂ i : ι, ⋃ j : ι', s i j :=
 supr_infi_of_antitone hs
 
 /-- An increasing intersection distributes over finite union. -/
-lemma Inter_Union_of_monotone {ι ι' α : Type*} [fintype ι] [preorder ι'] [is_directed ι' (swap (≤))]
+lemma Inter_Union_of_monotone {ι ι' α : Type*} [finite ι] [preorder ι'] [is_directed ι' (swap (≤))]
   [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ i, monotone (s i)) :
   (⋂ j : ι', ⋃ i : ι, s i j) = ⋃ i : ι, ⋂ j : ι', s i j :=
 infi_supr_of_monotone hs
 
 /-- A decreasing intersection distributes over finite union. -/
-lemma Inter_Union_of_antitone {ι ι' α : Type*} [fintype ι] [preorder ι'] [is_directed ι' (≤)]
+lemma Inter_Union_of_antitone {ι ι' α : Type*} [finite ι] [preorder ι'] [is_directed ι' (≤)]
   [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ i, antitone (s i)) :
   (⋂ j : ι', ⋃ i : ι, s i j) = ⋃ i : ι, ⋂ j : ι', s i j :=
 infi_supr_of_antitone hs
@@ -1053,7 +1054,7 @@ begin
   exact Union_Inter_of_monotone (λ i j₁ j₂ h, preimage_mono $ hs i i.2 h)
 end
 
-lemma Union_univ_pi_of_monotone {ι ι' : Type*} [linear_order ι'] [nonempty ι'] [fintype ι]
+lemma Union_univ_pi_of_monotone {ι ι' : Type*} [linear_order ι'] [nonempty ι'] [finite ι]
   {α : ι → Type*} {s : Π i, ι' → set (α i)} (hs : ∀ i, monotone (s i)) :
   (⋃ j : ι', pi univ (λ i, s i j)) = pi univ (λ i, ⋃ j, s i j) :=
 Union_pi_of_monotone finite_univ (λ i _, hs i)

src/order/filter/basic.lean

@@ -163,7 +163,7 @@ attribute [protected] finset.Inter_mem_sets
   ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f :=
 by rw [sInter_eq_bInter, bInter_mem hfin]
 
-@[simp] lemma Inter_mem {β : Type v} {s : β → set α} [fintype β] :
+@[simp] lemma Inter_mem {β : Type v} {s : β → set α} [finite β] :
   (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f :=
 by simpa using bInter_mem finite_univ
 
@@ -555,7 +555,7 @@ lemma exists_Inter_of_mem_infi {ι : Type*} {α : Type*} {f : ι → filter α}
   (hs : s ∈ ⨅ i, f i) : ∃ t : ι → set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=
 let ⟨I, If, V, hVs, hV', hVU, hVU'⟩ := mem_infi'.1 hs in ⟨V, hVs, hVU'⟩
 
-lemma mem_infi_of_fintype {ι : Type*} [fintype ι] {α : Type*} {f : ι → filter α} (s) :
+lemma mem_infi_of_finite {ι : Type*} [finite ι] {α : Type*} {f : ι → filter α} (s) :
   s ∈ (⨅ i, f i) ↔ ∃ t : ι → set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=
 begin
   refine ⟨exists_Inter_of_mem_infi, _⟩,
@@ -772,7 +772,7 @@ lemma mem_infi_finset {s : finset α} {f : α → filter β} {t : set β} :
 begin
   simp only [← finset.set_bInter_coe, bInter_eq_Inter, infi_subtype'],
   refine ⟨λ h, _, _⟩,
-  { rcases (mem_infi_of_fintype _).1 h with ⟨p, hp, rfl⟩,
+  { rcases (mem_infi_of_finite _).1 h with ⟨p, hp, rfl⟩,
     refine ⟨λ a, if h : a ∈ s then p ⟨a, h⟩ else univ, λ a ha, by simpa [ha] using hp ⟨a, ha⟩, _⟩,
     refine Inter_congr_of_surjective id surjective_id _,
     rintro ⟨a, ha⟩, simp [ha] },
@@ -891,9 +891,9 @@ begin
   { rw [finset.infi_insert, finset.set_bInter_insert, hs, inf_principal] },
 end
 
-@[simp] lemma infi_principal_fintype {ι : Type w} [fintype ι] (f : ι → set α) :
+@[simp] lemma infi_principal {ι : Type w} [finite ι] (f : ι → set α) :
   (⨅ i, 𝓟 (f i)) = 𝓟 (⋂ i, f i) :=
-by simpa using infi_principal_finset finset.univ f
+by { casesI nonempty_fintype ι, simpa using infi_principal_finset finset.univ f }
 
 lemma infi_principal_finite {ι : Type w} {s : set ι} (hs : s.finite) (f : ι → set α) :
   (⨅ i ∈ s, 𝓟 (f i)) = 𝓟 (⋂ i ∈ s, f i) :=
@@ -984,9 +984,9 @@ lemma eventually_congr {f : filter α} {p q : α → Prop} (h : ∀ᶠ x in f, p
   (∀ᶠ x in f, p x) ↔ (∀ᶠ x in f, q x) :=
 ⟨λ hp, hp.congr h, λ hq, hq.congr $ by simpa only [iff.comm] using h⟩
 
-@[simp] lemma eventually_all {ι} [fintype ι] {l} {p : ι → α → Prop} :
+@[simp] lemma eventually_all {ι : Type*} [finite ι] {l} {p : ι → α → Prop} :
   (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x :=
-by simpa only [filter.eventually, set_of_forall] using Inter_mem
+by { casesI nonempty_fintype ι, simpa only [filter.eventually, set_of_forall] using Inter_mem }
 
 @[simp] lemma eventually_all_finite {ι} {I : set ι} (hI : I.finite) {l} {p : ι → α → Prop} :
   (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ (∀ i ∈ I, ∀ᶠ x in l, p i x) :=

src/order/filter/cofinite.lean

@@ -95,7 +95,7 @@ filter.coext $ λ s, by simp only [compl_mem_coprod, mem_cofinite, compl_compl,
   finite_image_fst_and_snd_iff]
 
 /-- Finite product of finite sets is finite -/
-lemma Coprod_cofinite {α : ι → Type*} [fintype ι] :
+lemma Coprod_cofinite {α : ι → Type*} [finite ι] :
   filter.Coprod (λ i, (cofinite : filter (α i))) = cofinite :=
 filter.coext $ λ s, by simp only [compl_mem_Coprod, mem_cofinite, compl_compl,
   forall_finite_image_eval_iff]

src/topology/algebra/module/finite_dimension.lean

@@ -47,13 +47,14 @@ open_locale big_operators
 
 section semiring
 
-variables {ι 𝕜 F : Type*} [fintype ι] [semiring 𝕜] [topological_space 𝕜]
+variables {ι 𝕜 F : Type*} [finite ι] [semiring 𝕜] [topological_space 𝕜]
   [add_comm_monoid F] [module 𝕜 F] [topological_space F]
   [has_continuous_add F] [has_continuous_smul 𝕜 F]
 
-/-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
+/-- A linear map on `ι → 𝕜` (where `ι` is finite) is continuous -/
 lemma linear_map.continuous_on_pi (f : (ι → 𝕜) →ₗ[𝕜] F) : continuous f :=
 begin
+  casesI nonempty_fintype ι,
   classical,
   -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
   -- function.
@@ -69,9 +70,8 @@ end semiring
 
 section field
 
-variables {ι 𝕜 E F : Type*} [fintype ι] [field 𝕜] [topological_space 𝕜]
-  [add_comm_group E] [module 𝕜 E] [topological_space E]
-  [add_comm_group F] [module 𝕜 F] [topological_space F]
+variables {𝕜 E F : Type*} [field 𝕜] [topological_space 𝕜] [add_comm_group E] [module 𝕜 E]
+  [topological_space E] [add_comm_group F] [module 𝕜 F] [topological_space F]
   [topological_add_group F] [has_continuous_smul 𝕜 F]
 
 /-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional. -/

src/topology/basic.lean

@@ -141,8 +141,7 @@ finite.induction_on hs
   (λ a s has hs ih h, by rw bInter_insert; exact
     is_open.inter (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
 
-lemma is_open_Inter [fintype β] {s : β → set α}
-  (h : ∀ i, is_open (s i)) : is_open (⋂ i, s i) :=
+lemma is_open_Inter [finite β] {s : β → set α} (h : ∀ i, is_open (s i)) : is_open (⋂ i, s i) :=
 suffices is_open (⋂ (i : β) (hi : i ∈ @univ β), s i), by simpa,
 is_open_bInter finite_univ (λ i _, h i)
 
@@ -206,8 +205,8 @@ finite.induction_on hs
   (λ a s has hs ih h, by rw bUnion_insert; exact
     is_closed.union (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
 
-lemma is_closed_Union [fintype β] {s : β → set α}
-  (h : ∀ i, is_closed (s i)) : is_closed (Union s) :=
+lemma is_closed_Union [finite β] {s : β → set α} (h : ∀ i, is_closed (s i)) :
+  is_closed (⋃ i, s i) :=
 suffices is_closed (⋃ (i : β) (hi : i ∈ @univ β), s i),
   by convert this; simp [set.ext_iff],
 is_closed_bUnion finite_univ (λ i _, h i)
@@ -291,9 +290,9 @@ begin
   simp [h₂],
 end
 
-@[simp] lemma interior_Inter_of_fintype {ι : Type*} [fintype ι] (f : ι → set α) :
+@[simp] lemma interior_Inter {ι : Type*} [finite ι] (f : ι → set α) :
   interior (⋂ i, f i) = ⋂ i, interior (f i) :=
-by { convert finset.univ.interior_Inter f; simp, }
+by { casesI nonempty_fintype ι, convert finset.univ.interior_Inter f; simp }
 
 lemma interior_union_is_closed_of_interior_empty {s t : set α} (h₁ : is_closed s)
   (h₂ : interior t = ∅) :
@@ -422,9 +421,9 @@ begin
   simp [h₂],
 end
 
-@[simp] lemma closure_Union_of_fintype {ι : Type*} [fintype ι] (f : ι → set α) :
+@[simp] lemma closure_Union {ι : Type*} [finite ι] (f : ι → set α) :
   closure (⋃ i, f i) = ⋃ i, closure (f i) :=
-by { convert finset.univ.closure_bUnion f; simp, }
+by { casesI nonempty_fintype ι, convert finset.univ.closure_bUnion f; simp }
 
 lemma interior_subset_closure {s : set α} : interior s ⊆ closure s :=
 subset.trans interior_subset subset_closure

src/topology/bornology/basic.lean

@@ -176,7 +176,7 @@ bInter_mem hs
   is_cobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, is_cobounded (f i) :=
 bInter_finset_mem s
 
-@[simp] lemma is_cobounded_Inter [fintype ι] {f : ι → set α} :
+@[simp] lemma is_cobounded_Inter [finite ι] {f : ι → set α} :
   is_cobounded (⋂ i, f i) ↔ ∀ i, is_cobounded (f i) :=
 Inter_mem
 
@@ -196,7 +196,7 @@ lemma is_bounded_sUnion {S : set (set α)} (hs : S.finite) :
   is_bounded (⋃₀ S) ↔ (∀ s ∈ S, is_bounded s) :=
 by rw [sUnion_eq_bUnion, is_bounded_bUnion hs]
 
-@[simp] lemma is_bounded_Union [fintype ι] {s : ι → set α} :
+@[simp] lemma is_bounded_Union [finite ι] {s : ι → set α} :
   is_bounded (⋃ i, s i) ↔ ∀ i, is_bounded (s i) :=
 by rw [← sUnion_range, is_bounded_sUnion (finite_range s), forall_range_iff]
 

src/topology/constructions.lean

@@ -1125,7 +1125,7 @@ begin
   erw induced_compose,
 end
 
-variables [fintype ι] [∀ i, topological_space (π i)] [∀ i, discrete_topology (π i)]
+variables [finite ι] [∀ i, topological_space (π i)] [∀ i, discrete_topology (π i)]
 
 /-- A finite product of discrete spaces is discrete. -/
 instance Pi.discrete_topology : discrete_topology (Π i, π i) :=

src/topology/continuous_on.lean

@@ -283,7 +283,7 @@ begin
   simp only [infi_inf_eq]
 end
 
-lemma nhds_within_pi_univ_eq {ι : Type*} {α : ι → Type*} [fintype ι] [Π i, topological_space (α i)]
+lemma nhds_within_pi_univ_eq {ι : Type*} {α : ι → Type*} [finite ι] [Π i, topological_space (α i)]
   (s : Π i, set (α i)) (x : Π i, α i) :
   𝓝[pi univ s] x = ⨅ i, comap (λ x, x i) 𝓝[s i] (x i) :=
 by simpa [nhds_within] using nhds_within_pi_eq finite_univ s x

src/topology/metric_space/metrizable.lean

@@ -24,7 +24,7 @@ open_locale bounded_continuous_function filter topological_space
 namespace topological_space
 
 variables {ι X Y : Type*} {π : ι → Type*} [topological_space X] [topological_space Y]
-  [fintype ι] [Π i, topological_space (π i)]
+  [finite ι] [Π i, topological_space (π i)]
 
 /-- A topological space is *pseudo metrizable* if there exists a pseudo metric space structure
 compatible with the topology. To endow such a space with a compatible distance, use
@@ -68,7 +68,8 @@ inducing_coe.pseudo_metrizable_space
 
 instance pseudo_metrizable_space_pi [Π i, pseudo_metrizable_space (π i)] :
   pseudo_metrizable_space (Π i, π i) :=
-by { letI := λ i, pseudo_metrizable_space_pseudo_metric (π i), apply_instance }
+by { casesI nonempty_fintype ι, letI := λ i, pseudo_metrizable_space_pseudo_metric (π i),
+  apply_instance }
 
 /-- A topological space is metrizable if there exists a metric space structure compatible with the
 topology. To endow such a space with a compatible distance, use
@@ -117,7 +118,7 @@ instance metrizable_space.subtype [metrizable_space X] (s : set X) : metrizable_
 embedding_subtype_coe.metrizable_space
 
 instance metrizable_space_pi [Π i, metrizable_space (π i)] : metrizable_space (Π i, π i) :=
-by { letI := λ i, metrizable_space_metric (π i), apply_instance }
+by { casesI nonempty_fintype ι, letI := λ i, metrizable_space_metric (π i), apply_instance }
 
 variables (X) [t3_space X] [second_countable_topology X]
 

src/topology/separation.lean

@@ -258,7 +258,7 @@ begin
     exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt finset.coe_inj.2 hts'⟩, htne, hto⟩ }
 end
 
-theorem exists_open_singleton_of_fintype [t0_space α] [fintype α] [nonempty α] :
+theorem exists_open_singleton_of_fintype [t0_space α] [finite α] [nonempty α] :
   ∃ x : α, is_open ({x} : set α) :=
 let ⟨x, _, h⟩ := exists_open_singleton_of_open_finite (set.to_finite _) univ_nonempty
   is_open_univ in ⟨x, h⟩

src/topology/subset_properties.lean

@@ -413,8 +413,8 @@ lemma compact_accumulate {K : ℕ → set α} (hK : ∀ n, is_compact (K n)) (n
   is_compact (accumulate K n) :=
 (finite_le_nat n).compact_bUnion $ λ k _, hK k
 
-lemma compact_Union {f : ι → set α} [fintype ι]
-  (h : ∀ i, is_compact (f i)) : is_compact (⋃ i, f i) :=
+lemma compact_Union {f : ι → set α} [finite ι] (h : ∀ i, is_compact (f i)) :
+  is_compact (⋃ i, f i) :=
 by rw ← bUnion_univ; exact finite_univ.compact_bUnion (λ i _, h i)
 
 lemma set.finite.is_compact (hs : s.finite) : is_compact s :=
@@ -751,11 +751,10 @@ lemma not_compact_space_iff : ¬compact_space α ↔ noncompact_space α :=
 instance : noncompact_space ℤ :=
 noncompact_space_of_ne_bot $ by simp only [filter.cocompact_eq_cofinite, filter.cofinite_ne_bot]
 
+-- Note: We can't make this into an instance because it loops with `finite.compact_space`.
 /-- A compact discrete space is finite. -/
-noncomputable
-def fintype_of_compact_of_discrete [compact_space α] [discrete_topology α] :
-  fintype α :=
-fintype_of_finite_univ $ compact_univ.finite_of_discrete
+lemma finite_of_compact_of_discrete [compact_space α] [discrete_topology α] : finite α :=
+finite.of_finite_univ $ compact_univ.finite_of_discrete
 
 lemma finite_cover_nhds_interior [compact_space α] {U : α → set α} (hU : ∀ x, U x ∈ 𝓝 x) :
   ∃ t : finset α, (⋃ x ∈ t, interior (U x)) = univ :=
@@ -915,7 +914,7 @@ begin
 end
 
 /-- Finite topological spaces are compact. -/
-@[priority 100] instance fintype.compact_space [fintype α] : compact_space α :=
+@[priority 100] instance finite.compact_space [finite α] : compact_space α :=
 { compact_univ := finite_univ.is_compact }
 
 /-- The product of two compact spaces is compact. -/
@@ -929,7 +928,7 @@ instance [compact_space α] [compact_space β] : compact_space (α ⊕ β) :=
   exact (is_compact_range continuous_inl).union (is_compact_range continuous_inr)
 end⟩
 
-instance [fintype ι] [Π i, topological_space (π i)] [∀ i, compact_space (π i)] :
+instance [finite ι] [Π i, topological_space (π i)] [∀ i, compact_space (π i)] :
   compact_space (Σ i, π i) :=
 begin
   refine ⟨_⟩,
@@ -1418,8 +1417,8 @@ lemma is_clopen.prod {s : set α} {t : set β} (hs : is_clopen s) (ht : is_clope
   is_clopen (s ×ˢ t) :=
 ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩
 
-lemma is_clopen_Union {β : Type*} [fintype β] {s : β → set α}
-  (h : ∀ i, is_clopen (s i)) : is_clopen (⋃ i, s i) :=
+lemma is_clopen_Union {β : Type*} [finite β] {s : β → set α} (h : ∀ i, is_clopen (s i)) :
+  is_clopen (⋃ i, s i) :=
 ⟨is_open_Union (forall_and_distrib.1 h).1, is_closed_Union (forall_and_distrib.1 h).2⟩
 
 lemma is_clopen_bUnion {β : Type*} {s : set β} {f : β → set α} (hs : s.finite)
@@ -1432,8 +1431,8 @@ lemma is_clopen_bUnion_finset {β : Type*} {s : finset β} {f : β → set α}
   is_clopen (⋃ i ∈ s, f i) :=
 is_clopen_bUnion s.finite_to_set h
 
-lemma is_clopen_Inter {β : Type*} [fintype β] {s : β → set α}
-  (h : ∀ i, is_clopen (s i)) : is_clopen (⋂ i, s i) :=
+lemma is_clopen_Inter {β : Type*} [finite β] {s : β → set α} (h : ∀ i, is_clopen (s i)) :
+  is_clopen (⋂ i, s i) :=
 ⟨(is_open_Inter (forall_and_distrib.1 h).1), (is_closed_Inter (forall_and_distrib.1 h).2)⟩
 
 lemma is_clopen_bInter {β : Type*} {s : set β} (hs : s.finite) {f : β → set α}