diff --git a/archive/100-theorems-list/83_friendship_graphs.lean b/archive/100-theorems-list/83_friendship_graphs.lean
index 0e4f03120b234..a60e1e69bdf6a 100644
--- a/archive/100-theorems-list/83_friendship_graphs.lean
+++ b/archive/100-theorems-list/83_friendship_graphs.lean
@@ -76,7 +76,7 @@ theorem adj_matrix_sq_of_ne {v w : V} (hvw : v ≠ w) :
   ((G.adj_matrix R) ^ 2) v w = 1 :=
 begin
   rw [sq, ← nat.cast_one, ← hG hvw],
-  simp [common_neighbors, neighbor_finset_eq_filter, finset.filter_filter, finset.filter_inter,
+  simp [common_neighbors, neighbor_finset_eq_filter, finset.filter_filter,
     and_comm, ← neighbor_finset_def],
 end
 
diff --git a/src/analysis/locally_convex/weak_dual.lean b/src/analysis/locally_convex/weak_dual.lean
index 080fcb72b52b6..767ae15df4c5a 100644
--- a/src/analysis/locally_convex/weak_dual.lean
+++ b/src/analysis/locally_convex/weak_dual.lean
@@ -100,7 +100,7 @@ begin
     simp only [id.def],
     let U' := hU₁.to_finset,
     by_cases hU₃ : U.fst.nonempty,
-    { have hU₃' : U'.nonempty := (set.finite.to_finset.nonempty hU₁).mpr hU₃,
+    { have hU₃' : U'.nonempty := hU₁.nonempty_to_finset.mpr hU₃,
       refine ⟨(U'.sup p).ball 0 $ U'.inf' hU₃' U.snd, p.basis_sets_mem _ $
         (finset.lt_inf'_iff _).2 $ λ y hy, hU₂ y $ (hU₁.mem_to_finset).mp hy, λ x hx y hy, _⟩,
       simp only [set.mem_preimage, set.mem_pi, mem_ball_zero_iff],
diff --git a/src/combinatorics/configuration.lean b/src/combinatorics/configuration.lean
index c767e7bd0718e..778bb949eb37b 100644
--- a/src/combinatorics/configuration.lean
+++ b/src/combinatorics/configuration.lean
@@ -435,11 +435,11 @@ begin
   classical,
   have h1 : fintype.card {q // q ≠ p} + 1 = fintype.card P,
   { apply (eq_tsub_iff_add_eq_of_le (nat.succ_le_of_lt (fintype.card_pos_iff.mpr ⟨p⟩))).mp,
-    convert (fintype.card_subtype_compl).trans (congr_arg _ (fintype.card_subtype_eq p)) },
+    convert (fintype.card_subtype_compl _).trans (congr_arg _ (fintype.card_subtype_eq p)) },
   have h2 : ∀ l : {l : L // p ∈ l}, fintype.card {q // q ∈ l.1 ∧ q ≠ p} = order P L,
   { intro l,
     rw [←fintype.card_congr (equiv.subtype_subtype_equiv_subtype_inter _ _),
-        fintype.card_subtype_compl, ←nat.card_eq_fintype_card],
+      fintype.card_subtype_compl (λ (x : subtype (∈ l.val)), x.val = p), ←nat.card_eq_fintype_card],
     refine tsub_eq_of_eq_add ((point_count_eq P l.1).trans _),
     rw ← fintype.card_subtype_eq (⟨p, l.2⟩ : {q : P // q ∈ l.1}),
     simp_rw subtype.ext_iff_val },
diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean
index 5d940e07294f7..f77d5b131c90a 100644
--- a/src/combinatorics/simple_graph/basic.lean
+++ b/src/combinatorics/simple_graph/basic.lean
@@ -755,7 +755,7 @@ by { ext, simp }
 
 lemma neighbor_finset_compl [decidable_eq V] [decidable_rel G.adj] (v : V) :
   Gᶜ.neighbor_finset v = (G.neighbor_finset v)ᶜ \ {v} :=
-by simp only [neighbor_finset, neighbor_set_compl, set.to_finset_sdiff, set.to_finset_compl,
+by simp only [neighbor_finset, neighbor_set_compl, set.to_finset_diff, set.to_finset_compl,
     set.to_finset_singleton]
 
 @[simp]
@@ -917,17 +917,17 @@ begin
   { rw finset.insert_subset,
     split,
     { simpa, },
-    { rw [neighbor_finset, ← set.subset_iff_to_finset_subset],
+    { rw [neighbor_finset, set.to_finset_mono],
       exact G.common_neighbors_subset_neighbor_set_left _ _ } }
 end
 
 lemma card_common_neighbors_top [decidable_eq V] {v w : V} (h : v ≠ w) :
   fintype.card ((⊤ : simple_graph V).common_neighbors v w) = fintype.card V - 2 :=
 begin
-  simp only [common_neighbors_top_eq, ← set.to_finset_card, set.to_finset_sdiff],
+  simp only [common_neighbors_top_eq, ← set.to_finset_card, set.to_finset_diff],
   rw finset.card_sdiff,
   { simp [finset.card_univ, h], },
-  { simp only [←set.subset_iff_to_finset_subset, set.subset_univ] },
+  { simp only [set.to_finset_mono, set.subset_univ] },
 end
 
 end finite
diff --git a/src/combinatorics/simple_graph/strongly_regular.lean b/src/combinatorics/simple_graph/strongly_regular.lean
index 524ac8e540e0d..5f8a7113bd96a 100644
--- a/src/combinatorics/simple_graph/strongly_regular.lean
+++ b/src/combinatorics/simple_graph/strongly_regular.lean
@@ -134,7 +134,7 @@ lemma is_SRG_with.card_common_neighbors_eq_of_adj_compl (h : G.is_SRG_with n k 
   fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - μ) - 2 :=
 begin
   simp only [←set.to_finset_card, common_neighbors, set.to_finset_inter, neighbor_set_compl,
-    set.to_finset_sdiff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
+    set.to_finset_diff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
   simp_rw compl_neighbor_finset_sdiff_inter_eq,
   have hne : v ≠ w := ne_of_adj _ ha,
   rw compl_adj at ha,
@@ -153,7 +153,7 @@ lemma is_SRG_with.card_common_neighbors_eq_of_not_adj_compl (h : G.is_SRG_with n
   fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - ℓ) :=
 begin
   simp only [←set.to_finset_card, common_neighbors, set.to_finset_inter, neighbor_set_compl,
-    set.to_finset_sdiff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
+    set.to_finset_diff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
   simp only [not_and, not_not, compl_adj] at hna,
   have h2' := hna hn,
   simp_rw [compl_neighbor_finset_sdiff_inter_eq, sdiff_compl_neighbor_finset_inter_eq h2'],
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index c4a8648dada97..804ed9a6d3afc 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -641,6 +641,13 @@ by simp [to_finset]
 @[simp] theorem mem_to_finset_val {s : set α} [fintype s] {a : α} : a ∈ s.to_finset.1 ↔ a ∈ s :=
 mem_to_finset
 
+/-- Membership of a set with a `fintype` instance is decidable.
+
+Using this as an instance leads to potential loops with `subtype.fintype` under certain decidability
+assumptions, so it should only be declared a local instance. -/
+def decidable_mem_of_fintype [decidable_eq α] (s : set α) [fintype s] (a) : decidable (a ∈ s) :=
+decidable_of_iff _ mem_to_finset
+
 -- We use an arbitrary `[fintype s]` instance here,
 -- not necessarily coming from a `[fintype α]`.
 @[simp]
@@ -667,9 +674,46 @@ by simp only [finset.ssubset_def, to_finset_mono, ssubset_def]
   disjoint s.to_finset t.to_finset ↔ disjoint s t :=
 by simp only [disjoint_iff_disjoint_coe, coe_to_finset]
 
+lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
+  [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
+by { ext, simp }
+
+lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]
+  [fintype s] [fintype t] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
+by { ext, simp }
+
+lemma to_finset_diff {α : Type*} [decidable_eq α] (s t : set α) [fintype s] [fintype t]
+  [fintype (s \ t : set α)] : (s \ t).to_finset = s.to_finset \ t.to_finset :=
+by { ext, simp }
+
+lemma to_finset_ne_eq_erase {α : Type*} [decidable_eq α] [fintype α] (a : α)
+  [fintype {x : α | x ≠ a}] : {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
+by { ext, simp }
+
 theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] :
   (sᶜ).to_finset = s.to_finsetᶜ :=
-by { ext a, simp }
+by { ext, simp }
+
+/- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
+it essentially infers `fintype.{v} (set.univ.{u} : set α)` with `v` and `u` distinct.
+Reported in leanprover-community/lean#672 -/
+@[simp] lemma to_finset_univ [fintype ↥(set.univ : set α)] [fintype α] :
+  (set.univ : set α).to_finset = finset.univ :=
+by { ext, simp }
+
+@[simp] lemma to_finset_range [decidable_eq α] [fintype β] (f : β → α) [fintype (set.range f)] :
+  (set.range f).to_finset = finset.univ.image f :=
+by { ext, simp }
+
+/- TODO The `↥` circumvents an elaboration bug. See comment on `set.to_finset_univ`. -/
+lemma to_finset_singleton (a : α) [fintype ↥({a} : set α)] : ({a} : set α).to_finset = {a} :=
+by { ext, simp }
+
+/- TODO The `↥` circumvents an elaboration bug. See comment on `set.to_finset_univ`. -/
+@[simp] lemma to_finset_insert [decidable_eq α] {a : α} {s : set α}
+  [fintype ↥(insert a s : set α)] [fintype s] :
+  (insert a s).to_finset = insert a s.to_finset :=
+by { ext, simp }
 
 lemma filter_mem_univ_eq_to_finset [fintype α] (s : set α) [fintype s] [decidable_pred (∈ s)] :
   finset.univ.filter (∈ s) = s.to_finset :=
@@ -1168,23 +1212,12 @@ instance Prop.fintype : fintype Prop :=
 instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
 fintype.subtype (univ.filter p) (by simp)
 
-/- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
-it essentially infers `fintype.{v} (set.univ.{u} : set α)` with `v` and `u` distinct.
-Reported in leanprover-community/lean#672 -/
-@[simp] lemma set.to_finset_univ [fintype ↥(set.univ : set α)] [fintype α] :
-  (set.univ : set α).to_finset = finset.univ :=
-by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
-
 @[simp] lemma set.to_finset_eq_empty_iff {s : set α} [fintype s] : s.to_finset = ∅ ↔ s = ∅ :=
-by simp [ext_iff, set.ext_iff]
+by simp only [ext_iff, set.ext_iff, set.mem_to_finset, not_mem_empty, set.mem_empty_eq]
 
 @[simp] lemma set.to_finset_empty : (∅ : set α).to_finset = ∅ :=
 set.to_finset_eq_empty_iff.mpr rfl
 
-@[simp] lemma set.to_finset_range [decidable_eq α] [fintype β] (f : β → α) [fintype (set.range f)] :
-  (set.range f).to_finset = finset.univ.image f :=
-by simp [ext_iff]
-
 /-- A set on a fintype, when coerced to a type, is a fintype. -/
 def set_fintype [fintype α] (s : set α) [decidable_pred (∈ s)] : fintype s :=
 subtype.fintype (λ x, x ∈ s)
@@ -1412,6 +1445,26 @@ begin
   simp
 end
 
+@[simp]
+lemma fintype.card_subtype_compl [fintype α]
+  (p : α → Prop) [fintype {x // p x}] [fintype {x // ¬ p x}] :
+  fintype.card {x // ¬ p x} = fintype.card α - fintype.card {x // p x} :=
+begin
+  classical,
+  rw [fintype.card_of_subtype (set.to_finset pᶜ), set.to_finset_compl p, finset.card_compl,
+      fintype.card_of_subtype (set.to_finset p)];
+  intro; simp only [set.mem_to_finset, set.mem_compl_eq]; refl,
+end
+
+/-- If two subtypes of a fintype have equal cardinality, so do their complements. -/
+lemma fintype.card_compl_eq_card_compl [fintype α]
+  (p q : α → Prop)
+  [fintype {x // p x}] [fintype {x // ¬ p x}]
+  [fintype {x // q x}] [fintype {x // ¬ q x}]
+  (h : fintype.card {x // p x} = fintype.card {x // q x}) :
+  fintype.card {x // ¬ p x} = fintype.card {x // ¬ q x} :=
+by simp only [fintype.card_subtype_compl, h]
+
 theorem fintype.card_quotient_le [fintype α] (s : setoid α) [decidable_rel ((≈) : α → α → Prop)] :
   fintype.card (quotient s) ≤ fintype.card α :=
 fintype.card_le_of_surjective _ (surjective_quotient_mk _)
diff --git a/src/data/nat/nth.lean b/src/data/nat/nth.lean
index 9bc9a72418d12..653ca737914eb 100644
--- a/src/data/nat/nth.lean
+++ b/src/data/nat/nth.lean
@@ -83,7 +83,7 @@ begin
   apply finset.card_erase_of_mem,
   rw [nth, set.finite.mem_to_finset],
   apply Inf_mem,
-  rwa [←set.finite.to_finset.nonempty hp'', ←finset.card_pos, hk],
+  rwa [←hp''.nonempty_to_finset, ←finset.card_pos, hk],
 end
 
 lemma nth_set_card {n : ℕ} (hp : (set_of p).finite)
@@ -108,7 +108,7 @@ lemma nth_set_nonempty_of_lt_card {n : ℕ} (hp : (set_of p).finite) (hlt: n < h
 begin
   have hp': {i : ℕ | p i ∧ ∀ (k : ℕ), k < n → nth p k < i}.finite,
   { exact hp.subset (λ x hx, hx.1) },
-  rw [←hp'^.to_finset.nonempty, ←finset.card_pos, nth_set_card p hp],
+  rw [←hp'.nonempty_to_finset, ←finset.card_pos, nth_set_card p hp],
   exact nat.sub_pos_of_lt hlt,
 end
 
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index de6dfea7e0e91..c650d408892ac 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -9,8 +9,35 @@ import data.set.functor
 /-!
 # Finite sets
 
-This file defines predicates `finite : set α → Prop` and `infinite : set α → Prop` and proves some
-basic facts about finite sets.
+This file defines predicates for finite and infinite sets and provides
+`fintype` instances for many set constructions. It also proves basic facts
+about finite sets and gives ways to manipulate `set.finite` expressions.
+
+## Main definitions
+
+* `set.finite : set α → Prop`
+* `set.infinite : set α → Prop`
+* `set.finite_of_fintype` to prove `set.finite` for a `set` from a `fintype` instance.
+* `set.finite.to_finset` to noncomputably produce a `finset` from a `set.finite` proof.
+  (See `set.to_finset` for a computable version.)
+
+## 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.
+
+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
+may be accessed using `set.to_finset`. This gets the `finset` in the correct form, since otherwise
+`finset.univ : finset s` is a `finset` for the subtype for `s`. The second component is
+"constructors" for `set.finite` that give proofs that `fintype` instances exist classically given
+other `set.finite` proofs. Unlike the `fintype` instances, these *do not* use any decidability
+instances since they do not compute anything.
+
+## Tags
+
+finite sets
 -/
 
 open set function
@@ -20,529 +47,733 @@ variables {α : Type u} {β : Type v} {ι : Sort w} {γ : Type x}
 
 namespace set
 
-/-- A set is finite if the subtype is a fintype, i.e. there is a
-  list that enumerates its members. -/
+/-- 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. -/
 inductive finite (s : set α) : Prop
 | intro : fintype s → finite
 
-lemma finite_def {s : set α} : finite s ↔ nonempty (fintype s) := ⟨λ ⟨h⟩, ⟨h⟩, λ ⟨h⟩, ⟨h⟩⟩
+/-- Constructor for `set.finite` with the `fintype` as an instance argument. -/
+theorem finite_of_fintype (s : set α) [h : fintype s] : s.finite := ⟨h⟩
+
+lemma finite_def {s : set α} : s.finite ↔ nonempty (fintype s) := ⟨λ ⟨h⟩, ⟨h⟩, λ ⟨h⟩, ⟨h⟩⟩
 
-/-- A set is infinite if it is not finite. -/
-def infinite (s : set α) : Prop := ¬ finite s
+/-- A finite set coerced to a type is a `fintype`.
+This is the `fintype` projection for a `set.finite`.
 
-/-- The subtype corresponding to a finite set is a finite type. Note
-that because `finite` isn't a typeclass, this will not fire if it
+Note that because `finite` isn't a typeclass, this definition will not fire if it
 is made into an instance -/
-noncomputable def finite.fintype {s : set α} (h : finite s) : fintype s :=
-classical.choice $ finite_def.1 h
+noncomputable def finite.fintype {s : set α} (h : s.finite) : fintype s :=
+(finite_def.mp h).some
 
-/-- Get a finset from a finite set -/
-noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
+/-- Using choice, get the `finset` that represents this `set.` -/
+noncomputable def finite.to_finset {s : set α} (h : s.finite) : finset α :=
 @set.to_finset _ _ h.fintype
 
-@[simp] lemma not_infinite {s : set α} : ¬ s.infinite ↔ s.finite :=
-by simp [infinite]
+theorem finite.exists_finset {s : set α} (h : s.finite) :
+  ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s :=
+by { casesI h, exact ⟨s.to_finset, λ _, mem_to_finset⟩ }
+
+theorem finite.exists_finset_coe {s : set α} (h : s.finite) :
+  ∃ s' : finset α, ↑s' = s :=
+by { casesI h, exact ⟨s.to_finset, s.coe_to_finset⟩ }
+
+/-- Finite sets can be lifted to finsets. -/
+instance : can_lift (set α) (finset α) :=
+{ coe := coe,
+  cond := finite,
+  prf := λ s hs, hs.exists_finset_coe }
+
+/-- A set is infinite if it is not finite.
+
+Protected so that it does not conflict with global `infinite`. -/
+protected def infinite (s : set α) : Prop := ¬ s.finite
+
+@[simp] lemma not_infinite {s : set α} : ¬ s.infinite ↔ s.finite := not_not
 
 /-- See also `fintype_or_infinite`. -/
 lemma finite_or_infinite {s : set α} : s.finite ∨ s.infinite := em _
 
-@[simp] theorem finite.mem_to_finset {s : set α} (h : finite s) {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
-@mem_to_finset _ _ h.fintype _
 
-@[simp] theorem finite.to_finset.nonempty {s : set α} (h : finite s) :
-  h.to_finset.nonempty ↔ s.nonempty :=
-show (∃ x, x ∈ h.to_finset) ↔ (∃ x, x ∈ s),
-from exists_congr (λ _, h.mem_to_finset)
+/-! ### Basic properties of `set.finite.to_finset` -/
+
+section finite_to_finset
 
-@[simp] lemma finite.coe_to_finset {s : set α} (h : finite s) : ↑h.to_finset = s :=
+@[simp] lemma finite.coe_to_finset {s : set α} (h : s.finite) : (h.to_finset : set α) = s :=
 @set.coe_to_finset _ s h.fintype
 
-@[simp] lemma finite.coe_sort_to_finset {s : set α} (h : finite s) :
+@[simp] theorem finite.mem_to_finset {s : set α} (h : s.finite) {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
+@mem_to_finset _ _ h.fintype _
+
+@[simp] theorem finite.nonempty_to_finset {s : set α} (h : s.finite) :
+  h.to_finset.nonempty ↔ s.nonempty :=
+by rw [← finset.coe_nonempty, finite.coe_to_finset]
+
+@[simp] lemma finite.coe_sort_to_finset {s : set α} (h : s.finite) :
   (h.to_finset : Type*) = s :=
 by rw [← finset.coe_sort_coe _, h.coe_to_finset]
 
-@[simp] lemma finite_empty_to_finset (h : finite (∅ : set α)) : h.to_finset = ∅ :=
+@[simp] lemma finite_empty_to_finset (h : (∅ : set α).finite) : h.to_finset = ∅ :=
 by rw [← finset.coe_inj, h.coe_to_finset, finset.coe_empty]
 
-@[simp] lemma finite.to_finset_inj {s t : set α} {hs : finite s} {ht : finite t} :
+@[simp] lemma finite.to_finset_inj {s t : set α} {hs : s.finite} {ht : t.finite} :
   hs.to_finset = ht.to_finset ↔ s = t :=
-by simp [←finset.coe_inj]
+by simp only [←finset.coe_inj, finite.coe_to_finset]
 
-lemma subset_to_finset_iff {s : finset α} {t : set α} (ht : finite t) :
+lemma subset_to_finset_iff {s : finset α} {t : set α} (ht : t.finite) :
   s ⊆ ht.to_finset ↔ ↑s ⊆ t :=
 by rw [← finset.coe_subset, ht.coe_to_finset]
 
-@[simp] lemma finite_to_finset_eq_empty_iff {s : set α} {h : finite s} :
+@[simp] lemma finite_to_finset_eq_empty_iff {s : set α} {h : s.finite} :
   h.to_finset = ∅ ↔ s = ∅ :=
-by simp [←finset.coe_inj]
+by simp only [←finset.coe_inj, finite.coe_to_finset, finset.coe_empty]
 
-theorem finite.exists_finset {s : set α} : finite s →
-  ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s
-| ⟨h⟩ := by exactI ⟨to_finset s, λ _, mem_to_finset⟩
-
-theorem finite.exists_finset_coe {s : set α} (hs : finite s) :
-  ∃ s' : finset α, ↑s' = s :=
-⟨hs.to_finset, hs.coe_to_finset⟩
+@[simp, mono] lemma finite.to_finset_mono {s t : set α} {hs : s.finite} {ht : t.finite} :
+  hs.to_finset ⊆ ht.to_finset ↔ s ⊆ t :=
+begin
+  split,
+  { intros h x,
+    rw [← hs.mem_to_finset, ← ht.mem_to_finset],
+    exact λ hx, h hx },
+  { intros h x,
+    rw [hs.mem_to_finset, ht.mem_to_finset],
+    exact λ hx, h hx }
+end
 
-/-- Finite sets can be lifted to finsets. -/
-instance : can_lift (set α) (finset α) :=
-{ coe := coe,
-  cond := finite,
-  prf := λ s hs, hs.exists_finset_coe }
+@[simp, mono] lemma finite.to_finset_strict_mono {s t : set α} {hs : s.finite} {ht : t.finite} :
+  hs.to_finset ⊂ ht.to_finset ↔ s ⊂ t :=
+begin
+  rw [←lt_eq_ssubset, ←finset.lt_iff_ssubset, lt_iff_le_and_ne, lt_iff_le_and_ne],
+  simp
+end
 
-theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} :=
-⟨fintype.of_finset s (λ _, iff.rfl)⟩
+end finite_to_finset
 
-theorem finite.of_fintype [fintype α] (s : set α) : finite s :=
-by classical; exact ⟨set_fintype s⟩
 
-theorem exists_finite_iff_finset {p : set α → Prop} :
-  (∃ s, finite s ∧ p s) ↔ ∃ s : finset α, p ↑s :=
-⟨λ ⟨s, hs, hps⟩, ⟨hs.to_finset, hs.coe_to_finset.symm ▸ hps⟩,
-  λ ⟨s, hs⟩, ⟨↑s, finite_mem_finset s, hs⟩⟩
+/-! ### Fintype instances
 
-lemma finite.fin_embedding {s : set α} (h : finite s) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s :=
-⟨_, (fintype.equiv_fin (h.to_finset : set α)).symm.as_embedding, by simp⟩
+Every instance here should have a corresponding `set.finite` constructor in the next section.
+ -/
 
-lemma finite.fin_param {s : set α} (h : finite s) :
-  ∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=
-let ⟨n, f, hf⟩ := h.fin_embedding in ⟨n, f, f.injective, hf⟩
+section fintype_instances
 
-/-- Membership of a subset of a finite type is decidable.
+instance fintype_univ [fintype α] : fintype (@univ α) :=
+fintype.of_equiv α (equiv.set.univ α).symm
 
-Using this as an instance leads to potential loops with `subtype.fintype` under certain decidability
-assumptions, so it should only be declared a local instance. -/
-def decidable_mem_of_fintype [decidable_eq α] (s : set α) [fintype s] (a) : decidable (a ∈ s) :=
-decidable_of_iff _ mem_to_finset
+/-- If `(set.univ : set α)` is finite then `α` is a finite type. -/
+noncomputable def fintype_of_finite_univ (H : (univ : set α).finite) : fintype α :=
+@fintype.of_equiv _ (univ : set α) H.fintype (equiv.set.univ _)
 
-instance fintype_empty : fintype (∅ : set α) :=
-fintype.of_finset ∅ $ by simp
+instance fintype_union [decidable_eq α] (s t : set α) [fintype s] [fintype t] :
+  fintype (s ∪ t : set α) := fintype.of_finset (s.to_finset ∪ t.to_finset) $ by simp
 
-theorem empty_card : fintype.card (∅ : set α) = 0 := rfl
+instance fintype_sep (s : set α) (p : α → Prop) [fintype s] [decidable_pred p] :
+  fintype ({a ∈ s | p a} : set α) := fintype.of_finset (s.to_finset.filter p) $ by simp
 
-@[simp] theorem empty_card' {h : fintype.{u} (∅ : set α)} :
-  @fintype.card (∅ : set α) h = 0 :=
-eq.trans (by congr) empty_card
+instance fintype_inter (s t : set α) [decidable_eq α] [fintype s] [fintype t] :
+  fintype (s ∩ t : set α) := fintype.of_finset (s.to_finset ∩ t.to_finset) $ by simp
 
-@[simp] theorem finite_empty : @finite α ∅ := ⟨set.fintype_empty⟩
+/-- A `fintype` instance for set intersection where the left set has a `fintype` instance. -/
+instance fintype_inter_of_left (s t : set α) [fintype s] [decidable_pred (∈ t)] :
+  fintype (s ∩ t : set α) := fintype.of_finset (s.to_finset.filter (∈ t)) $ by simp
 
-instance finite.inhabited : inhabited {s : set α // finite s} := ⟨⟨∅, finite_empty⟩⟩
+/-- A `fintype` instance for set intersection where the right set has a `fintype` instance. -/
+instance fintype_inter_of_right (s t : set α) [fintype t] [decidable_pred (∈ s)] :
+  fintype (s ∩ t : set α) := fintype.of_finset (t.to_finset.filter (∈ s)) $ by simp [and_comm]
 
-/-- A `fintype` structure on `insert a s`. -/
-def fintype_insert' {a : α} (s : set α) [fintype s] (h : a ∉ s) : fintype (insert a s : set α) :=
-fintype.of_finset ⟨a ::ₘ s.to_finset.1, s.to_finset.nodup.cons (by simp [h]) ⟩ $ by simp
+/-- A `fintype` structure on a set defines a `fintype` structure on its subset. -/
+def fintype_subset (s : set α) {t : set α} [fintype s] [decidable_pred (∈ t)] (h : t ⊆ s) :
+  fintype t :=
+by { rw ← inter_eq_self_of_subset_right h, apply set.fintype_inter_of_left }
 
-theorem card_fintype_insert' {a : α} (s : set α) [fintype s] (h : a ∉ s) :
-  @fintype.card _ (fintype_insert' s h) = fintype.card s + 1 :=
-by rw [fintype_insert', fintype.card_of_finset];
-   simp [finset.card, to_finset]; refl
+instance fintype_diff [decidable_eq α] (s t : set α) [fintype s] [fintype t] :
+  fintype (s \ t : set α) := fintype.of_finset (s.to_finset \ t.to_finset) $ by simp
 
-@[simp] theorem card_insert {a : α} (s : set α)
-  [fintype s] (h : a ∉ s) {d : fintype.{u} (insert a s : set α)} :
-  @fintype.card _ d = fintype.card s + 1 :=
-by rw ← card_fintype_insert' s h; congr
+instance fintype_diff_left (s t : set α) [fintype s] [decidable_pred (∈ t)] :
+  fintype (s \ t : set α) := set.fintype_sep s (∈ tᶜ)
 
-lemma card_image_of_inj_on {s : set α} [fintype s]
-  {f : α → β} [fintype (f '' s)] (H : ∀x∈s, ∀y∈s, f x = f y → x = y) :
-  fintype.card (f '' s) = fintype.card s :=
-by haveI := classical.prop_decidable; exact
-calc fintype.card (f '' s) = (s.to_finset.image f).card : fintype.card_of_finset' _ (by simp)
-... = s.to_finset.card : finset.card_image_of_inj_on
-    (λ x hx y hy hxy, H x (mem_to_finset.1 hx) y (mem_to_finset.1 hy) hxy)
-... = fintype.card s : (fintype.card_of_finset' _ (λ a, mem_to_finset)).symm
+instance fintype_Union [decidable_eq α] [fintype (plift ι)]
+  (f : ι → set α) [∀ i, fintype (f i)] : fintype (⋃ i, f i) :=
+fintype.of_finset (finset.univ.bUnion (λ i : plift ι, (f i.down).to_finset)) $ by simp
 
-lemma card_image_of_injective (s : set α) [fintype s]
-  {f : α → β} [fintype (f '' s)] (H : function.injective f) :
-  fintype.card (f '' s) = fintype.card s :=
-card_image_of_inj_on $ λ _ _ _ _ h, H h
+instance fintype_sUnion [decidable_eq α] {s : set (set α)}
+  [fintype s] [H : ∀ (t : s), fintype (t : set α)] : fintype (⋃₀ s) :=
+by { rw sUnion_eq_Union, exact @set.fintype_Union _ _ _ _ _ H }
 
-section
+/-- A union of sets with `fintype` structure over a set with `fintype` structure has a `fintype`
+structure. -/
+def fintype_bUnion [decidable_eq α] {ι : Type*} (s : set ι) [fintype s]
+  (t : ι → set α) (H : ∀ i ∈ s, fintype (t i)) : fintype (⋃(x ∈ s), t x) :=
+fintype.of_finset
+(s.to_finset.attach.bUnion
+  (λ x, by { haveI := H x (by simpa using x.property), exact (t x).to_finset })) $ by simp
 
-local attribute [instance] decidable_mem_of_fintype
+instance fintype_bUnion' [decidable_eq α] {ι : Type*} (s : set ι) [fintype s]
+  (t : ι → set α) [∀ i, fintype (t i)] : fintype (⋃(x ∈ s), t x) :=
+fintype.of_finset (s.to_finset.bUnion (λ x, (t x).to_finset)) $ by simp
 
-instance fintype_insert [decidable_eq α] (a : α) (s : set α) [fintype s] :
-  fintype (insert a s : set α) :=
-if h : a ∈ s then by rwa [insert_eq, union_eq_self_of_subset_left (singleton_subset_iff.2 h)]
-else fintype_insert' _ h
+/-- If `s : set α` is a set with `fintype` instance and `f : α → set β` is a function such that
+each `f a`, `a ∈ s`, has a `fintype` structure, then `s >>= f` has a `fintype` structure. -/
+def fintype_bind {α β} [decidable_eq β] (s : set α) [fintype s]
+  (f : α → set β) (H : ∀ a ∈ s, fintype (f a)) : fintype (s >>= f) :=
+set.fintype_bUnion s f H
 
-end
+instance fintype_bind' {α β} [decidable_eq β] (s : set α) [fintype s]
+  (f : α → set β) [H : ∀ a, fintype (f a)] : fintype (s >>= f) :=
+set.fintype_bUnion' s f
 
-@[simp] theorem finite.insert (a : α) {s : set α} : finite s → finite (insert a s)
-| ⟨h⟩ := ⟨@set.fintype_insert _ (classical.dec_eq α) _ _ h⟩
+instance fintype_empty : fintype (∅ : set α) := fintype.of_finset ∅ $ by simp
 
-lemma to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : finite s) :
-  (hs.insert a).to_finset = insert a hs.to_finset :=
-finset.ext $ by simp
+instance fintype_singleton (a : α) : fintype ({a} : set α) := fintype.of_finset {a} $ by simp
 
-@[simp] lemma insert_to_finset [decidable_eq α] {a : α} {s : set α} [fintype s] :
-  (insert a s).to_finset = insert a s.to_finset :=
-by simp [finset.ext_iff, mem_insert_iff]
+instance fintype_pure : ∀ a : α, fintype (pure a : set α) :=
+set.fintype_singleton
 
-@[elab_as_eliminator]
-theorem finite.induction_on {C : set α → Prop} {s : set α} (h : finite s)
-  (H0 : C ∅) (H1 : ∀ {a s}, a ∉ s → finite s → C s → C (insert a s)) : C s :=
-let ⟨t⟩ := h in by exactI
-match s.to_finset, @mem_to_finset _ s _ with
-| ⟨l, nd⟩, al := begin
-    change ∀ a, a ∈ l ↔ a ∈ s at al,
-    clear _let_match _match t h, revert s nd al,
-    refine multiset.induction_on l _ (λ a l IH, _); intros s nd al,
-    { rw show s = ∅, from eq_empty_iff_forall_not_mem.2 (by simpa using al),
-      exact H0 },
-    { rw ← show insert a {x | x ∈ l} = s, from set.ext (by simpa using al),
-      cases multiset.nodup_cons.1 nd with m nd',
-      refine H1 _ ⟨finset.subtype.fintype ⟨l, nd'⟩⟩ (IH nd' (λ _, iff.rfl)),
-      exact m }
-  end
-end
+/-- A `fintype` structure on `insert a s` when inserting a new element. -/
+def fintype_insert_of_not_mem {a : α} (s : set α) [fintype s] (h : a ∉ s) :
+  fintype (insert a s : set α) :=
+fintype.of_finset ⟨a ::ₘ s.to_finset.1, s.to_finset.nodup.cons (by simp [h]) ⟩ $ by simp
 
-@[elab_as_eliminator]
-theorem finite.dinduction_on {C : ∀s:set α, finite s → Prop} {s : set α} (h : finite s)
-  (H0 : C ∅ finite_empty)
-  (H1 : ∀ {a s}, a ∉ s → ∀ h : finite s, C s h → C (insert a s) (h.insert a)) :
-  C s h :=
-have ∀ h : finite s, C s h,
-  from finite.induction_on h (λ h, H0) (λ a s has hs ih h, H1 has hs (ih _)),
-this h
+/-- A `fintype` structure on `insert a s` when inserting a pre-existing element. -/
+def fintype_insert_of_mem {a : α} (s : set α) [fintype s] (h : a ∈ s) :
+  fintype (insert a s : set α) :=
+fintype.of_finset s.to_finset $ by simp [h]
 
-instance fintype_singleton (a : α) : fintype ({a} : set α) :=
-unique.fintype
+instance fintype_insert (a : α) (s : set α) [decidable_eq α] [fintype s] :
+  fintype (insert a s : set α) :=
+fintype.of_finset (insert a s.to_finset) $ by simp
 
-@[simp] theorem card_singleton (a : α) :
-  fintype.card ({a} : set α) = 1 :=
-fintype.card_of_subsingleton _
+/-- Normally, `insert a s` for `finset` requires `[decidable_eq α]`, but we can use this weaker
+assumption here. -/
+instance fintype_insert' (a : α) (s : set α) [decidable $ a ∈ s] [fintype s] :
+  fintype (insert a s : set α) :=
+if h : a ∈ s then fintype_insert_of_mem s h else fintype_insert_of_not_mem s h
 
-@[simp] theorem finite_singleton (a : α) : finite ({a} : set α) :=
-⟨set.fintype_singleton _⟩
+instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
+fintype.of_finset (s.to_finset.image f) $ by simp
 
-lemma subsingleton.finite {s : set α} (h : s.subsingleton) : finite s :=
-h.induction_on finite_empty finite_singleton
+/-- If a function `f` has a partial inverse and sends a set `s` to a set with `[fintype]` instance,
+then `s` has a `fintype` structure as well. -/
+def fintype_of_fintype_image (s : set α)
+  {f : α → β} {g} (I : is_partial_inv f g) [fintype (f '' s)] : fintype s :=
+fintype.of_finset ⟨_, (f '' s).to_finset.2.filter_map g $ injective_of_partial_inv_right I⟩ $ λ a,
+begin
+  suffices : (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s,
+  by simpa [exists_and_distrib_left.symm, and.comm, and.left_comm, and.assoc],
+  rw exists_swap,
+  suffices : (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s, {simpa [and.comm, and.left_comm, and.assoc]},
+  simp [I _, (injective_of_partial_inv I).eq_iff]
+end
 
-lemma to_finset_singleton (a : α) : ({a} : set α).to_finset = {a} := rfl
+instance fintype_range [decidable_eq α] (f : ι → α) [fintype (plift ι)] :
+  fintype (range f) :=
+fintype.of_finset (finset.univ.image $ f ∘ plift.down) $ by simp [equiv.plift.exists_congr_left]
 
-lemma finite_is_top (α : Type*) [partial_order α] : finite {x : α | is_top x} :=
-(subsingleton_is_top α).finite
+instance fintype_map {α β} [decidable_eq β] :
+  ∀ (s : set α) (f : α → β) [fintype s], fintype (f <$> s) := set.fintype_image
 
-lemma finite_is_bot (α : Type*) [partial_order α] : finite {x : α | is_bot x} :=
-(subsingleton_is_bot α).finite
+instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
+fintype.of_finset (finset.range n) $ by simp
 
-instance fintype_pure : ∀ a : α, fintype (pure a : set α) :=
-set.fintype_singleton
+instance fintype_le_nat (n : ℕ) : fintype {i | i ≤ n} :=
+by simpa [nat.lt_succ_iff] using set.fintype_lt_nat (n+1)
 
-theorem finite_pure (a : α) : finite (pure a : set α) :=
-⟨set.fintype_pure a⟩
+/-- This is not an instance so that it does not conflict with the one
+in src/order/locally_finite. -/
+def nat.fintype_Iio (n : ℕ) : fintype (Iio n) :=
+set.fintype_lt_nat n
 
-instance fintype_univ [fintype α] : fintype (@univ α) :=
-fintype.of_equiv α $ (equiv.set.univ α).symm
+instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] :
+  fintype (s ×ˢ t : set (α × β)) :=
+fintype.of_finset (s.to_finset.product t.to_finset) $ by simp
 
-theorem finite_univ [fintype α] : finite (@univ α) := ⟨set.fintype_univ⟩
+/-- `image2 f s t` is `fintype` if `s` and `t` are. -/
+instance fintype_image2 [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β)
+  [hs : fintype s] [ht : fintype t] : fintype (image2 f s t : set γ) :=
+by { rw ← image_prod, apply set.fintype_image }
 
-/-- If `(set.univ : set α)` is finite then `α` is a finite type. -/
-noncomputable def fintype_of_univ_finite (H : (univ : set α).finite ) :
-  fintype α :=
-@fintype.of_equiv _ (univ : set α) H.fintype (equiv.set.univ _)
+instance fintype_seq [decidable_eq β] (f : set (α → β)) (s : set α) [fintype f] [fintype s] :
+  fintype (f.seq s) :=
+by { rw seq_def, apply set.fintype_bUnion' }
 
-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
+instance fintype_seq' {α β : Type u} [decidable_eq β]
+  (f : set (α → β)) (s : set α) [fintype f] [fintype s] : fintype (f <*> s) :=
+set.fintype_seq f s
 
-theorem infinite_univ_iff : (@univ α).infinite ↔ _root_.infinite α :=
-⟨λ h₁, ⟨λ h₂, h₁ $ @finite_univ α h₂⟩, λ ⟨h₁⟩ h₂, h₁ (fintype_of_univ_finite h₂)⟩
+instance fintype_mem_finset (s : finset α) : fintype {a | a ∈ s} :=
+finset.fintype_coe_sort s
 
-theorem infinite_univ [h : _root_.infinite α] : infinite (@univ α) :=
-infinite_univ_iff.2 h
+end fintype_instances
 
-theorem infinite_coe_iff {s : set α} : _root_.infinite s ↔ infinite s :=
-⟨λ ⟨h₁⟩ h₂, h₁ h₂.fintype, λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩⟩
 
-theorem infinite.to_subtype {s : set α} (h : infinite s) : _root_.infinite s :=
-infinite_coe_iff.2 h
+/-! ### Constructors for `set.finite`
 
-/-- Embedding of `ℕ` into an infinite set. -/
-noncomputable def infinite.nat_embedding (s : set α) (h : infinite s) : ℕ ↪ s :=
-by { haveI := h.to_subtype, exact infinite.nat_embedding s }
+Every constructor here should have a corresponding `fintype` instance in the previous section
+(or in the `fintype` module).
 
-lemma infinite.exists_subset_card_eq {s : set α} (hs : infinite s) (n : ℕ) :
-  ∃ t : finset α, ↑t ⊆ s ∧ t.card = n :=
-⟨((finset.range n).map (hs.nat_embedding _)).map (embedding.subtype _), by simp⟩
+The implementation of these constructors ideally should be no more than `set.finite_of_fintype`,
+after possibly setting up some `fintype` and classical `decidable` instances.
+-/
+section set_finite_constructors
 
-lemma infinite.nonempty {s : set α} (h : s.infinite) : s.nonempty :=
-let a := infinite.nat_embedding s h 37 in ⟨a.1, a.2⟩
+theorem finite.of_fintype [fintype α] (s : set α) : s.finite :=
+by { classical, apply finite_of_fintype }
 
-instance fintype_union [decidable_eq α] (s t : set α) [fintype s] [fintype t] :
-  fintype (s ∪ t : set α) :=
-fintype.of_finset (s.to_finset ∪ t.to_finset) $ by simp
+theorem finite_univ [fintype α] : (@univ α).finite := finite_of_fintype _
 
-theorem finite.union {s t : set α} : finite s → finite t → finite (s ∪ t)
-| ⟨hs⟩ ⟨ht⟩ := ⟨@set.fintype_union _ (classical.dec_eq α) _ _ hs ht⟩
+theorem finite.union {s t : set α} (hs : s.finite) (ht : t.finite) : (s ∪ t).finite :=
+by { classical, casesI hs, casesI ht, apply finite_of_fintype }
 
 lemma finite.sup {s t : set α} : finite s → finite t → finite (s ⊔ t) := finite.union
 
-lemma infinite_of_finite_compl [_root_.infinite α] {s : set α}
-  (hs : sᶜ.finite) : s.infinite :=
-λ h, set.infinite_univ (by simpa using hs.union h)
+theorem finite.sep {s : set α} (hs : s.finite) (p : α → Prop) : {a ∈ s | p a}.finite :=
+by { classical, casesI hs, apply finite_of_fintype }
 
-lemma finite.infinite_compl [_root_.infinite α] {s : set α}
-  (hs : s.finite) : sᶜ.infinite :=
-λ h, set.infinite_univ (by simpa using hs.union h)
+theorem finite.inter_of_left {s : set α} (hs : s.finite) (t : set α) : (s ∩ t).finite :=
+by { classical, casesI hs, apply finite_of_fintype }
 
-instance fintype_sep (s : set α) (p : α → Prop) [fintype s] [decidable_pred p] :
-  fintype ({a ∈ s | p a} : set α) :=
-fintype.of_finset (s.to_finset.filter p) $ by simp
+theorem finite.inter_of_right {s : set α} (hs : s.finite) (t : set α) : (t ∩ s).finite :=
+by { classical, casesI hs, apply finite_of_fintype }
 
-instance fintype_inter (s t : set α) [fintype s] [decidable_pred (∈ t)] : fintype (s ∩ t : set α) :=
-set.fintype_sep s t
+theorem finite.inf_of_left {s : set α} (h : finite s) (t : set α) : finite (s ⊓ t) :=
+h.inter_of_left t
 
-/-- A `fintype` structure on a set defines a `fintype` structure on its subset. -/
-def fintype_subset (s : set α) {t : set α} [fintype s] [decidable_pred (∈ t)] (h : t ⊆ s) :
-  fintype t :=
-by rw ← inter_eq_self_of_subset_right h; apply_instance
+theorem finite.inf_of_right {s : set α} (h : finite s) (t : set α) : finite (t ⊓ s) :=
+h.inter_of_right t
 
-theorem finite.subset {s : set α} : finite s → ∀ {t : set α}, t ⊆ s → finite t
-| ⟨hs⟩ t h := ⟨@set.fintype_subset _ _ _ hs (classical.dec_pred t) h⟩
+theorem finite.subset {s : set α} (hs : s.finite) {t : set α} (ht : t ⊆ s) : t.finite :=
+by { classical, casesI hs, haveI := set.fintype_subset _ ht, apply finite_of_fintype }
 
-@[simp] lemma finite_union {s t : set α} : finite (s ∪ t) ↔ finite s ∧ finite t :=
-⟨λ h, ⟨h.subset (subset_union_left _ _), h.subset (subset_union_right _ _)⟩,
- λ ⟨hs, ht⟩, hs.union ht⟩
+theorem finite.diff {s : set α} (hs : s.finite) (t : set α) : (s \ t).finite :=
+by { classical, casesI hs, apply finite_of_fintype }
 
-lemma finite.of_diff {s t : set α} (hd : finite (s \ t)) (ht : finite t) : finite s :=
+theorem finite.of_diff {s t : set α} (hd : finite (s \ t)) (ht : finite t) : finite s :=
 (hd.union ht).subset $ subset_diff_union _ _
 
-theorem finite.inter_of_left {s : set α} (h : finite s) (t : set α) : finite (s ∩ t) :=
-h.subset (inter_subset_left _ _)
+theorem finite_Union [fintype (plift ι)] {f : ι → set α} (H : ∀ i, (f i).finite) :
+  (⋃ i, f i).finite :=
+by { classical, haveI := λ i, (H i).fintype, apply finite_of_fintype }
 
-theorem finite.inter_of_right {s : set α} (h : finite s) (t : set α) : finite (t ∩ s) :=
-h.subset (inter_subset_right _ _)
+theorem finite.sUnion {s : set (set α)} (hs : s.finite) (H : ∀ t ∈ s, finite t) : (⋃₀ s).finite :=
+by { classical, casesI hs, haveI := λ (i : s), (H i i.2).fintype, apply finite_of_fintype }
 
-theorem finite.inf_of_left {s : set α} (h : finite s) (t : set α) : finite (s ⊓ t) :=
-h.inter_of_left t
+theorem finite.bUnion {ι} {s : set ι} (hs : s.finite)
+  {t : ι → set α} (ht : ∀ i ∈ s, (t i).finite) : (⋃(i ∈ s), t i).finite :=
+by { classical, casesI hs,
+     haveI := fintype_bUnion s t (λ i hi, (ht i hi).fintype), apply finite_of_fintype }
 
-theorem finite.inf_of_right {s : set α} (h : finite s) (t : set α) : finite (t ⊓ s) :=
-h.inter_of_right t
+/-- Dependent version of `finite.bUnion`. -/
+theorem finite.bUnion' {ι} {s : set ι} (hs : s.finite)
+  {t : Π (i ∈ s), set α} (ht : ∀ i ∈ s, (t i ‹_›).finite) : (⋃(i ∈ s), t i ‹_›).finite :=
+by { casesI hs, rw [bUnion_eq_Union], apply finite_Union (λ (i : s), ht i.1 i.2), }
 
-lemma finite.sInter {α : Type*} {s : set (set α)} {t : set α} (ht : t ∈ s)
-  (hf : t.finite) : (⋂₀s).finite :=
+theorem finite.sInter {α : Type*} {s : set (set α)} {t : set α} (ht : t ∈ s)
+  (hf : t.finite) : (⋂₀ s).finite :=
 hf.subset (sInter_subset_of_mem ht)
 
-protected theorem infinite.mono {s t : set α} (h : s ⊆ t) : infinite s → infinite t :=
-mt (λ ht, ht.subset h)
-
-lemma infinite.diff {s t : set α} (hs : s.infinite) (ht : t.finite) :
-  (s \ t).infinite :=
-λ h, hs $ h.of_diff ht
+theorem finite.bind {α β} {s : set α} {f : α → set β} (h : s.finite) (hf : ∀ a ∈ s, (f a).finite) :
+  finite (s >>= f) :=
+h.bUnion hf
 
-@[simp] lemma infinite_union {s t : set α} : infinite (s ∪ t) ↔ infinite s ∨ infinite t :=
-by simp only [infinite, finite_union, not_and_distrib]
+@[simp] theorem finite_empty : (∅ : set α).finite := finite_of_fintype _
 
-instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
-fintype.of_finset (s.to_finset.image f) $ by simp
+@[simp] theorem finite_singleton (a : α) : ({a} : set α).finite := finite_of_fintype _
 
-instance fintype_range [decidable_eq α] (f : ι → α) [fintype (plift ι)] :
-  fintype (range f) :=
-fintype.of_finset (finset.univ.image $ f ∘ plift.down) $
-  by simp [(@equiv.plift ι).exists_congr_left]
+theorem finite_pure (a : α) : (pure a : set α).finite := finite_of_fintype _
 
-theorem finite_range (f : ι → α) [fintype (plift ι)] : finite (range f) :=
-by haveI := classical.dec_eq α; exact ⟨by apply_instance⟩
+@[simp] theorem finite.insert (a : α) {s : set α} (hs : s.finite) : (insert a s).finite :=
+by { classical, casesI hs, apply finite_of_fintype }
 
-theorem finite.image {s : set α} (f : α → β) : finite s → finite (f '' s)
-| ⟨h⟩ := ⟨@set.fintype_image _ _ (classical.dec_eq β) _ _ h⟩
+theorem finite.image {s : set α} (f : α → β) (hs : s.finite) : (f '' s).finite :=
+by { classical, casesI hs, apply finite_of_fintype }
 
-theorem infinite_of_infinite_image (f : α → β) {s : set α} (hs : (f '' s).infinite) :
-  s.infinite :=
-mt (finite.image f) hs
+theorem finite_range (f : ι → α) [fintype (plift ι)] : (range f).finite :=
+by { classical, apply finite_of_fintype }
 
-lemma finite.dependent_image {s : set α} (hs : finite s) (F : Π i ∈ s, β) :
+lemma finite.dependent_image {s : set α} (hs : s.finite) (F : Π i ∈ s, β) :
   finite {y : β | ∃ x (hx : x ∈ s), y = F x hx} :=
-begin
-  letI : fintype s := hs.fintype,
-  convert finite_range (λ x : s, F x x.2),
-  simp only [set_coe.exists, subtype.coe_mk, eq_comm],
-end
+by { casesI hs, simpa [range, eq_comm] using finite_range (λ x : s, F x x.2) }
+
+theorem finite.map {α β} {s : set α} : ∀ (f : α → β), finite s → finite (f <$> s) :=
+finite.image
+
+theorem finite.of_finite_image {s : set α} {f : α → β} (h : (f '' s).finite) (hi : set.inj_on f s) :
+  finite s :=
+by { casesI h, exact ⟨fintype.of_injective (λ a, (⟨f a.1, mem_image_of_mem f a.2⟩ : f '' s))
+                       (λ a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext_iff_val.1 eq)⟩ }
 
-theorem finite.of_preimage {f : α → β} {s : set β} (h : finite (f ⁻¹' s)) (hf : surjective f) :
+theorem finite.of_preimage {f : α → β} {s : set β} (h : (f ⁻¹' s).finite) (hf : surjective f) :
   finite s :=
 hf.image_preimage s ▸ h.image _
 
-instance fintype_map {α β} [decidable_eq β] :
-  ∀ (s : set α) (f : α → β) [fintype s], fintype (f <$> s) := set.fintype_image
+theorem finite.preimage {s : set β} {f : α → β}
+  (I : set.inj_on f (f⁻¹' s)) (h : finite s) : finite (f ⁻¹' s) :=
+(h.subset (image_preimage_subset f s)).of_finite_image I
 
-theorem finite.map {α β} {s : set α} :
-  ∀ (f : α → β), finite s → finite (f <$> s) := finite.image
+theorem finite.preimage_embedding {s : set β} (f : α ↪ β) (h : s.finite) : (f ⁻¹' s).finite :=
+h.preimage (λ _ _ _ _ h', f.injective h')
 
-/-- If a function `f` has a partial inverse and sends a set `s` to a set with `[fintype]` instance,
-then `s` has a `fintype` structure as well. -/
-def fintype_of_fintype_image (s : set α)
-  {f : α → β} {g} (I : is_partial_inv f g) [fintype (f '' s)] : fintype s :=
-fintype.of_finset ⟨_, (f '' s).to_finset.2.filter_map g $ injective_of_partial_inv_right I⟩ $ λ a,
+lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := finite_of_fintype _
+
+lemma finite_le_nat (n : ℕ) : finite {i | i ≤ n} := finite_of_fintype _
+
+lemma finite.prod {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
+  (s ×ˢ t : set (α × β)).finite :=
+by { classical, casesI hs, casesI ht, apply finite_of_fintype }
+
+lemma finite.image2 (f : α → β → γ) {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
+  finite (image2 f s t) :=
+by { classical, casesI hs, casesI ht, apply finite_of_fintype }
+
+theorem finite.seq {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) :
+  finite (f.seq s) :=
+by { classical, casesI hf, casesI hs, apply finite_of_fintype }
+
+theorem finite.seq' {α β : Type u} {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) :
+  finite (f <*> s) :=
+hf.seq hs
+
+theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} := finite_of_fintype _
+
+lemma subsingleton.finite {s : set α} (h : s.subsingleton) : finite s :=
+h.induction_on finite_empty finite_singleton
+
+theorem exists_finite_iff_finset {p : set α → Prop} :
+  (∃ s : set α, s.finite ∧ p s) ↔ ∃ s : finset α, p ↑s :=
+⟨λ ⟨s, hs, hps⟩, ⟨hs.to_finset, hs.coe_to_finset.symm ▸ hps⟩,
+  λ ⟨s, hs⟩, ⟨↑s, finite_mem_finset s, hs⟩⟩
+
+/-- There are finitely many subsets of a given finite set -/
+lemma finite.finite_subsets {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} :=
+⟨fintype.of_finset ((finset.powerset h.to_finset).map finset.coe_emb.1) $ λ s,
+  by simpa [← @exists_finite_iff_finset α (λ t, t ⊆ a ∧ t = s), subset_to_finset_iff,
+    ← and.assoc] using h.subset⟩
+
+/-- Finite product of finite sets is finite -/
+lemma finite.pi {δ : Type*} [fintype δ] {κ : δ → Type*} {t : Π d, set (κ d)}
+  (ht : ∀ d, (t d).finite) :
+  (pi univ t).finite :=
 begin
-  suffices : (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s,
-  by simpa [exists_and_distrib_left.symm, and.comm, and.left_comm, and.assoc],
-  rw exists_swap,
-  suffices : (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s, {simpa [and.comm, and.left_comm, and.assoc]},
-  simp [I _, (injective_of_partial_inv I).eq_iff]
+  lift t to Π d, finset (κ d) using ht,
+  classical,
+  rw ← fintype.coe_pi_finset,
+  exact finite_of_fintype (fintype.pi_finset t),
 end
 
-theorem finite_of_finite_image {s : set α} {f : α → β} (hi : set.inj_on f s) :
-  finite (f '' s) → finite s | ⟨h⟩ :=
-⟨@fintype.of_injective _ _ h (λ a : s, ⟨f a.1, mem_image_of_mem f a.2⟩) $
-  λ a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext_iff_val.1 eq⟩
+/-- A finite union of finsets is finite. -/
+lemma union_finset_finite_of_range_finite (f : α → finset β) (h : (range f).finite) :
+  (⋃ a, (f a : set β)).finite :=
+by { rw ← bUnion_range, exact h.bUnion (λ y hy, finite_of_fintype y) }
+
+lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))
+  (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) :=
+(hf.union hg).subset range_ite_subset
+
+lemma finite_range_const {c : β} : finite (range (λ x : α, c)) :=
+(finite_singleton c).subset range_const_subset
+
+end set_finite_constructors
+
+
+/-! ### Properties -/
+
+instance finite.inhabited : inhabited {s : set α // s.finite} := ⟨⟨∅, finite_empty⟩⟩
+
+@[simp] lemma finite_union {s t : set α} : (s ∪ t).finite ↔ s.finite ∧ t.finite :=
+⟨λ h, ⟨h.subset (subset_union_left _ _), h.subset (subset_union_right _ _)⟩,
+ λ ⟨hs, ht⟩, hs.union ht⟩
 
 theorem finite_image_iff {s : set α} {f : α → β} (hi : inj_on f s) :
-  finite (f '' s) ↔ finite s :=
-⟨finite_of_finite_image hi, finite.image _⟩
+  (f '' s).finite ↔ s.finite :=
+⟨λ h, h.of_finite_image hi, finite.image _⟩
 
-theorem infinite_image_iff {s : set α} {f : α → β} (hi : inj_on f s) :
-  infinite (f '' s) ↔ infinite s :=
-not_congr $ finite_image_iff hi
+lemma univ_finite_iff_nonempty_fintype :
+  (univ : set α).finite ↔ nonempty (fintype α) :=
+⟨λ h, ⟨fintype_of_finite_univ h⟩, λ ⟨_i⟩, by exactI finite_univ⟩
 
-theorem infinite_of_inj_on_maps_to {s : set α} {t : set β} {f : α → β}
-  (hi : inj_on f s) (hm : maps_to f s t) (hs : infinite s) : infinite t :=
-((infinite_image_iff hi).2 hs).mono (maps_to'.mp hm)
+lemma finite.to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :
+  (hs.insert a).to_finset = insert a hs.to_finset :=
+finset.ext $ by simp
 
-theorem infinite.exists_ne_map_eq_of_maps_to {s : set α} {t : set β} {f : α → β}
-  (hs : infinite s) (hf : maps_to f s t) (ht : finite t) :
-  ∃ (x ∈ s) (y ∈ s), x ≠ y ∧ f x = f y :=
+lemma finite.fin_embedding {s : set α} (h : finite s) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s :=
+⟨_, (fintype.equiv_fin (h.to_finset : set α)).symm.as_embedding, by simp⟩
+
+lemma finite.fin_param {s : set α} (h : s.finite) :
+  ∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=
+let ⟨n, f, hf⟩ := h.fin_embedding in ⟨n, f, f.injective, hf⟩
+
+lemma finite_option {s : set (option α)} : s.finite ↔ finite {x : α | some x ∈ s} :=
+⟨λ h, h.preimage_embedding embedding.some,
+  λ h, ((h.image some).insert none).subset $
+    λ x, option.cases_on x (λ _, or.inl rfl) (λ x hx, or.inr $ mem_image_of_mem _ hx)⟩
+
+lemma finite_image_fst_and_snd_iff {s : set (α × β)} :
+  (prod.fst '' s).finite ∧ (prod.snd '' s).finite ↔ s.finite :=
+⟨λ 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)} :
+  (∀ d, (eval d '' s).finite) ↔ s.finite :=
+⟨λ h, (finite.pi h).subset $ subset_pi_eval_image _ _, λ h d, h.image _⟩
+
+lemma finite_subset_Union {s : set α} (hs : finite s)
+  {ι} {t : ι → set α} (h : s ⊆ ⋃ i, t i) : ∃ I : set ι, I.finite ∧ s ⊆ ⋃ i ∈ I, t i :=
 begin
-  contrapose! ht,
-  exact infinite_of_inj_on_maps_to (λ x hx y hy, not_imp_not.1 (ht x hx y hy)) hf hs
+  casesI hs,
+  choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i, {simpa [subset_def] using h},
+  refine ⟨range f, finite_range f, λ x hx, _⟩,
+  rw [bUnion_range, mem_Union],
+  exact ⟨⟨x, hx⟩, hf _⟩
 end
 
-theorem infinite.exists_lt_map_eq_of_maps_to [linear_order α] {s : set α} {t : set β} {f : α → β}
-  (hs : infinite s) (hf : maps_to f s t) (ht : finite t) :
-  ∃ (x ∈ s) (y ∈ s), x < y ∧ f x = f y :=
-let ⟨x, hx, y, hy, hxy, hf⟩ := hs.exists_ne_map_eq_of_maps_to hf ht
-in hxy.lt_or_lt.elim (λ hxy, ⟨x, hx, y, hy, hxy, hf⟩) (λ hyx, ⟨y, hy, x, hx, hyx, hf.symm⟩)
+lemma eq_finite_Union_of_finite_subset_Union  {ι} {s : ι → set α} {t : set α} (tfin : t.finite)
+  (h : t ⊆ ⋃ i, s i) :
+  ∃ I : set ι, I.finite ∧ ∃ σ : {i | i ∈ I} → set α,
+     (∀ i, (σ i).finite) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i :=
+let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
+⟨I, Ifin, λ x, s x ∩ t,
+    λ i, tfin.subset (inter_subset_right _ _),
+    λ i, inter_subset_left _ _,
+    begin
+      ext x,
+      rw mem_Union,
+      split,
+      { intro x_in,
+        rcases mem_Union.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩,
+        use [i, hi, H, x_in] },
+      { rintros ⟨i, hi, H⟩,
+        exact H }
+    end⟩
 
-lemma finite.exists_lt_map_eq_of_range_subset [linear_order α] [_root_.infinite α] {t : set β}
-  {f : α → β} (hf : range f ⊆ t) (ht : finite t) :
-  ∃ a b, a < b ∧ f a = f b :=
+@[elab_as_eliminator]
+theorem finite.induction_on {C : set α → Prop} {s : set α} (h : s.finite)
+  (H0 : C ∅) (H1 : ∀ {a s}, a ∉ s → finite s → C s → C (insert a s)) : C s :=
+let ⟨t⟩ := h in by exactI
+match s.to_finset, @mem_to_finset _ s _ with
+| ⟨l, nd⟩, al := begin
+    change ∀ a, a ∈ l ↔ a ∈ s at al,
+    clear _let_match _match t h, revert s nd al,
+    refine multiset.induction_on l _ (λ a l IH, _); intros s nd al,
+    { rw show s = ∅, from eq_empty_iff_forall_not_mem.2 (by simpa using al),
+      exact H0 },
+    { rw ← show insert a {x | x ∈ l} = s, from set.ext (by simpa using al),
+      cases multiset.nodup_cons.1 nd with m nd',
+      refine H1 _ ⟨finset.subtype.fintype ⟨l, nd'⟩⟩ (IH nd' (λ _, iff.rfl)),
+      exact m }
+  end
+end
+
+@[elab_as_eliminator]
+theorem finite.dinduction_on {C : ∀ (s : set α), s.finite → Prop} {s : set α} (h : s.finite)
+  (H0 : C ∅ finite_empty)
+  (H1 : ∀ {a s}, a ∉ s → ∀ h : finite s, C s h → C (insert a s) (h.insert a)) :
+  C s h :=
+have ∀ h : finite s, C s h,
+  from finite.induction_on h (λ h, H0) (λ a s has hs ih h, H1 has hs (ih _)),
+this h
+
+section
+local attribute [instance] nat.fintype_Iio
+
+/--
+If `P` is some relation between terms of `γ` and sets in `γ`,
+such that every finite set `t : set γ` has some `c : γ` related to it,
+then there is a recursively defined sequence `u` in `γ`
+so `u n` is related to the image of `{0, 1, ..., n-1}` under `u`.
+
+(We use this later to show sequentially compact sets
+are totally bounded.)
+-/
+lemma seq_of_forall_finite_exists  {γ : Type*}
+  {P : γ → set γ → Prop} (h : ∀ t : set γ, t.finite → ∃ c, P c t) :
+  ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n) :=
+⟨λ n, @nat.strong_rec_on' (λ _, γ) n $ λ n ih, classical.some $ h
+    (range $ λ m : Iio n, ih m.1 m.2)
+    (finite_range _),
+λ n, begin
+  classical,
+  refine nat.strong_rec_on' n (λ n ih, _),
+  rw nat.strong_rec_on_beta', convert classical.some_spec (h _ _),
+  ext x, split,
+  { rintros ⟨m, hmn, rfl⟩, exact ⟨⟨m, hmn⟩, rfl⟩ },
+  { rintros ⟨⟨m, hmn⟩, rfl⟩, exact ⟨m, hmn, rfl⟩ }
+end⟩
+
+end
+
+
+/-! ### Cardinality -/
+
+theorem empty_card : fintype.card (∅ : set α) = 0 := rfl
+
+@[simp] theorem empty_card' {h : fintype.{u} (∅ : set α)} :
+  @fintype.card (∅ : set α) h = 0 :=
+eq.trans (by congr) empty_card
+
+theorem card_fintype_insert_of_not_mem {a : α} (s : set α) [fintype s] (h : a ∉ s) :
+  @fintype.card _ (fintype_insert_of_not_mem s h) = fintype.card s + 1 :=
+by rw [fintype_insert_of_not_mem, fintype.card_of_finset];
+   simp [finset.card, to_finset]; refl
+
+@[simp] theorem card_insert {a : α} (s : set α)
+  [fintype s] (h : a ∉ s) {d : fintype.{u} (insert a s : set α)} :
+  @fintype.card _ d = fintype.card s + 1 :=
+by rw ← card_fintype_insert_of_not_mem s h; congr
+
+lemma card_image_of_inj_on {s : set α} [fintype s]
+  {f : α → β} [fintype (f '' s)] (H : ∀x∈s, ∀y∈s, f x = f y → x = y) :
+  fintype.card (f '' s) = fintype.card s :=
+by haveI := classical.prop_decidable; exact
+calc fintype.card (f '' s) = (s.to_finset.image f).card : fintype.card_of_finset' _ (by simp)
+... = s.to_finset.card : finset.card_image_of_inj_on
+    (λ x hx y hy hxy, H x (mem_to_finset.1 hx) y (mem_to_finset.1 hy) hxy)
+... = fintype.card s : (fintype.card_of_finset' _ (λ a, mem_to_finset)).symm
+
+lemma card_image_of_injective (s : set α) [fintype s]
+  {f : α → β} [fintype (f '' s)] (H : function.injective f) :
+  fintype.card (f '' s) = fintype.card s :=
+card_image_of_inj_on $ λ _ _ _ _ h, H h
+
+@[simp] theorem card_singleton (a : α) :
+  fintype.card ({a} : set α) = 1 :=
+fintype.card_of_subsingleton _
+
+lemma card_lt_card {s t : set α} [fintype s] [fintype t] (h : s ⊂ t) :
+  fintype.card s < fintype.card t :=
+fintype.card_lt_of_injective_not_surjective (set.inclusion h.1) (set.inclusion_injective h.1) $
+  λ hst, (ssubset_iff_subset_ne.1 h).2 (eq_of_inclusion_surjective hst)
+
+lemma card_le_of_subset {s t : set α} [fintype s] [fintype t] (hsub : s ⊆ t) :
+  fintype.card s ≤ fintype.card t :=
+fintype.card_le_of_injective (set.inclusion hsub) (set.inclusion_injective hsub)
+
+lemma eq_of_subset_of_card_le {s t : set α} [fintype s] [fintype t]
+   (hsub : s ⊆ t) (hcard : fintype.card t ≤ fintype.card s) : s = t :=
+(eq_or_ssubset_of_subset hsub).elim id
+  (λ h, absurd hcard $ not_le_of_lt $ card_lt_card h)
+
+lemma card_range_of_injective [fintype α] {f : α → β} (hf : injective f)
+  [fintype (range f)] : fintype.card (range f) = fintype.card α :=
+eq.symm $ fintype.card_congr $ equiv.of_injective f hf
+
+lemma finite.card_to_finset {s : set α} [fintype s] (h : s.finite) :
+  h.to_finset.card = fintype.card s :=
 begin
-  rw [range_subset_iff, ←maps_univ_to] at hf,
-  obtain ⟨a, -, b, -, h⟩ := (@infinite_univ α _).exists_lt_map_eq_of_maps_to hf ht,
-  exact ⟨a, b, h⟩,
+  rw [← finset.card_attach, finset.attach_eq_univ, ← fintype.card],
+  refine fintype.card_congr (equiv.set_congr _),
+  ext x,
+  show x ∈ h.to_finset ↔ x ∈ s,
+  simp,
 end
 
-theorem infinite_range_of_injective [_root_.infinite α] {f : α → β} (hi : injective f) :
-  infinite (range f) :=
-by { rw [←image_univ, infinite_image_iff (inj_on_of_injective hi _)], exact infinite_univ }
+lemma card_ne_eq [fintype α] (a : α) [fintype {x : α | x ≠ a}] :
+  fintype.card {x : α | x ≠ a} = fintype.card α - 1 :=
+begin
+  haveI := classical.dec_eq α,
+  rw [←to_finset_card, to_finset_ne_eq_erase, finset.card_erase_of_mem (finset.mem_univ _),
+      finset.card_univ],
+end
 
-theorem infinite_of_injective_forall_mem [_root_.infinite α] {s : set β} {f : α → β}
-  (hi : injective f) (hf : ∀ x : α, f x ∈ s) : infinite s :=
-by { rw ←range_subset_iff at hf, exact (infinite_range_of_injective hi).mono hf }
 
-theorem finite.preimage {s : set β} {f : α → β}
-  (I : set.inj_on f (f⁻¹' s)) (h : finite s) : finite (f ⁻¹' s) :=
-finite_of_finite_image I (h.subset (image_preimage_subset f s))
+/-! ### Infinite sets -/
 
-theorem finite.preimage_embedding {s : set β} (f : α ↪ β) (h : s.finite) : (f ⁻¹' s).finite :=
-finite.preimage (λ _ _ _ _ h', f.injective h') h
+theorem infinite_univ_iff : (@univ α).infinite ↔ infinite α :=
+⟨λ h₁, ⟨λ h₂, h₁ $ @finite_univ α h₂⟩, λ ⟨h₁⟩ h₂, h₁ (fintype_of_finite_univ h₂)⟩
 
-lemma finite_option {s : set (option α)} : finite s ↔ finite {x : α | some x ∈ s} :=
-⟨λ h, h.preimage_embedding embedding.some,
-  λ h, ((h.image some).insert none).subset $
-    λ x, option.cases_on x (λ _, or.inl rfl) (λ x hx, or.inr $ mem_image_of_mem _ hx)⟩
+theorem infinite_univ [h : infinite α] : (@univ α).infinite :=
+infinite_univ_iff.2 h
 
-instance fintype_Union [decidable_eq α] [fintype (plift ι)]
-  (f : ι → set α) [∀ i, fintype (f i)] : fintype (⋃ i, f i) :=
-fintype.of_finset (finset.univ.bUnion (λ i : plift ι, (f i.down).to_finset)) $ by simp
+theorem infinite_coe_iff {s : set α} : infinite s ↔ s.infinite :=
+⟨λ ⟨h₁⟩ h₂, h₁ h₂.fintype, λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩⟩
 
-theorem finite_Union [fintype (plift ι)] {f : ι → set α} (H : ∀i, finite (f i)) :
-  finite (⋃ i, f i) :=
-⟨@set.fintype_Union _ _ (classical.dec_eq α) _ _ (λ i, finite.fintype (H i))⟩
+theorem infinite.to_subtype {s : set α} (h : s.infinite) : infinite s :=
+infinite_coe_iff.2 h
 
-/-- A union of sets with `fintype` structure over a set with `fintype` structure has a `fintype`
-structure. -/
-def fintype_bUnion [decidable_eq α] {ι : Type*} {s : set ι} [fintype s]
-  (f : ι → set α) (H : ∀ i ∈ s, fintype (f i)) : fintype (⋃ i ∈ s, f i) :=
-by rw bUnion_eq_Union; exact
-@set.fintype_Union _ _ _ _ _ (by rintro ⟨i, hi⟩; exact H i hi)
+/-- Embedding of `ℕ` into an infinite set. -/
+noncomputable def infinite.nat_embedding (s : set α) (h : s.infinite) : ℕ ↪ s :=
+by { haveI := h.to_subtype, exact infinite.nat_embedding s }
 
-instance fintype_bUnion' [decidable_eq α] {ι : Type*} {s : set ι} [fintype s]
-  (f : ι → set α) [H : ∀ i, fintype (f i)] : fintype (⋃ i ∈ s, f i) :=
-fintype_bUnion _ (λ i _, H i)
+lemma infinite.exists_subset_card_eq {s : set α} (hs : s.infinite) (n : ℕ) :
+  ∃ t : finset α, ↑t ⊆ s ∧ t.card = n :=
+⟨((finset.range n).map (hs.nat_embedding _)).map (embedding.subtype _), by simp⟩
 
-theorem finite.sUnion {s : set (set α)} (h : finite s) (H : ∀t∈s, finite t) : finite (⋃₀ s) :=
-by rw sUnion_eq_Union; haveI := finite.fintype h;
-   apply finite_Union; simpa using H
+lemma infinite.nonempty {s : set α} (h : s.infinite) : s.nonempty :=
+let a := infinite.nat_embedding s h 37 in ⟨a.1, a.2⟩
 
-theorem finite.bUnion {α} {ι : Type*} {s : set ι} {f : Π i ∈ s, set α} :
-  finite s → (∀ i ∈ s, finite (f i ‹_›)) → finite (⋃ i∈s, f i ‹_›)
-| ⟨hs⟩ h := by rw [bUnion_eq_Union]; exactI finite_Union (λ i, h _ _)
+lemma infinite_of_finite_compl [infinite α] {s : set α} (hs : sᶜ.finite) : s.infinite :=
+λ h, set.infinite_univ (by simpa using hs.union h)
 
-instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
-fintype.of_finset (finset.range n) $ by simp
+lemma finite.infinite_compl [infinite α] {s : set α} (hs : s.finite) : sᶜ.infinite :=
+λ h, set.infinite_univ (by simpa using hs.union h)
 
-instance fintype_le_nat (n : ℕ) : fintype {i | i ≤ n} :=
-by simpa [nat.lt_succ_iff] using set.fintype_lt_nat (n+1)
+protected theorem infinite.mono {s t : set α} (h : s ⊆ t) : s.infinite → t.infinite :=
+mt (λ ht, ht.subset h)
 
-lemma finite_le_nat (n : ℕ) : finite {i | i ≤ n} := ⟨set.fintype_le_nat _⟩
+lemma infinite.diff {s t : set α} (hs : s.infinite) (ht : t.finite) : (s \ t).infinite :=
+λ h, hs $ h.of_diff ht
 
-lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := ⟨set.fintype_lt_nat _⟩
+@[simp] lemma infinite_union {s t : set α} : (s ∪ t).infinite ↔ s.infinite ∨ t.infinite :=
+by simp only [set.infinite, finite_union, not_and_distrib]
 
-lemma infinite.exists_nat_lt {s : set ℕ} (hs : infinite s) (n : ℕ) : ∃ m ∈ s, n < m :=
-let ⟨m, hm⟩ := (hs.diff $ set.finite_le_nat n).nonempty in ⟨m, by simpa using hm⟩
+theorem infinite_of_infinite_image (f : α → β) {s : set α} (hs : (f '' s).infinite) :
+  s.infinite :=
+mt (finite.image f) hs
 
-instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintype (s ×ˢ t : set _) :=
-fintype.of_finset (s.to_finset.product t.to_finset) $ by simp
+theorem infinite_image_iff {s : set α} {f : α → β} (hi : inj_on f s) :
+  (f '' s).infinite ↔ s.infinite :=
+not_congr $ finite_image_iff hi
 
-lemma finite.prod {s : set α} {t : set β} : finite s → finite t → finite (s ×ˢ t)
-| ⟨hs⟩ ⟨ht⟩ := by exactI ⟨set.fintype_prod s t⟩
+theorem infinite_of_inj_on_maps_to {s : set α} {t : set β} {f : α → β}
+  (hi : inj_on f s) (hm : maps_to f s t) (hs : s.infinite) : t.infinite :=
+((infinite_image_iff hi).2 hs).mono (maps_to'.mp hm)
 
-lemma finite_image_fst_and_snd_iff {s : set (α × β)} :
-  finite (prod.fst '' s) ∧ finite (prod.snd '' s) ↔ finite s :=
-⟨λ h, (h.1.prod h.2).subset $ λ x h, ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩,
-  λ h, ⟨h.image _, h.image _⟩⟩
+theorem infinite.exists_ne_map_eq_of_maps_to {s : set α} {t : set β} {f : α → β}
+  (hs : s.infinite) (hf : maps_to f s t) (ht : t.finite) :
+  ∃ (x ∈ s) (y ∈ s), x ≠ y ∧ f x = f y :=
+begin
+  contrapose! ht,
+  exact infinite_of_inj_on_maps_to (λ x hx y hy, not_imp_not.1 (ht x hx y hy)) hf hs
+end
 
-/-- `image2 f s t` is finitype if `s` and `t` are. -/
-instance fintype_image2 [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β)
-  [hs : fintype s] [ht : fintype t] : fintype (image2 f s t : set γ) :=
-by { rw ← image_prod, apply set.fintype_image }
+theorem infinite_range_of_injective [infinite α] {f : α → β} (hi : injective f) :
+  (range f).infinite :=
+by { rw [←image_univ, infinite_image_iff (inj_on_of_injective hi _)], exact infinite_univ }
 
-lemma finite.image2 (f : α → β → γ) {s : set α} {t : set β} (hs : finite s) (ht : finite t) :
-  finite (image2 f s t) :=
-by { rw ← image_prod, exact (hs.prod ht).image _ }
+theorem infinite_of_injective_forall_mem [infinite α] {s : set β} {f : α → β}
+  (hi : injective f) (hf : ∀ x : α, f x ∈ s) : s.infinite :=
+by { rw ←range_subset_iff at hf, exact (infinite_range_of_injective hi).mono hf }
 
-/-- If `s : set α` is a set with `fintype` instance and `f : α → set β` is a function such that
-each `f a`, `a ∈ s`, has a `fintype` structure, then `s >>= f` has a `fintype` structure. -/
-def fintype_bind {α β} [decidable_eq β] (s : set α) [fintype s]
-  (f : α → set β) (H : ∀ a ∈ s, fintype (f a)) : fintype (s >>= f) :=
-set.fintype_bUnion _ H
+lemma infinite.exists_nat_lt {s : set ℕ} (hs : s.infinite) (n : ℕ) : ∃ m ∈ s, n < m :=
+let ⟨m, hm⟩ := (hs.diff $ set.finite_le_nat n).nonempty in ⟨m, by simpa using hm⟩
 
-instance fintype_bind' {α β} [decidable_eq β] (s : set α) [fintype s]
-  (f : α → set β) [H : ∀ a, fintype (f a)] : fintype (s >>= f) :=
-fintype_bind _ _ (λ i _, H i)
+lemma infinite.exists_not_mem_finset {s : set α} (hs : s.infinite) (f : finset α) :
+  ∃ a ∈ s, a ∉ f :=
+let ⟨a, has, haf⟩ := (hs.diff (finite_of_fintype f)).nonempty
+in ⟨a, has, λ h, haf $ finset.mem_coe.1 h⟩
 
-theorem finite.bind {α β} {s : set α} {f : α → set β} (h : finite s) (hf : ∀ a ∈ s, finite (f a)) :
-  finite (s >>= f) :=
-h.bUnion hf
 
-instance fintype_seq [decidable_eq β] (f : set (α → β)) (s : set α) [fintype f] [fintype s] :
-  fintype (f.seq s) :=
-by { rw seq_def, apply set.fintype_bUnion' }
+/-! ### Order properties -/
 
-instance fintype_seq' {α β : Type u} [decidable_eq β]
-  (f : set (α → β)) (s : set α) [fintype f] [fintype s] :
-  fintype (f <*> s) :=
-set.fintype_seq f s
+lemma finite_is_top (α : Type*) [partial_order α] : finite {x : α | is_top x} :=
+(subsingleton_is_top α).finite
 
-theorem finite.seq {f : set (α → β)} {s : set α} (hf : finite f) (hs : finite s) :
-  finite (f.seq s) :=
-by { rw seq_def, exact hf.bUnion (λ f _, hs.image _) }
+lemma finite_is_bot (α : Type*) [partial_order α] : finite {x : α | is_bot x} :=
+(subsingleton_is_bot α).finite
 
-theorem finite.seq' {α β : Type u} {f : set (α → β)} {s : set α} (hf : finite f) (hs : finite s) :
-  finite (f <*> s) :=
-hf.seq hs
+theorem infinite.exists_lt_map_eq_of_maps_to [linear_order α] {s : set α} {t : set β} {f : α → β}
+  (hs : s.infinite) (hf : maps_to f s t) (ht : t.finite) :
+  ∃ (x ∈ s) (y ∈ s), x < y ∧ f x = f y :=
+let ⟨x, hx, y, hy, hxy, hf⟩ := hs.exists_ne_map_eq_of_maps_to hf ht
+in hxy.lt_or_lt.elim (λ hxy, ⟨x, hx, y, hy, hxy, hf⟩) (λ hyx, ⟨y, hy, x, hx, hyx, hf.symm⟩)
 
-/-- There are finitely many subsets of a given finite set -/
-lemma finite.finite_subsets {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} :=
-⟨fintype.of_finset ((finset.powerset h.to_finset).map finset.coe_emb.1) $ λ s,
-  by simpa [← @exists_finite_iff_finset α (λ t, t ⊆ a ∧ t = s), subset_to_finset_iff,
-    ← and.assoc] using h.subset⟩
+lemma finite.exists_lt_map_eq_of_range_subset [linear_order α] [infinite α] {t : set β}
+  {f : α → β} (hf : range f ⊆ t) (ht : t.finite) :
+  ∃ a b, a < b ∧ f a = f b :=
+begin
+  rw [range_subset_iff, ←maps_univ_to] at hf,
+  obtain ⟨a, -, b, -, h⟩ := (@infinite_univ α _).exists_lt_map_eq_of_maps_to hf ht,
+  exact ⟨a, b, h⟩,
+end
 
 lemma exists_min_image [linear_order β] (s : set α) (f : α → β) (h1 : finite s) :
   s.nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
@@ -570,75 +801,6 @@ begin
   { exact nonempty.elim hα (λ a, ⟨a, λ x hx, absurd (set.nonempty_of_mem hx) hs⟩) }
 end
 
-end set
-
-namespace finset
-variables [decidable_eq β]
-variables {s : finset α}
-
-lemma finite_to_set (s : finset α) : set.finite (↑s : set α) :=
-set.finite_mem_finset s
-
-@[simp] lemma finite_to_set_to_finset {α : Type*} (s : finset α) :
-  (finite_to_set s).to_finset = s :=
-by { ext, rw [set.finite.mem_to_finset, mem_coe] }
-
-end finset
-
-namespace set
-
-/-- Finite product of finite sets is finite -/
-lemma finite.pi {δ : Type*} [fintype δ] {κ : δ → Type*} {t : Π d, set (κ d)}
-  (ht : ∀ d, (t d).finite) :
-  (pi univ t).finite :=
-begin
-  lift t to Π d, finset (κ d) using ht,
-  classical,
-  rw ← fintype.coe_pi_finset,
-  exact (fintype.pi_finset t).finite_to_set,
-end
-
-lemma forall_finite_image_eval_iff {δ : Type*} [fintype δ] {κ : δ → Type*} {s : set (Π d, κ d)} :
-  (∀ d, finite (eval d '' s)) ↔ finite s :=
-⟨λ h, (finite.pi h).subset $ subset_pi_eval_image _ _, λ h d, h.image _⟩
-
-/-- A finite union of finsets is finite. -/
-lemma union_finset_finite_of_range_finite (f : α → finset β) (h : (range f).finite) :
-  (⋃ a, (f a : set β)).finite :=
-begin
-  rw ← bUnion_range,
-  exact h.bUnion (λ y hy, y.finite_to_set)
-end
-
-lemma finite_subset_Union {s : set α} (hs : finite s)
-  {ι} {t : ι → set α} (h : s ⊆ ⋃ i, t i) : ∃ I : set ι, finite I ∧ s ⊆ ⋃ i ∈ I, t i :=
-begin
-  casesI hs,
-  choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i, {simpa [subset_def] using h},
-  refine ⟨range f, finite_range f, λ x hx, _⟩,
-  rw [bUnion_range, mem_Union],
-  exact ⟨⟨x, hx⟩, hf _⟩
-end
-
-lemma eq_finite_Union_of_finite_subset_Union  {ι} {s : ι → set α} {t : set α} (tfin : finite t)
-  (h : t ⊆ ⋃ i, s i) :
-  ∃ I : set ι, (finite I) ∧ ∃ σ : {i | i ∈ I} → set α,
-     (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i :=
-let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
-⟨I, Ifin, λ x, s x ∩ t,
-    λ i, tfin.subset (inter_subset_right _ _),
-    λ i, inter_subset_left _ _,
-    begin
-      ext x,
-      rw mem_Union,
-      split,
-      { intro x_in,
-        rcases mem_Union.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩,
-        use [i, hi, H, x_in] },
-      { rintros ⟨i, hi, H⟩,
-        exact H }
-    end⟩
-
 /-- An increasing union distributes over finite intersection. -/
 lemma Union_Inter_of_monotone {ι ι' α : Type*} [fintype ι] [linear_order ι']
   [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ i, monotone (s i)) :
@@ -666,88 +828,13 @@ lemma Union_univ_pi_of_monotone {ι ι' : Type*} [linear_order ι'] [nonempty ι
   (⋃ j : ι', pi univ (λ i, s i j)) = pi univ (λ i, ⋃ j, s i j) :=
 Union_pi_of_monotone (finite.of_fintype _) (λ i _, hs i)
 
-instance nat.fintype_Iio (n : ℕ) : fintype (Iio n) :=
-fintype.of_finset (finset.range n) $ by simp
-
-/--
-If `P` is some relation between terms of `γ` and sets in `γ`,
-such that every finite set `t : set γ` has some `c : γ` related to it,
-then there is a recursively defined sequence `u` in `γ`
-so `u n` is related to the image of `{0, 1, ..., n-1}` under `u`.
-
-(We use this later to show sequentially compact sets
-are totally bounded.)
--/
-lemma seq_of_forall_finite_exists  {γ : Type*}
-  {P : γ → set γ → Prop} (h : ∀ t,  finite t → ∃ c, P c t) :
-  ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n) :=
-⟨λ n, @nat.strong_rec_on' (λ _, γ) n $ λ n ih, classical.some $ h
-    (range $ λ m : Iio n, ih m.1 m.2)
-    (finite_range _),
-λ n, begin
-  classical,
-  refine nat.strong_rec_on' n (λ n ih, _),
-  rw nat.strong_rec_on_beta', convert classical.some_spec (h _ _),
-  ext x, split,
-  { rintros ⟨m, hmn, rfl⟩, exact ⟨⟨m, hmn⟩, rfl⟩ },
-  { rintros ⟨⟨m, hmn⟩, rfl⟩, exact ⟨m, hmn, rfl⟩ }
-end⟩
-
-lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))
-  (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) :=
-(hf.union hg).subset range_ite_subset
-
-lemma finite_range_const {c : β} : finite (range (λ x : α, c)) :=
-(finite_singleton c).subset range_const_subset
-
 lemma range_find_greatest_subset {P : α → ℕ → Prop} [∀ x, decidable_pred (P x)] {b : ℕ}:
   range (λ x, nat.find_greatest (P x) b) ⊆ ↑(finset.range (b + 1)) :=
 by { rw range_subset_iff, intro x, simp [nat.lt_succ_iff, nat.find_greatest_le] }
 
 lemma finite_range_find_greatest {P : α → ℕ → Prop} [∀ x, decidable_pred (P x)] {b : ℕ} :
   finite (range (λ x, nat.find_greatest (P x) b)) :=
-(finset.range (b + 1)).finite_to_set.subset range_find_greatest_subset
-
-lemma card_lt_card {s t : set α} [fintype s] [fintype t] (h : s ⊂ t) :
-  fintype.card s < fintype.card t :=
-fintype.card_lt_of_injective_not_surjective (set.inclusion h.1) (set.inclusion_injective h.1) $
-  λ hst, (ssubset_iff_subset_ne.1 h).2 (eq_of_inclusion_surjective hst)
-
-lemma card_le_of_subset {s t : set α} [fintype s] [fintype t] (hsub : s ⊆ t) :
-  fintype.card s ≤ fintype.card t :=
-fintype.card_le_of_injective (set.inclusion hsub) (set.inclusion_injective hsub)
-
-lemma eq_of_subset_of_card_le {s t : set α} [fintype s] [fintype t]
-   (hsub : s ⊆ t) (hcard : fintype.card t ≤ fintype.card s) : s = t :=
-(eq_or_ssubset_of_subset hsub).elim id
-  (λ h, absurd hcard $ not_le_of_lt $ card_lt_card h)
-
-lemma subset_iff_to_finset_subset (s t : set α) [fintype s] [fintype t] :
-  s ⊆ t ↔ s.to_finset ⊆ t.to_finset :=
-by simp
-
-@[simp, mono] lemma finite.to_finset_mono {s t : set α} {hs : finite s} {ht : finite t} :
-  hs.to_finset ⊆ ht.to_finset ↔ s ⊆ t :=
-begin
-  split,
-  { intros h x,
-    rw [←finite.mem_to_finset hs, ←finite.mem_to_finset ht],
-    exact λ hx, h hx },
-  { intros h x,
-    rw [finite.mem_to_finset hs, finite.mem_to_finset ht],
-    exact λ hx, h hx }
-end
-
-@[simp, mono] lemma finite.to_finset_strict_mono {s t : set α} {hs : finite s} {ht : finite t} :
-  hs.to_finset ⊂ ht.to_finset ↔ s ⊂ t :=
-begin
-  rw [←lt_eq_ssubset, ←finset.lt_iff_ssubset, lt_iff_le_and_ne, lt_iff_le_and_ne],
-  simp
-end
-
-lemma card_range_of_injective [fintype α] {f : α → β} (hf : injective f)
-  [fintype (range f)] : fintype.card (range f) = fintype.card α :=
-eq.symm $ fintype.card_congr $ equiv.of_injective f hf
+(finite_of_fintype ↑(finset.range (b + 1))).subset range_find_greatest_subset
 
 lemma finite.exists_maximal_wrt [partial_order β] (f : α → β) (s : set α) (h : set.finite s) :
   s.nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a' :=
@@ -770,52 +857,6 @@ begin
     { exact ih c hcs hbc } }
 end
 
-lemma finite.card_to_finset {s : set α} [fintype s] (h : s.finite) :
-  h.to_finset.card = fintype.card s :=
-begin
-  rw [← finset.card_attach, finset.attach_eq_univ, ← fintype.card],
-  refine fintype.card_congr (equiv.set_congr _),
-  ext x, show x ∈ h.to_finset ↔ x ∈ s,
-  simp,
-end
-
-lemma infinite.exists_not_mem_finset {s : set α} (hs : s.infinite) (f : finset α) :
-  ∃ a ∈ s, a ∉ f :=
-let ⟨a, has, haf⟩ := (hs.diff f.finite_to_set).nonempty in ⟨a, has, λ h, haf $ finset.mem_coe.1 h⟩
-
-section decidable_eq
-
-lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
-  [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
-by ext; simp
-
-lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]
-  [fintype s] [fintype t] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
-by ext; simp
-
-instance fintype_sdiff  {α : Type*} [decidable_eq α]
-  (s t : set α) [fintype s] [fintype t] :
-  fintype (s \ t : set α) :=
-fintype.of_finset (s.to_finset \ t.to_finset) $ by simp
-
-lemma to_finset_sdiff {α : Type*} [decidable_eq α] (s t : set α) [fintype s] [fintype t]
-  [fintype (s \ t : set α)] : (s \ t).to_finset = s.to_finset \ t.to_finset :=
-by ext; simp
-
-lemma to_finset_ne_eq_erase {α : Type*} [decidable_eq α] [fintype α] (a : α)
-  [fintype {x : α | x ≠ a}] : {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
-by ext; simp
-
-lemma card_ne_eq [fintype α] (a : α) [fintype {x : α | x ≠ a}] :
-  fintype.card {x : α | x ≠ a} = fintype.card α - 1 :=
-begin
-  haveI := classical.dec_eq α,
-  rw [←to_finset_card, to_finset_ne_eq_erase, finset.card_erase_of_mem (finset.mem_univ _),
-      finset.card_univ],
-end
-
-end decidable_eq
-
 section
 
 variables [semilattice_sup α] [nonempty α] {s : set α}
@@ -868,34 +909,15 @@ namespace finset
 /-- A finset is bounded above. -/
 protected lemma bdd_above [semilattice_sup α] [nonempty α] (s : finset α) :
   bdd_above (↑s : set α) :=
-s.finite_to_set.bdd_above
+(set.finite_of_fintype ↑s).bdd_above
 
 /-- A finset is bounded below. -/
 protected lemma bdd_below [semilattice_inf α] [nonempty α] (s : finset α) :
   bdd_below (↑s : set α) :=
-s.finite_to_set.bdd_below
+(set.finite_of_fintype ↑s).bdd_below
 
 end finset
 
-namespace fintype
-variables [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q]
-
-@[simp]
-lemma card_subtype_compl : fintype.card {x // ¬ p x} = fintype.card α - fintype.card {x // p x} :=
-begin
-  classical,
-  rw [fintype.card_of_subtype (set.to_finset pᶜ), set.to_finset_compl p, finset.card_compl,
-      fintype.card_of_subtype (set.to_finset p)];
-    intros; simp; refl
-end
-
-/-- If two subtypes of a fintype have equal cardinality, so do their complements. -/
-lemma card_compl_eq_card_compl (h : fintype.card {x // p x} = fintype.card {x // q x}) :
-  fintype.card {x // ¬ p x} = fintype.card {x // ¬ q x} :=
-by simp only [card_subtype_compl, h]
-
-end fintype
-
 /--
 If a set `s` does not contain any elements between any pair of elements `x, z ∈ s` with `x ≤ z`
 (i.e if given `x, y, z ∈ s` such that `x ≤ y ≤ z`, then `y` is either `x` or `z`), then `s` is
@@ -920,3 +942,17 @@ begin
   { dsimp only [x, y] at this, exact key₁ (f.injective $ subtype.coe_injective this) },
   { dsimp only [y, z] at this, exact key₂ (f.injective $ subtype.coe_injective this) }
 end
+
+/-! ### Finset -/
+
+namespace finset
+
+/-- Gives a `set.finite` for the `finset` coerced to a `set`.
+This is a wrapper around `set.finite_of_fintype`. -/
+lemma finite_to_set (s : finset α) : (s : set α).finite := set.finite_of_fintype _
+
+@[simp] lemma finite_to_set_to_finset {α : Type*} (s : finset α) :
+  s.finite_to_set.to_finset = s :=
+by { ext, rw [set.finite.mem_to_finset, mem_coe] }
+
+end finset
diff --git a/src/data/set/intervals/infinite.lean b/src/data/set/intervals/infinite.lean
index cdca43d3557a7..1298ad7be5587 100644
--- a/src/data/set/intervals/infinite.lean
+++ b/src/data/set/intervals/infinite.lean
@@ -20,7 +20,7 @@ section bounded
 
 variables [densely_ordered α]
 
-lemma Ioo.infinite {a b : α} (h : a < b) : infinite (Ioo a b) :=
+lemma Ioo.infinite {a b : α} (h : a < b) : (Ioo a b).infinite :=
 begin
   rintro (f : finite (Ioo a b)),
   obtain ⟨m, hm₁, hm₂⟩ : ∃ m ∈ Ioo a b, ∀ x ∈ Ioo a b, ¬x < m,
@@ -29,13 +29,13 @@ begin
   exact hm₂ z ⟨hz₁, lt_trans hz₂ hm₁.2⟩ hz₂,
 end
 
-lemma Ico.infinite {a b : α} (h : a < b) : infinite (Ico a b) :=
+lemma Ico.infinite {a b : α} (h : a < b) : (Ico a b).infinite :=
 (Ioo.infinite h).mono Ioo_subset_Ico_self
 
-lemma Ioc.infinite {a b : α} (h : a < b) : infinite (Ioc a b) :=
+lemma Ioc.infinite {a b : α} (h : a < b) : (Ioc a b).infinite :=
 (Ioo.infinite h).mono Ioo_subset_Ioc_self
 
-lemma Icc.infinite {a b : α} (h : a < b) : infinite (Icc a b) :=
+lemma Icc.infinite {a b : α} (h : a < b) : (Icc a b).infinite :=
 (Ioo.infinite h).mono Ioo_subset_Icc_self
 
 end bounded
@@ -44,7 +44,7 @@ section unbounded_below
 
 variables [no_min_order α]
 
-lemma Iio.infinite {b : α} : infinite (Iio b) :=
+lemma Iio.infinite {b : α} : (Iio b).infinite :=
 begin
   rintro (f : finite (Iio b)),
   obtain ⟨m, hm₁, hm₂⟩ : ∃ m < b, ∀ x < b, ¬x < m,
@@ -53,7 +53,7 @@ begin
   exact hm₂ z (lt_trans hz hm₁) hz
 end
 
-lemma Iic.infinite {b : α} : infinite (Iic b) :=
+lemma Iic.infinite {b : α} : (Iic b).infinite :=
 Iio.infinite.mono Iio_subset_Iic_self
 
 end unbounded_below
@@ -62,9 +62,9 @@ section unbounded_above
 
 variables [no_max_order α]
 
-lemma Ioi.infinite {a : α} : infinite (Ioi a) := @Iio.infinite αᵒᵈ _ _ _
+lemma Ioi.infinite {a : α} : (Ioi a).infinite := @Iio.infinite αᵒᵈ _ _ _
 
-lemma Ici.infinite {a : α} : infinite (Ici a) :=
+lemma Ici.infinite {a : α} : (Ici a).infinite :=
 Ioi.infinite.mono Ioi_subset_Ici_self
 
 end unbounded_above
diff --git a/src/logic/equiv/fintype.lean b/src/logic/equiv/fintype.lean
index 253760caf4612..a04aa3628a1a4 100644
--- a/src/logic/equiv/fintype.lean
+++ b/src/logic/equiv/fintype.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 
-import data.set.finite
+import data.fintype.basic
 import group_theory.perm.sign
 import logic.equiv.basic
 
@@ -87,7 +87,7 @@ is an equivalence between the complement of those subtypes.
 See also `equiv.compl`, for a computable version when a term of type
 `{e' : α ≃ α // ∀ x : {x // p x}, e' x = e x}` is known. -/
 noncomputable def to_compl (e : {x // p x} ≃ {x // q x}) : {x // ¬ p x} ≃ {x // ¬ q x} :=
-classical.choice (fintype.card_eq.mp (fintype.card_compl_eq_card_compl (fintype.card_congr e)))
+classical.choice (fintype.card_eq.mp (fintype.card_compl_eq_card_compl _ _ (fintype.card_congr e)))
 
 /-- If `e` is an equivalence between two subtypes of a fintype `α`, `e.extend_subtype`
 is a permutation of `α` acting like `e` on the subtypes and doing something arbitrary outside.
diff --git a/src/order/well_founded_set.lean b/src/order/well_founded_set.lean
index 93e24066cdf74..f6471660f60b9 100644
--- a/src/order/well_founded_set.lean
+++ b/src/order/well_founded_set.lean
@@ -146,15 +146,15 @@ begin
   classical,
   rw [is_wf_iff_no_descending_seq] at *,
   rintros f fst,
-  have h : infinite (f ⁻¹' s) ∨ infinite (f ⁻¹' t),
-  { have h : infinite (univ : set ℕ) := infinite_univ,
+  have h : (f ⁻¹' s).infinite ∨ (f ⁻¹' t).infinite,
+  { have h : (univ : set ℕ).infinite := infinite_univ,
     have hpre : f ⁻¹' (s ∪ t) = set.univ,
     { rw [← image_univ, image_subset_iff, univ_subset_iff] at fst,
       exact fst },
     rw preimage_union at hpre,
     rw ← hpre at h,
-    rw [infinite, infinite],
-    rw infinite at h,
+    rw [set.infinite, set.infinite],
+    rw set.infinite at h,
     contrapose! h,
     exact finite.union h.1 h.2, },
   rw [← infinite_coe_iff, ← infinite_coe_iff] at h,
@@ -355,15 +355,15 @@ begin
   classical,
   rw [is_pwo_iff_exists_monotone_subseq] at *,
   rintros f fst,
-  have h : infinite (f ⁻¹' s) ∨ infinite (f ⁻¹' t),
-  { have h : infinite (univ : set ℕ) := infinite_univ,
+  have h : (f ⁻¹' s).infinite ∨ (f ⁻¹' t).infinite,
+  { have h : (univ : set ℕ).infinite := infinite_univ,
     have hpre : f ⁻¹' (s ∪ t) = set.univ,
     { rw [← image_univ, image_subset_iff, univ_subset_iff] at fst,
       exact fst },
     rw preimage_union at hpre,
     rw ← hpre at h,
-    rw [infinite, infinite],
-    rw infinite at h,
+    rw [set.infinite, set.infinite],
+    rw set.infinite at h,
     contrapose! h,
     exact finite.union h.1 h.2, },
   rw [← infinite_coe_iff, ← infinite_coe_iff] at h,
diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean
index 12ff6706e3b27..4cc6b3146a5ac 100644
--- a/src/ring_theory/hahn_series.lean
+++ b/src/ring_theory/hahn_series.lean
@@ -1394,7 +1394,7 @@ instance : has_scalar (hahn_series Γ R) (summable_family Γ R α) :=
       exact λ a ha, (set.add_subset_add (set.subset.refl _) (set.subset_Union _ a)) ha,
     end,
     finite_co_support' := λ g, begin
-      refine ((add_antidiagonal x.is_pwo_support s.is_pwo_Union_support g).finite_to_set.bUnion
+      refine ((add_antidiagonal x.is_pwo_support s.is_pwo_Union_support g).finite_to_set.bUnion'
         (λ ij hij, _)).subset (λ a ha, _),
       { exact λ ij hij, function.support (λ a, (s a).coeff ij.2) },
       { apply s.finite_co_support },
diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean
index 65dce2d63b87b..d47f80668a88b 100644
--- a/src/topology/metric_space/closeds.lean
+++ b/src/topology/metric_space/closeds.lean
@@ -211,12 +211,13 @@ instance closeds.compact_space [compact_space α] : compact_space (closeds α) :
   let F := {f : closeds α | (f : set α) ⊆ s},
   refine ⟨F, _, λ u _, _⟩,
   -- `F` is finite
-  { apply @finite_of_finite_image _ _ F coe,
-    { exact set_like.coe_injective.inj_on F },
-    { refine fs.finite_subsets.subset (λb, _),
+  { apply @finite.of_finite_image _ _ F coe,
+    { apply fs.finite_subsets.subset (λb, _),
       simp only [and_imp, set.mem_image, set.mem_set_of_eq, exists_imp_distrib],
       assume x hx hx',
-      rwa hx' at hx }},
+      rwa hx' at hx },
+    { exact set_like.coe_injective.inj_on F } },
+
   -- `F` is ε-dense
   { obtain ⟨t0, t0s, Dut0⟩ := main u,
     have : is_closed t0 := (fs.subset t0s).is_compact.is_closed,
diff --git a/src/topology/metric_space/emetric_paracompact.lean b/src/topology/metric_space/emetric_paracompact.lean
index 801c60c72932c..e98eeb0e4256e 100644
--- a/src/topology/metric_space/emetric_paracompact.lean
+++ b/src/topology/metric_space/emetric_paracompact.lean
@@ -148,8 +148,8 @@ begin
         ennreal.mul_le_mul le_rfl $ add_le_add le_rfl $ hpow_le (add_le_add hm le_rfl)
       ... = 3 * 2⁻¹ ^ m : by rw [mul_add, h2pow, bit1, add_mul, one_mul] },
     -- Finally, we glue `Hgt` and `Hle`
-    have : (⋃ (m ≤ n + k) (i ∈ {i : ι | (D m i ∩ B).nonempty}), {(m, i)}).finite,
-      from (finite_le_nat _).bUnion (λ i hi, (Hle i hi).finite.bUnion (λ _ _, finite_singleton _)),
+    have : (⋃ (m ≤ n + k) (i ∈ {i : ι | (D m i ∩ B).nonempty}), {(m, i)}).finite :=
+      (finite_le_nat _).bUnion' (λ i hi, (Hle i hi).finite.bUnion' (λ _ _, finite_singleton _)),
     refine this.subset (λ I hI, _), simp only [mem_Union],
     refine ⟨I.1, _, I.2, hI, prod.mk.eta.symm⟩,
     exact not_lt.1 (λ hlt, Hgt I.1 hlt I.2 hI.some_spec) }
diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean
index 4a642f95dfc9e..76f053ddc7700 100644
--- a/src/topology/subset_properties.lean
+++ b/src/topology/subset_properties.lean
@@ -722,7 +722,7 @@ noncompact_space_of_ne_bot $ by simp only [filter.cocompact_eq_cofinite, filter.
 noncomputable
 def fintype_of_compact_of_discrete [compact_space α] [discrete_topology α] :
   fintype α :=
-fintype_of_univ_finite $ compact_univ.finite_of_discrete
+fintype_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 :=
@@ -754,7 +754,7 @@ finitely many elements, `fintype` version. -/
 noncomputable def locally_finite.fintype_of_compact {ι : Type*} [compact_space α] {f : ι → set α}
   (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) :
   fintype ι :=
-fintype_of_univ_finite (hf.finite_of_compact hne)
+fintype_of_finite_univ (hf.finite_of_compact hne)
 
 /-- The comap of the cocompact filter on `β` by a continuous function `f : α → β` is less than or
 equal to the cocompact filter on `α`.