diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean
index 103fb681d190e..a35c35ab9e857 100644
--- a/src/algebra/pointwise.lean
+++ b/src/algebra/pointwise.lean
@@ -72,7 +72,7 @@ set.ext $ λ a,
 @[to_additive]
 lemma pointwise_mul_finite [has_mul α] {s t : set α} (hs : finite s) (ht : finite t) :
   finite (s * t) :=
-by { rw pointwise_mul_eq_image, apply set.finite_image, exact set.finite_prod hs ht }
+by { rw pointwise_mul_eq_image, exact (hs.prod ht).image _ }
 
 @[to_additive pointwise_add_add_semigroup]
 def pointwise_mul_semigroup [semigroup α] : semigroup (set α) :=
diff --git a/src/analysis/analytic/composition.lean b/src/analysis/analytic/composition.lean
index fe1dfb414b896..07798ef40156d 100644
--- a/src/analysis/analytic/composition.lean
+++ b/src/analysis/analytic/composition.lean
@@ -556,7 +556,7 @@ end
 power series, here given a a finset.
 See also `comp_partial_sum`. -/
 def comp_partial_sum_target (N : ℕ) : finset (Σ n, composition n) :=
-set.finite.to_finset $ set.finite_dependent_image (finset.finite_to_set _)
+set.finite.to_finset $ (finset.finite_to_set _).dependent_image
   (comp_partial_sum_target_subset_image_comp_partial_sum_source N)
 
 @[simp] lemma mem_comp_partial_sum_target_iff {N : ℕ} {a : Σ n, composition n} :
diff --git a/src/data/analysis/filter.lean b/src/data/analysis/filter.lean
index 9cd07cad8bb50..8e75825cd4236 100644
--- a/src/data/analysis/filter.lean
+++ b/src/data/analysis/filter.lean
@@ -174,7 +174,7 @@ protected def cofinite [decidable_eq α] : (@cofinite α).realizer := ⟨finset
   inf_le_left  := λ s t a, mt (finset.mem_union_left _),
   inf_le_right := λ s t a, mt (finset.mem_union_right _) },
 filter_eq $ set.ext $ λ x,
-⟨λ ⟨s, h⟩, finite_subset (finite_mem_finset s) (compl_subset_comm.1 h),
+⟨λ ⟨s, h⟩, s.finite_to_set.subset (compl_subset_comm.1 h),
  λ ⟨fs⟩, by exactI ⟨(-x).to_finset, λ a (h : a ∉ (-x).to_finset),
   classical.by_contradiction $ λ h', h (mem_to_finset.2 h')⟩⟩⟩
 
diff --git a/src/data/analysis/topology.lean b/src/data/analysis/topology.lean
index f00b71fec6836..e481b28aef5e5 100644
--- a/src/data/analysis/topology.lean
+++ b/src/data/analysis/topology.lean
@@ -180,7 +180,7 @@ theorem locally_finite_iff_exists_realizer [topological_space α]
        show ∃ (b : F.σ), x ∈ (F.F) b ∧ (F.F) b ⊆ g x, from
        let ⟨h, h'⟩ := h₁ x in F.mem_nhds.1 h) in
   ⟨⟨λ x, ⟨g₂ x, (h₂ x).1⟩, λ x, finite.fintype $
-    let ⟨h, h'⟩ := h₁ x in finite_subset h' $ λ i hi,
+    let ⟨h, h'⟩ := h₁ x in h'.subset $ λ i hi,
     hi.mono (inter_subset_inter_right _ (h₂ x).2)⟩⟩,
  λ ⟨R⟩, R.to_locally_finite⟩
 
diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index 5dc30d75caa7a..69aca8d95833e 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -253,8 +253,7 @@ omit dec
 lemma finite_supp (f : Π₀ i, β i) : set.finite {i | f i ≠ 0} :=
 begin
   classical,
-  exact quotient.induction_on f (λ x, set.finite_subset
-  (finset.finite_to_set x.2.to_finset) (λ i H,
+  exact quotient.induction_on f (λ x, x.2.to_finset.finite_to_set.subset (λ i H,
     multiset.mem_to_finset.2 ((x.3 i).resolve_right H)))
 end
 include dec
diff --git a/src/data/finsupp.lean b/src/data/finsupp.lean
index acf528c6aaf70..8389f2159fd66 100644
--- a/src/data/finsupp.lean
+++ b/src/data/finsupp.lean
@@ -1812,6 +1812,6 @@ end
 The set of `m : σ →₀ ℕ` that are coordinatewise less than or equal to `n`,
 but not equal to `n` everywhere, is a finite set. -/
 lemma finite_lt_nat (n : σ →₀ ℕ) : set.finite {m | m < n} :=
-set.finite_subset (finite_le_nat n) $ λ m, le_of_lt
+(finite_le_nat n).subset $ λ m, le_of_lt
 
 end finsupp
diff --git a/src/data/real/hyperreal.lean b/src/data/real/hyperreal.lean
index f1c9a7336d143..30b5397820d2f 100644
--- a/src/data/real/hyperreal.lean
+++ b/src/data/real/hyperreal.lean
@@ -94,7 +94,7 @@ begin
     λ i hi1, le_of_lt (by simp only [lt_iff_not_ge];
     exact λ hi2, hi1 (lt_of_le_of_lt (le_abs_self _) (hf' i hi2)) : i < N),
   exact mem_hyperfilter_of_finite_compl
-    (set.finite_subset (set.finite_le_nat N) hs)
+    ((set.finite_le_nat N).subset hs)
 end
 
 lemma neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
@@ -437,7 +437,7 @@ Exists.cases_on (hf' (r + 1)) $ λ i hi,
     by simp only [set.compl_set_of, not_lt];
     exact λ a har, le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _))),
   (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
-  set.finite_subset (set.finite_le_nat _) hS
+  (set.finite_le_nat _).subset hS
 
 theorem infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : tendsto f at_top at_bot) :
   infinite_neg (of_seq f) :=
@@ -449,7 +449,7 @@ Exists.cases_on (hf' (r - 1)) $ λ i hi,
     by simp only [set.compl_set_of, not_lt];
     exact λ a har, le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har)),
   (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
-  set.finite_subset (set.finite_le_nat _) hS
+  (set.finite_le_nat _).subset hS
 
 lemma not_infinite_neg {x : ℝ*} : ¬ infinite x → ¬ infinite (-x) :=
 not_imp_not.mpr infinite_iff_infinite_neg.mpr
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index 622cf5c29d3d6..e98ed6c70fcb0 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -121,11 +121,11 @@ else fintype_insert' _ h
 
 end
 
-@[simp] theorem finite_insert (a : α) {s : set α} : finite s → finite (insert a s)
+@[simp] theorem finite.insert (a : α) {s : set α} : finite s → finite (insert a s)
 | ⟨h⟩ := ⟨@set.fintype_insert _ (classical.dec_eq α) _ _ h⟩
 
 lemma to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : finite s) :
-  (finite_insert a hs).to_finset = insert a hs.to_finset :=
+  (hs.insert a).to_finset = insert a hs.to_finset :=
 finset.ext $ by simp
 
 @[elab_as_eliminator]
@@ -149,7 +149,7 @@ end
 @[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) (finite_insert a h)) :
+  (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 (assume h, H0) (assume a s has hs ih h, H1 has hs (ih _)),
@@ -186,7 +186,7 @@ infinite_univ_iff.2 h
 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_union {s t : set α} : finite s → finite t → finite (s ∪ t)
+theorem finite.union {s t : set α} : finite s → finite t → finite (s ∪ t)
 | ⟨hs⟩ ⟨ht⟩ := ⟨@set.fintype_union _ (classical.dec_eq α) _ _ hs ht⟩
 
 instance fintype_sep (s : set α) (p : α → Prop) [fintype s] [decidable_pred p] : fintype ({a ∈ s | p a} : set α) :=
@@ -195,10 +195,11 @@ fintype.of_finset (s.to_finset.filter p) $ by simp
 instance fintype_inter (s t : set α) [fintype s] [decidable_pred t] : fintype (s ∩ t : set α) :=
 set.fintype_sep s 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_subset {s : set α} : finite s → ∀ {t : set α}, t ⊆ s → finite 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⟩
 
 instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
@@ -210,10 +211,10 @@ fintype.of_finset (finset.univ.image f) $ by simp [range]
 theorem finite_range (f : α → β) [fintype α] : finite (range f) :=
 by haveI := classical.dec_eq β; exact ⟨by apply_instance⟩
 
-theorem finite_image {s : set α} (f : α → β) : finite s → finite (f '' s)
+theorem finite.image {s : set α} (f : α → β) : finite s → finite (f '' s)
 | ⟨h⟩ := ⟨@set.fintype_image _ _ (classical.dec_eq β) _ _ h⟩
 
-lemma finite_dependent_image {s : set α} (hs : finite s) {F : Π i ∈ s, β} {t : set β}
+lemma finite.dependent_image {s : set α} (hs : finite s) {F : Π i ∈ s, β} {t : set β}
   (H : ∀ y ∈ t, ∃ x (hx : x ∈ s), y = F x hx) : set.finite t :=
 begin
   let G : s → β := λ x, F x.1 x.2,
@@ -222,15 +223,17 @@ begin
     rcases H y hy with ⟨x, hx, xy⟩,
     refine ⟨⟨x, hx⟩, xy.symm⟩ },
   letI : fintype s := finite.fintype hs,
-  exact finite_subset (finite_range G) A
+  exact (finite_range G).subset A
 end
 
 instance fintype_map {α β} [decidable_eq β] :
   ∀ (s : set α) (f : α → β) [fintype s], fintype (f <$> s) := set.fintype_image
 
-theorem finite_map {α β} {s : set α} :
-  ∀ (f : α → β), finite s → finite (f <$> s) := finite_image
+theorem finite.map {α β} {s : set α} :
+  ∀ (f : α → β), finite s → finite (f <$> s) := finite.image
 
+/-- 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 ⟨_, @multiset.nodup_filter_map β α g _
@@ -243,22 +246,18 @@ begin
   simp [I _, (injective_of_partial_inv I).eq_iff]
 end
 
-theorem finite_of_finite_image_on {s : set α} {f : α → β} (hi : set.inj_on f s) :
+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⟩) $
   assume a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext.1 eq⟩
 
-theorem finite_image_iff_on {s : set α} {f : α → β} (hi : inj_on f s) :
+theorem finite_image_iff {s : set α} {f : α → β} (hi : inj_on f s) :
   finite (f '' s) ↔ finite s :=
-⟨finite_of_finite_image_on hi, finite_image _⟩
+⟨finite_of_finite_image hi, finite.image _⟩
 
-theorem finite_of_finite_image {s : set α} {f : α → β} (I : set.inj_on f s) :
-  finite (f '' s) → finite s :=
-finite_of_finite_image_on I
-
-theorem finite_preimage {s : set β} {f : α → β}
+theorem finite.preimage {s : set β} {f : α → β}
   (I : set.inj_on f (f⁻¹' s)) (h : finite s) : finite (f ⁻¹' s) :=
-finite_of_finite_image I (finite_subset h (image_preimage_subset f s))
+finite_of_finite_image I (h.subset (image_preimage_subset f s))
 
 instance fintype_Union [decidable_eq α] {ι : Type*} [fintype ι]
   (f : ι → set α) [∀ i, fintype (f i)] : fintype (⋃ i, f i) :=
@@ -267,6 +266,8 @@ fintype.of_finset (finset.univ.bind (λ i, (f i).to_finset)) $ by simp
 theorem finite_Union {ι : Type*} [fintype ι] {f : ι → set α} (H : ∀i, finite (f i)) : finite (⋃ i, f i) :=
 ⟨@set.fintype_Union _ (classical.dec_eq α) _ _ _ (λ i, finite.fintype (H i))⟩
 
+/-- 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
@@ -276,17 +277,13 @@ 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)
 
-theorem finite_sUnion {s : set (set α)} (h : finite s) (H : ∀t∈s, finite t) : finite (⋃₀ s) :=
+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
 
-theorem finite_bUnion {α} {ι : Type*} {s : set ι} {f : ι → set α} :
-  finite s → (∀i, finite (f i)) → finite (⋃ i∈s, f i)
-| ⟨hs⟩ h := by rw [bUnion_eq_Union]; exactI finite_Union (λ i, h _)
-
-theorem finite_bUnion' {α} {ι : Type*} {s : set ι} (f : ι → 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 i.1 i.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 _ _)
 
 instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
 fintype.of_finset (finset.range n) $ by simp
@@ -301,9 +298,11 @@ lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := ⟨set.fintype_lt_nat _⟩
 instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintype (set.prod s t) :=
 fintype.of_finset (s.to_finset.product t.to_finset) $ by simp
 
-lemma finite_prod {s : set α} {t : set β} : finite s → finite t → finite (set.prod s t)
+lemma finite.prod {s : set α} {t : set β} : finite s → finite t → finite (set.prod s t)
 | ⟨hs⟩ ⟨ht⟩ := by exactI ⟨set.fintype_prod s t⟩
 
+/-- 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
@@ -321,19 +320,19 @@ instance fintype_seq {α β : Type u} [decidable_eq β]
   fintype (f <*> s) :=
 by rw seq_eq_bind_map; apply set.fintype_bind'
 
-theorem finite_seq {α β : Type u} {f : set (α → β)} {s : set α} :
+theorem finite.seq {α β : Type u} {f : set (α → β)} {s : set α} :
   finite f → finite s → finite (f <*> s)
 | ⟨hf⟩ ⟨hs⟩ := by { haveI := classical.dec_eq β, exactI ⟨set.fintype_seq _ _⟩ }
 
 /-- There are finitely many subsets of a given finite set -/
-lemma finite_subsets_of_finite {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} :=
+lemma finite.finite_subsets {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} :=
 begin
   -- we just need to translate the result, already known for finsets,
   -- to the language of finite sets
   let s : set (set α) := coe '' (↑(finset.powerset (finite.to_finset h)) : set (finset α)),
-  have : finite s := finite_image _ (finite_mem_finset _),
-  apply finite_subset this,
-  refine λ b hb, ⟨(finite_subset h hb).to_finset, _, finite.coe_to_finset _⟩,
+  have : finite s := (finite_mem_finset _).image _,
+  apply this.subset,
+  refine λ b hb, ⟨(h.subset hb).to_finset, _, finite.coe_to_finset _⟩,
   simpa [finset.subset_iff]
 end
 
@@ -383,7 +382,7 @@ lemma eq_finite_Union_of_finite_subset_Union  {ι} {s : ι → set α} {t : 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, finite_subset tfin (inter_subset_right _ _),
+    λ i, tfin.subset (inter_subset_right _ _),
     λ i, inter_subset_left _ _,
     begin
       ext x,
@@ -425,10 +424,10 @@ 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)) :=
-finite_subset (finite_union hf hg) range_ite_subset
+(hf.union hg).subset range_ite_subset
 
 lemma finite_range_const {c : β} : finite (range (λ x : α, c)) :=
-finite_subset (finite_singleton c) range_const_subset
+(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)) :=
@@ -436,7 +435,7 @@ by { rw range_subset_iff, assume 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)) :=
-finite_subset (finset.finite_to_set $ finset.range (b + 1)) range_find_greatest_subset
+(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 :=
@@ -503,11 +502,11 @@ section
 variables [semilattice_sup α] [nonempty α] {s : set α}
 
 /--A finite set is bounded above.-/
-lemma bdd_above_finite (hs : finite s) : bdd_above s :=
+protected lemma finite.bdd_above (hs : finite s) : bdd_above s :=
 finite.induction_on hs bdd_above_empty $ λ a s _ _ h, h.insert a
 
 /--A finite union of sets which are all bounded above is still bounded above.-/
-lemma bdd_above_finite_union {I : set β} {S : β → set α} (H : finite I) :
+lemma finite.bdd_above_bUnion {I : set β} {S : β → set α} (H : finite I) :
   (bdd_above (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_above (S i)) :=
 finite.induction_on H
   (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
@@ -520,13 +519,13 @@ section
 variables [semilattice_inf α] [nonempty α] {s : set α}
 
 /--A finite set is bounded below.-/
-lemma bdd_below_finite (hs : finite s) : bdd_below s :=
-finite.induction_on hs bdd_below_empty $ λ a s _ _ h, h.insert a
+protected lemma finite.bdd_below (hs : finite s) : bdd_below s :=
+@finite.bdd_above (order_dual α) _ _ _ hs
 
 /--A finite union of sets which are all bounded below is still bounded below.-/
-lemma bdd_below_finite_union {I : set β} {S : β → set α} (H : finite I) :
+lemma finite.bdd_below_bUnion {I : set β} {S : β → set α} (H : finite I) :
   (bdd_below (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_below (S i)) :=
-@bdd_above_finite_union (order_dual α) _ _ _ _ _ H
+@finite.bdd_above_bUnion (order_dual α) _ _ _ _ _ H
 
 end
 
@@ -539,7 +538,7 @@ section preimage
 /-- Preimage of `s : finset β` under a map `f` injective of `f ⁻¹' s` as a `finset`.  -/
 noncomputable def preimage {f : α → β} (s : finset β)
   (hf : set.inj_on f (f ⁻¹' ↑s)) : finset α :=
-(set.finite_preimage hf (set.finite_mem_finset s)).to_finset
+(s.finite_to_set.preimage hf).to_finset
 
 @[simp] lemma mem_preimage {f : α → β} {s : finset β} {hf : set.inj_on f (f ⁻¹' ↑s)} {x : α} :
   x ∈ preimage s hf ↔ f x ∈ s :=
@@ -577,12 +576,14 @@ calc
   ... = ∏ x in s, g x : by rw [image_preimage]
 
 /-- A finset is bounded above. -/
-lemma bdd_above [semilattice_sup α] [nonempty α] (s : finset α) : bdd_above (↑s : set α) :=
-set.bdd_above_finite (finset.finite_to_set s)
+protected lemma bdd_above [semilattice_sup α] [nonempty α] (s : finset α) :
+  bdd_above (↑s : set α) :=
+s.finite_to_set.bdd_above
 
 /-- A finset is bounded below. -/
-lemma bdd_below [semilattice_inf α] [nonempty α] (s : finset α) : bdd_below (↑s : set α) :=
-set.bdd_below_finite (finset.finite_to_set s)
+protected lemma bdd_below [semilattice_inf α] [nonempty α] (s : finset α) :
+  bdd_below (↑s : set α) :=
+s.finite_to_set.bdd_below
 
 end finset
 
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
index f37bf9f419028..dd47eef4cd181 100644
--- a/src/linear_algebra/basis.lean
+++ b/src/linear_algebra/basis.lean
@@ -407,7 +407,7 @@ begin
       refine span_mono (@supr_le_supr2 (set M) _ _ _ _ _ _),
       rintros ⟨i⟩, exact ⟨i, le_refl _⟩ },
     { change finite (plift.up ⁻¹' ↑s),
-      exact finite_preimage (assume i j _ _, plift.up.inj) s.finite_to_set } }
+      exact s.finite_to_set.preimage (assume i j _ _, plift.up.inj) } }
 end
 
 lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
@@ -1155,7 +1155,7 @@ lemma exists_finite_card_le_of_finite_of_linear_independent_of_span
   ∃h : finite s, h.to_finset.card ≤ ht.to_finset.card :=
 have s ⊆ (span K ↑(ht.to_finset) : submodule K V), by simp; assumption,
 let ⟨u, hust, hsu, eq⟩ := exists_of_linear_independent_of_finite_span hs this in
-have finite s, from finite_subset u.finite_to_set hsu,
+have finite s, from u.finite_to_set.subset hsu,
 ⟨this, by rw [←eq]; exact (finset.card_le_of_subset $ finset.coe_subset.mp $ by simp [hsu])⟩
 
 lemma linear_map.exists_left_inverse_of_injective (f : V →ₗ[K] V')
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index 5a015490ba81f..a2b31855f785c 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -72,7 +72,7 @@ begin
     { exact not_le_of_lt this ⟨set.embedding_of_subset _ _ hs⟩ },
     refine lt_of_le_of_lt (le_trans cardinal.mk_Union_le_sum_mk
       (cardinal.sum_le_sum _ (λ _, cardinal.omega) _)) _,
-    { exact λ j, le_of_lt (cardinal.lt_omega_iff_finite.2 $ finite_image _ (finset.finite_to_set _)) },
+    { exact λ j, le_of_lt (cardinal.lt_omega_iff_finite.2 $ (finset.finite_to_set _).image _) },
     { rwa [cardinal.sum_const, cardinal.mul_eq_max oJ (le_refl _), max_eq_left oJ] } },
   { rcases exists_finite_card_le_of_finite_of_linear_independent_of_span
       (cardinal.lt_omega_iff_finite.1 oJ) hv.1.to_subtype_range _ with ⟨fI, hi⟩,
diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean
index 0fdfcb3c12ca0..a47d4b5621081 100644
--- a/src/measure_theory/integration.lean
+++ b/src/measure_theory/integration.lean
@@ -2,14 +2,16 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl
+-/
+import measure_theory.measure_space
+import measure_theory.borel_space
 
-Lebesgue integral on `ennreal`.
+/-!
+# Lebesgue integral for `ennreal`-valued functions
 
 We define simple functions and show that each Borel measurable function on `ennreal` can be
 approximated by a sequence of simple functions.
 -/
-import measure_theory.measure_space
-import measure_theory.borel_space
 
 noncomputable theory
 open set (hiding restrict restrict_apply) filter
@@ -51,8 +53,7 @@ iff.intro
 
 /-- Constant function as a `simple_func`. -/
 def const (α) {β} [measurable_space α] (b : β) : α →ₛ β :=
-⟨λ a, b, λ x, is_measurable.const _,
-  finite_subset (set.finite_singleton b) $ by rintro _ ⟨a, rfl⟩; simp⟩
+⟨λ a, b, λ x, is_measurable.const _, finite_range_const⟩
 
 instance [inhabited β] : inhabited (α →ₛ β) := ⟨const _ (default _)⟩
 
@@ -62,8 +63,7 @@ lemma range_const (α) [measurable_space α] [nonempty α] (b : β) :
   (const α b).range = {b} :=
 begin
   ext b',
-  simp [mem_range],
-  tauto
+  simp [mem_range, eq_comm]
 end
 
 lemma is_measurable_cut (p : α → β → Prop) (f : α →ₛ β)
@@ -77,17 +77,18 @@ begin
 end
 
 theorem preimage_measurable (f : α →ₛ β) (s) : is_measurable (f ⁻¹' s) :=
-is_measurable_cut (λ _ b, b ∈ s) f (λ b, by simp [is_measurable.const])
+is_measurable_cut (λ _ b, b ∈ s) f (λ b, is_measurable.const (b ∈ s))
 
 /-- A simple function is measurable -/
-theorem measurable [measurable_space β] (f : α →ₛ β) : measurable f :=
+protected theorem measurable [measurable_space β] (f : α →ₛ β) : measurable f :=
 λ s _, preimage_measurable f s
 
+/-- If-then-else as a `simple_func`. -/
 def ite {s : set α} (hs : is_measurable s) (f g : α →ₛ β) : α →ₛ β :=
 ⟨λ a, if a ∈ s then f a else g a,
  λ x, by letI : measurable_space β := ⊤; exact
    measurable.if hs f.measurable g.measurable _ trivial,
- finite_subset (finite_union f.finite g.finite) begin
+ (f.finite.union g.finite).subset begin
    rintro _ ⟨a, rfl⟩,
    by_cases a ∈ s; simp [h],
    exacts [or.inl ⟨_, rfl⟩, or.inr ⟨_, rfl⟩]
@@ -101,7 +102,7 @@ then `f.bind g` binds the first argument of `g` to `f`. In other words, `f.bind
 def bind (f : α →ₛ β) (g : β → α →ₛ γ) : α →ₛ γ :=
 ⟨λa, g (f a) a,
  λ c, is_measurable_cut (λa b, g b a ∈ ({c} : set γ)) f (λ b, (g b).measurable_sn c),
- finite_subset (finite_bUnion f.finite (λ b, (g b).finite)) $
+ (f.finite.bUnion (λ b _, (g b).finite)).subset $
  by rintro _ ⟨a, rfl⟩; simp; exact ⟨a, a, rfl⟩⟩
 
 @[simp] theorem bind_apply (f : α →ₛ β) (g : β → α →ₛ γ) (a) :
diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean
index f76f986337c24..dc623e617f664 100644
--- a/src/measure_theory/simple_func_dense.lean
+++ b/src/measure_theory/simple_func_dense.lean
@@ -82,7 +82,7 @@ have x_mem_A' : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ A'
 have F_finite : ∀ {N}, finite (range (F N)) :=
 begin
   assume N, apply finite_range_ite,
-  { rw range_comp, apply finite_image, exact finite_range_find_greatest },
+  { rw range_comp, exact finite_range_find_greatest.image _ },
   { exact finite_range_const }
 end,
 -- prove that for all N, (F N) is a measurable function
diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean
index b14d487caec38..1f7d2a6ff3fc2 100644
--- a/src/order/filter/bases.lean
+++ b/src/order/filter/bases.lean
@@ -203,7 +203,7 @@ def filter_basis.of_sets (s : set (set α)) : filter_basis α :=
   nonempty := ⟨univ, ∅, ⟨⟨finite_empty, empty_subset s⟩, sInter_empty⟩⟩,
   inter_sets := begin
     rintros _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩,
-    exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨finite_union fina finb, union_subset suba subb⟩,
+    exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩,
            by rw sInter_union⟩,
   end }
 
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
index 2080387bf2376..90bd6ed22534e 100644
--- a/src/order/filter/basic.lean
+++ b/src/order/filter/basic.lean
@@ -256,7 +256,7 @@ begin
       exact ⟨t, hts, htfin, subset.trans hinter hVW⟩ },
     { rcases hV with ⟨t, hts, htfin, htinter⟩,
       rcases hW with ⟨z, hzs, hzfin, hzinter⟩,
-      refine ⟨t ∪ z, union_subset hts hzs, finite_union htfin hzfin, _⟩,
+      refine ⟨t ∪ z, union_subset hts hzs, htfin.union hzfin, _⟩,
       rw sInter_union,
       exact inter_subset_inter htinter hzinter } },
   { rcases h with ⟨t, ts, tfin, h⟩,
diff --git a/src/order/filter/cofinite.lean b/src/order/filter/cofinite.lean
index 5486cb7b92e1e..85d900e0b547f 100644
--- a/src/order/filter/cofinite.lean
+++ b/src/order/filter/cofinite.lean
@@ -31,9 +31,9 @@ def cofinite : filter α :=
 { sets             := {s | finite (- s)},
   univ_sets        := by simp only [compl_univ, finite_empty, mem_set_of_eq],
   sets_of_superset := assume s t (hs : finite (-s)) (st: s ⊆ t),
-    finite_subset hs $ compl_subset_compl.2 st,
+    hs.subset $ compl_subset_compl.2 st,
   inter_sets       := assume s t (hs : finite (-s)) (ht : finite (-t)),
-    by simp only [compl_inter, finite_union, ht, hs, mem_set_of_eq] }
+    by simp only [compl_inter, finite.union, ht, hs, mem_set_of_eq] }
 
 @[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite (-s) := iff.rfl
 
@@ -66,7 +66,7 @@ begin
     have := hs.to_finset.subset_range_sup_succ (finite.mem_to_finset.2 hbs),
     exact not_lt_of_le hb (finset.mem_range.1 this) },
   { rintros ⟨N, hN⟩,
-    apply finite_subset (finite_lt_nat N),
+    apply (finite_lt_nat N).subset,
     assume n hn,
     change n < N,
     exact lt_of_not_ge (λ hn', hn $ hN n hn') }
diff --git a/src/order/filter/ultrafilter.lean b/src/order/filter/ultrafilter.lean
index f010f5d58aaa5..d99d1c968b49d 100644
--- a/src/order/filter/ultrafilter.lean
+++ b/src/order/filter/ultrafilter.lean
@@ -79,7 +79,7 @@ assume h, (mem_or_mem_of_ultrafilter hf h).elim
 
 lemma mem_of_finite_Union_ultrafilter {is : set β} {s : β → set α}
   (hf : is_ultrafilter f) (his : finite is) (h : (⋃i∈is, s i) ∈ f) : ∃i∈is, s i ∈ f :=
-have his : finite (image s is), from finite_image s his,
+have his : finite (image s is), from his.image s,
 have h : (⋃₀ image s is) ∈ f, from by simp only [sUnion_image, set.sUnion_image]; assumption,
 let ⟨t, ⟨i, hi, h_eq⟩, (ht : t ∈ f)⟩ := mem_of_finite_sUnion_ultrafilter hf his h in
 ⟨i, hi, h_eq.symm ▸ ht⟩
diff --git a/src/ring_theory/free_comm_ring.lean b/src/ring_theory/free_comm_ring.lean
index 4b4ecbefe5e0d..8931c058d23bd 100644
--- a/src/ring_theory/free_comm_ring.lean
+++ b/src/ring_theory/free_comm_ring.lean
@@ -202,10 +202,10 @@ theorem exists_finite_support (x : free_comm_ring α) : ∃ s : set α, set.fini
 free_comm_ring.induction_on x
   ⟨∅, set.finite_empty, is_supported_neg is_supported_one⟩
   (λ p, ⟨{p}, set.finite_singleton p, is_supported_of.2 $ set.mem_singleton _⟩)
-  (λ x y ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩, ⟨s ∪ t, set.finite_union hfs hft, is_supported_add
+  (λ x y ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩, ⟨s ∪ t, hfs.union hft, is_supported_add
     (is_supported_upwards hxs $ set.subset_union_left s t)
     (is_supported_upwards hxt $ set.subset_union_right s t)⟩)
-  (λ x y ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩, ⟨s ∪ t, set.finite_union hfs hft, is_supported_mul
+  (λ x y ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩, ⟨s ∪ t, hfs.union hft, is_supported_mul
     (is_supported_upwards hxs $ set.subset_union_left s t)
     (is_supported_upwards hxt $ set.subset_union_right s t)⟩)
 
diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
index 3e9b27aeb6931..a13000f9c7f0b 100644
--- a/src/ring_theory/integral_closure.lean
+++ b/src/ring_theory/integral_closure.lean
@@ -262,10 +262,7 @@ begin
   rcases is_integral_iff_is_integral_closure_finite.1 hr with ⟨s, hfs, hr⟩,
   apply algebra.mem_bot.2, refine ⟨⟨_, _⟩, rfl⟩,
   refine (mem_integral_closure_iff_mem_fg _ _).2 ⟨algebra.adjoin _ (subtype.val '' s ∪ {r}),
-    algebra.fg_trans
-      (fg_adjoin_of_finite (set.finite_image _ hfs)
-        (λ y ⟨x, hx, hxy⟩, hxy ▸ x.2))
-      _,
+    algebra.fg_trans (fg_adjoin_of_finite (hfs.image _) (λ y ⟨x, hx, hxy⟩, hxy ▸ x.2)) _,
     algebra.subset_adjoin (or.inr rfl)⟩,
   refine fg_adjoin_singleton_of_integral _ _,
   rcases hr with ⟨p, hmp, hpx⟩,
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 976c7bc2b870b..a1a65bfa8ad6a 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -107,19 +107,19 @@ theorem fg_bot : (⊥ : submodule R M).fg :=
 theorem fg_sup {N₁ N₂ : submodule R M}
   (hN₁ : N₁.fg) (hN₂ : N₂.fg) : (N₁ ⊔ N₂).fg :=
 let ⟨t₁, ht₁⟩ := fg_def.1 hN₁, ⟨t₂, ht₂⟩ := fg_def.1 hN₂ in
-fg_def.2 ⟨t₁ ∪ t₂, finite_union ht₁.1 ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩
+fg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩
 
 variables {P : Type*} [add_comm_group P] [module R P]
 variables {f : M →ₗ[R] P}
 
 theorem fg_map {N : submodule R M} (hs : N.fg) : (N.map f).fg :=
-let ⟨t, ht⟩ := fg_def.1 hs in fg_def.2 ⟨f '' t, finite_image _ ht.1, by rw [span_image, ht.2]⟩
+let ⟨t, ht⟩ := fg_def.1 hs in fg_def.2 ⟨f '' t, ht.1.image _, by rw [span_image, ht.2]⟩
 
 theorem fg_prod {sb : submodule R M} {sc : submodule R P}
   (hsb : sb.fg) (hsc : sc.fg) : (sb.prod sc).fg :=
 let ⟨tb, htb⟩ := fg_def.1 hsb, ⟨tc, htc⟩ := fg_def.1 hsc in
 fg_def.2 ⟨prod.inl '' tb ∪ prod.inr '' tc,
-  finite_union (finite_image _ htb.1) (finite_image _ htc.1),
+  (htb.1.image _).union (htc.1.image _),
   by rw [linear_map.span_inl_union_inr, htb.2, htc.2]⟩
 
 variable (f)
@@ -330,7 +330,7 @@ theorem is_noetherian_iff_well_founded
       rcases IH (P ⊔ submodule.span R {x})
         ⟨@le_sup_left _ _ P _, this⟩
         (sup_le PN (submodule.span_le.2 (by simpa))) with ⟨s, hs, hs₂⟩,
-      refine ⟨insert x s, finite_insert _ hs, _⟩,
+      refine ⟨insert x s, hs.insert x, _⟩,
       rw [← hs₂, sup_assoc, ← submodule.span_union], simp }
   end⟩
 
diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean
index 76620c9965178..21852b3e4fc01 100644
--- a/src/topology/algebra/ordered.lean
+++ b/src/topology/algebra/ordered.lean
@@ -1097,7 +1097,7 @@ begin
   letI := classical.DLO α,
   rcases hs.elim_finite_subcover_image (λ x (_ : x ∈ s), @is_open_Ioi _ _ _ _ x) _
     with ⟨t, st, ft, ht⟩,
-  { refine H ((bdd_below_finite ft).imp $ λ C hC y hy, _),
+  { refine H (ft.bdd_below.imp $ λ C hC y hy, _),
     rcases mem_bUnion_iff.1 (ht hy) with ⟨x, hx, xy⟩,
     exact le_trans (hC hx) (le_of_lt xy) },
   { refine λ x hx, mem_bUnion_iff.2 (not_imp_comm.1 _ H),
diff --git a/src/topology/bases.lean b/src/topology/bases.lean
index e3883e4e4ab66..019cde8667a97 100644
--- a/src/topology/bases.lean
+++ b/src/topology/bases.lean
@@ -34,7 +34,7 @@ let b' := (λf, ⋂₀ f) '' {f:set (set α) | finite f ∧ f ⊆ s ∧ (⋂₀
 ⟨assume s₁ ⟨t₁, ⟨hft₁, ht₁b, ht₁⟩, eq₁⟩ s₂ ⟨t₂, ⟨hft₂, ht₂b, ht₂⟩, eq₂⟩,
     have ie : ⋂₀(t₁ ∪ t₂) = ⋂₀ t₁ ∩ ⋂₀ t₂, from Inf_union,
     eq₁ ▸ eq₂ ▸ assume x h,
-      ⟨_, ⟨t₁ ∪ t₂, ⟨finite_union hft₁ hft₂, union_subset ht₁b ht₂b,
+      ⟨_, ⟨t₁ ∪ t₂, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b,
         ie.symm ▸ ⟨_, h⟩⟩, ie⟩, h, subset.refl _⟩,
   eq_univ_iff_forall.2 $ assume a, ⟨univ, ⟨∅, ⟨finite_empty, empty_subset _,
     by rw sInter_empty; exact ⟨a, mem_univ a⟩⟩, sInter_empty⟩, mem_univ _⟩,
diff --git a/src/topology/basic.lean b/src/topology/basic.lean
index 1df828824c72a..04c440958feaf 100644
--- a/src/topology/basic.lean
+++ b/src/topology/basic.lean
@@ -643,14 +643,13 @@ def locally_finite (f : β → set α) :=
 ∀x:α, ∃t ∈ 𝓝 x, finite {i | (f i ∩ t).nonempty }
 
 lemma locally_finite_of_finite {f : β → set α} (h : finite (univ : set β)) : locally_finite f :=
-assume x, ⟨univ, univ_mem_sets, finite_subset h $ subset_univ _⟩
+assume x, ⟨univ, univ_mem_sets, h.subset $ subset_univ _⟩
 
 lemma locally_finite_subset
   {f₁ f₂ : β → set α} (hf₂ : locally_finite f₂) (hf : ∀b, f₁ b ⊆ f₂ b) : locally_finite f₁ :=
 assume a,
 let ⟨t, ht₁, ht₂⟩ := hf₂ a in
-⟨t, ht₁, finite_subset ht₂ $ assume i hi,
-   hi.mono $ inter_subset_inter (hf i) $ subset.refl _⟩
+⟨t, ht₁, ht₂.subset $ assume i hi, hi.mono $ inter_subset_inter (hf i) $ subset.refl _⟩
 
 lemma is_closed_Union_of_locally_finite {f : β → set α}
   (h₁ : locally_finite f) (h₂ : ∀i, is_closed (f i)) : is_closed (⋃i, f i) :=
diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean
index 1e07deee3013b..45a11fd123e47 100644
--- a/src/topology/instances/real.lean
+++ b/src/topology/instances/real.lean
@@ -229,8 +229,8 @@ metric.totally_bounded_iff.2 $ λ ε ε0, begin
   rcases exists_nat_gt ((b - a) / ε) with ⟨n, ba⟩,
   rw [div_lt_iff' ε0, sub_lt_iff_lt_add'] at ba,
   let s := (λ i:ℕ, a + ε * i) '' {i:ℕ | i < n},
-  refine ⟨s, finite_image _ ⟨set.fintype_lt_nat _⟩, λ x h, _⟩,
-  rcases h with ⟨ax, xb⟩,
+  refine ⟨s, (set.finite_lt_nat _).image _, _⟩,
+  rintro x ⟨ax, xb⟩,
   let i : ℕ := ⌊(x - a) / ε⌋.to_nat,
   have : (i : ℤ) = ⌊(x - a) / ε⌋ :=
     int.to_nat_of_nonneg (floor_nonneg.2 $ le_of_lt (div_pos (sub_pos.2 ax) ε0)),
diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean
index 37f459ae774f0..eecd551e8bafe 100644
--- a/src/topology/metric_space/closeds.lean
+++ b/src/topology/metric_space/closeds.lean
@@ -210,14 +210,14 @@ instance closeds.compact_space [compact_space α] : compact_space (closeds α) :
   -- `F` is finite
   { apply @finite_of_finite_image _ _ F (λf, f.val),
     { exact subtype.val_injective.inj_on F },
-    { refine finite_subset (finite_subsets_of_finite fs) (λb, _),
+    { refine 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 }},
   -- `F` is ε-dense
   { assume u _,
     rcases main u.val with ⟨t0, t0s, Dut0⟩,
-    have : is_closed t0 := closed_of_compact _ (finite_subset fs t0s).compact,
+    have : is_closed t0 := closed_of_compact _ (fs.subset t0s).compact,
     let t : closeds α := ⟨t0, this⟩,
     have : t ∈ F := t0s,
     have : edist u t < ε := lt_of_le_of_lt Dut0 δlt,
@@ -334,7 +334,7 @@ begin
       -- a : set α,  af : finite a,  ta : t.val ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2)
       -- replace each center by a nearby approximation in `s`, giving a new set `b`
       let b := F '' a,
-      have : finite b := finite_image _ af,
+      have : finite b := af.image _,
       have tb : ∀x ∈ t.val, ∃y ∈ b, edist x y < δ,
       { assume x hx,
         rcases mem_bUnion_iff.1 (ta hx) with ⟨z, za, Dxz⟩,
@@ -344,7 +344,7 @@ begin
              ... = δ : ennreal.add_halves _ },
       -- keep only the points in `b` that are close to point in `t`, yielding a new set `c`
       let c := {y ∈ b | ∃x∈t.val, edist x y < δ},
-      have : finite c := finite_subset ‹finite b› (λx hx, hx.1),
+      have : finite c := ‹finite b›.subset (λx hx, hx.1),
       -- points in `t` are well approximated by points in `c`
       have tc : ∀x ∈ t.val, ∃y ∈ c, edist x y ≤ δ,
       { assume x hx,
diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean
index 9806fa3e966e5..4faecece4f1c7 100644
--- a/src/topology/uniform_space/cauchy.lean
+++ b/src/topology/uniform_space/cauchy.lean
@@ -286,7 +286,7 @@ theorem totally_bounded_iff_subset {s : set α} : totally_bounded s ↔
   have : ∀ x : u, f x ∈ s ∧ (f x, x.1) ∈ r := λ x, classical.some_spec x.2.2,
   refine ⟨range f, _, _, _⟩,
   { exact range_subset_iff.2 (λ x, (this x).1) },
-  { have : finite u := finite_subset fk (λ x h, h.1),
+  { have : finite u := fk.subset (λ x h, h.1),
     exact ⟨@set.fintype_range _ _ _ _ this.fintype⟩ },
   { intros x xs,
     have := ks xs, simp at this,
@@ -332,7 +332,7 @@ assume t ht,
 have {p:α×α | (f p.1, f p.2) ∈ t} ∈ 𝓤 α,
   from hf ht,
 let ⟨c, hfc, hct⟩ := hs _ this in
-⟨f '' c, finite_image f hfc,
+⟨f '' c, hfc.image f,
   begin
     simp [image_subset_iff],
     simp [subset_def] at hct,
@@ -373,7 +373,7 @@ lemma totally_bounded_iff_filter {s : set α} :
   in
   have f ≠ ⊥,
     from infi_ne_bot_of_directed ⟨a⟩
-      (assume ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩, ⟨⟨t₁ ∪ t₂, finite_union ht₁ ht₂⟩,
+      (assume ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩, ⟨⟨t₁ ∪ t₂, ht₁.union ht₂⟩,
         principal_mono.mpr $ diff_subset_diff_right $ Union_subset_Union $
           assume t, Union_subset_Union_const or.inl,
         principal_mono.mpr $ diff_subset_diff_right $ Union_subset_Union $
diff --git a/src/topology/uniform_space/uniform_embedding.lean b/src/topology/uniform_space/uniform_embedding.lean
index a1047efadb7c8..560d878ef7818 100644
--- a/src/topology/uniform_space/uniform_embedding.lean
+++ b/src/topology/uniform_space/uniform_embedding.lean
@@ -293,7 +293,7 @@ lemma totally_bounded_preimage {f : α → β} {s : set β} (hf : uniform_embedd
   rcases mem_comap_sets.2 ht with ⟨t', ht', ts⟩,
   rcases totally_bounded_iff_subset.1
     (totally_bounded_subset (image_preimage_subset f s) hs) _ ht' with ⟨c, cs, hfc, hct⟩,
-  refine ⟨f ⁻¹' c, finite_preimage (hf.inj.inj_on _) hfc, λ x h, _⟩,
+  refine ⟨f ⁻¹' c, hfc.preimage (hf.inj.inj_on _), λ x h, _⟩,
   have := hct (mem_image_of_mem f h), simp at this ⊢,
   rcases this with ⟨z, zc, zt⟩,
   rcases cs zc with ⟨y, yc, rfl⟩,