diff --git a/src/algebra/algebraic_card.lean b/src/algebra/algebraic_card.lean
index 047fd6a866f88..cf43779263e5d 100644
--- a/src/algebra/algebraic_card.lean
+++ b/src/algebra/algebraic_card.lean
@@ -42,7 +42,7 @@ begin
     λ x, ulift.up (classical.some x.1.2),
   apply cardinal.mk_le_mk_mul_of_mk_preimage_le g (λ f, _),
   suffices : fintype (g ⁻¹' {f}),
-  { exact @mk_le_omega _ (@fintype.encodable _ this) },
+  { exact @mk_le_omega _ (@fintype.to_encodable _ this) },
   by_cases hf : f.1 = 0,
   { convert set.fintype_empty,
     apply set.eq_empty_iff_forall_not_mem.2 (λ x hx, _),
diff --git a/src/analysis/box_integral/partition/measure.lean b/src/analysis/box_integral/partition/measure.lean
index a216a433f8954..c060cee89227d 100644
--- a/src/analysis/box_integral/partition/measure.lean
+++ b/src/analysis/box_integral/partition/measure.lean
@@ -48,7 +48,7 @@ variables [fintype ι] (I : box ι)
 lemma measurable_set_coe : measurable_set (I : set (ι → ℝ)) :=
 begin
   rw [coe_eq_pi],
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   exact measurable_set.univ_pi (λ i, measurable_set_Ioc)
 end
 
diff --git a/src/computability/encoding.lean b/src/computability/encoding.lean
index 9fc7bb915e3f1..689fcc9360968 100644
--- a/src/computability/encoding.lean
+++ b/src/computability/encoding.lean
@@ -207,7 +207,7 @@ end
 lemma fin_encoding.card_le_omega {α : Type u} (e : fin_encoding α) :
   (# α) ≤ ω :=
 begin
-  haveI : encodable e.Γ := fintype.encodable _,
+  haveI : encodable e.Γ := fintype.to_encodable _,
   exact e.to_encoding.card_le_omega,
 end
 
diff --git a/src/data/W/basic.lean b/src/data/W/basic.lean
index c40fc1cf3436b..c359b858fd788 100644
--- a/src/data/W/basic.lean
+++ b/src/data/W/basic.lean
@@ -116,8 +116,6 @@ lemma depth_lt_depth_mk (a : α) (f : β a → W_type β) (i : β a) :
   depth (f i) < depth ⟨a, f⟩ :=
 nat.lt_succ_of_le (finset.le_sup (finset.mem_univ i))
 
-end W_type
-
 /-
 Show that W types are encodable when `α` is an encodable fintype and for every `a : α`, `β a` is
 encodable.
@@ -127,13 +125,11 @@ induction on `n` that these are all encodable. These auxiliary constructions are
 and of themselves, so we mark them as `private`.
 -/
 
-namespace encodable
-
 @[reducible] private def W_type' {α : Type*} (β : α → Type*)
     [Π a : α, fintype (β a)] [Π a : α, encodable (β a)] (n : ℕ) :=
 { t : W_type β // t.depth ≤ n}
 
-variables {α : Type*} {β : α → Type*} [Π a : α, fintype (β a)] [Π a : α, encodable (β a)]
+variables [Π a : α, encodable (β a)]
 
 private def encodable_zero : encodable (W_type' β 0) :=
 let f    : W_type' β 0 → empty := λ ⟨x, h⟩, false.elim $ not_lt_of_ge h (W_type.depth_pos _),
@@ -176,4 +172,4 @@ begin
   exact encodable.of_left_inverse f finv this
 end
 
-end encodable
+end W_type
diff --git a/src/data/rat/denumerable.lean b/src/data/rat/denumerable.lean
index 40f68559ecfa2..c0caa16a68cd6 100644
--- a/src/data/rat/denumerable.lean
+++ b/src/data/rat/denumerable.lean
@@ -28,7 +28,7 @@ instance : denumerable ℚ :=
 begin
   let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.nat_abs.coprime x.2 },
   letI : infinite T := infinite.of_injective _ denumerable_aux.injective,
-  letI : encodable T := encodable.subtype,
+  letI : encodable T := subtype.encodable,
   letI : denumerable T := of_encodable_of_infinite T,
   exact denumerable.of_equiv T denumerable_aux
 end
diff --git a/src/data/set/countable.lean b/src/data/set/countable.lean
index 88a77e31ca1a8..593b5da0df82f 100644
--- a/src/data/set/countable.lean
+++ b/src/data/set/countable.lean
@@ -185,7 +185,7 @@ lemma countable.insert {s : set α} (a : α) (h : countable s) : countable (inse
 countable_insert.2 h
 
 lemma finite.countable {s : set α} : finite s → countable s
-| ⟨h⟩ := trunc.nonempty (by exactI trunc_encodable_of_fintype s)
+| ⟨h⟩ := trunc.nonempty (by exactI fintype.trunc_encodable s)
 
 lemma subsingleton.countable {s : set α} (hs : s.subsingleton) : countable s :=
 hs.finite.countable
diff --git a/src/data/tprod.lean b/src/data/tprod.lean
index e5aff2b8f0c50..a653cb6bcb69c 100644
--- a/src/data/tprod.lean
+++ b/src/data/tprod.lean
@@ -23,7 +23,7 @@ construction/theorem that is easier to define/prove on binary products than on f
 * Then we can use the equivalence `list.tprod.pi_equiv_tprod` below (or enhanced versions of it,
   like a `measurable_equiv` for product measures) to get the construction on `Π i : ι, α i`, at
   least when assuming `[fintype ι] [encodable ι]` (using `encodable.sorted_univ`).
-  Using `local attribute [instance] fintype.encodable` we can get rid of the argument
+  Using `local attribute [instance] fintype.to_encodable` we can get rid of the argument
   `[encodable ι]`.
 
 ## Main definitions
diff --git a/src/logic/encodable/basic.lean b/src/logic/encodable/basic.lean
index c39912d3f5b58..993780e8eb558 100644
--- a/src/logic/encodable/basic.lean
+++ b/src/logic/encodable/basic.lean
@@ -84,16 +84,16 @@ of_left_inverse e e.symm e.left_inv
 @[simp] theorem decode_of_equiv {α β} [encodable α] (e : β ≃ α) (n : ℕ) :
   @decode _ (of_equiv _ e) n = (decode α n).map e.symm := rfl
 
-instance nat : encodable ℕ :=
+instance _root_.nat.encodable : encodable ℕ :=
 ⟨id, some, λ a, rfl⟩
 
 @[simp] theorem encode_nat (n : ℕ) : encode n = n := rfl
 @[simp] theorem decode_nat (n : ℕ) : decode ℕ n = some n := rfl
 
-@[priority 100] instance is_empty [is_empty α] : encodable α :=
+@[priority 100] instance _root_.is_empty.to_encodable [is_empty α] : encodable α :=
 ⟨is_empty_elim, λ n, none, is_empty_elim⟩
 
-instance unit : encodable punit :=
+instance _root_.punit.encodable : encodable punit :=
 ⟨λ_, 0, λ n, nat.cases_on n (some punit.star) (λ _, none), λ _, by simp⟩
 
 @[simp] theorem encode_star : encode punit.star = 0 := rfl
@@ -102,7 +102,7 @@ instance unit : encodable punit :=
 @[simp] theorem decode_unit_succ (n) : decode punit (succ n) = none := rfl
 
 /-- If `α` is encodable, then so is `option α`. -/
-instance option {α : Type*} [h : encodable α] : encodable (option α) :=
+instance _root_.option.encodable {α : Type*} [h : encodable α] : encodable (option α) :=
 ⟨λ o, option.cases_on o nat.zero (λ a, succ (encode a)),
  λ n, nat.cases_on n (some none) (λ m, (decode α m).map some),
  λ o, by cases o; dsimp; simp [encodek, nat.succ_ne_zero]⟩
@@ -193,7 +193,7 @@ match bodd_div2 n with
 end
 
 /-- If `α` and `β` are encodable, then so is their sum. -/
-instance sum : encodable (α ⊕ β) :=
+instance _root_.sum.encodable : encodable (α ⊕ β) :=
 ⟨encode_sum, decode_sum, λ s,
   by cases s; simp [encode_sum, decode_sum, encodek]; refl⟩
 
@@ -206,7 +206,7 @@ instance sum : encodable (α ⊕ β) :=
 
 end sum
 
-instance bool : encodable bool :=
+instance _root_.bool.encodable : encodable bool :=
 of_equiv (unit ⊕ unit) equiv.bool_equiv_punit_sum_punit
 
 @[simp] theorem encode_tt : encode tt = 1 := rfl
@@ -226,7 +226,7 @@ begin
   simp [decode_sum]; cases bodd n; simp [decode_sum]; rw e; refl
 end
 
-noncomputable instance «Prop» : encodable Prop :=
+noncomputable instance _root_.Prop.encodable : encodable Prop :=
 of_equiv bool equiv.Prop_equiv_bool
 
 section sigma
@@ -241,7 +241,7 @@ def decode_sigma (n : ℕ) : option (sigma γ) :=
 let (n₁, n₂) := unpair n in
 (decode α n₁).bind $ λ a, (decode (γ a) n₂).map $ sigma.mk a
 
-instance sigma : encodable (sigma γ) :=
+instance _root_.sigma.encodable : encodable (sigma γ) :=
 ⟨encode_sigma, decode_sigma, λ ⟨a, b⟩,
   by simp [encode_sigma, decode_sigma, unpair_mkpair, encodek]⟩
 
@@ -258,7 +258,7 @@ section prod
 variables [encodable α] [encodable β]
 
 /-- If `α` and `β` are encodable, then so is their product. -/
-instance prod : encodable (α × β) :=
+instance _root_.prod.encodable : encodable (α × β) :=
 of_equiv _ (equiv.sigma_equiv_prod α β).symm
 
 @[simp] theorem decode_prod_val (n : ℕ) : decode (α × β) n =
@@ -289,7 +289,7 @@ def decode_subtype (v : ℕ) : option {a : α // P a} :=
 if h : P a then some ⟨a, h⟩ else none
 
 /-- A decidable subtype of an encodable type is encodable. -/
-instance subtype : encodable {a : α // P a} :=
+instance _root_.subtype.encodable : encodable {a : α // P a} :=
 ⟨encode_subtype, decode_subtype,
  λ ⟨v, h⟩, by simp [encode_subtype, decode_subtype, encodek, h]⟩
 
@@ -298,21 +298,21 @@ by cases a; refl
 
 end subtype
 
-instance fin (n) : encodable (fin n) :=
+instance _root_.fin.encodable (n) : encodable (fin n) :=
 of_equiv _ (equiv.fin_equiv_subtype _)
 
-instance int : encodable ℤ :=
+instance _root_.int.encodable : encodable ℤ :=
 of_equiv _ equiv.int_equiv_nat
 
-instance pnat : encodable ℕ+ :=
+instance _root_.pnat.encodable : encodable ℕ+ :=
 of_equiv _ equiv.pnat_equiv_nat
 
 /-- The lift of an encodable type is encodable. -/
-instance ulift [encodable α] : encodable (ulift α) :=
+instance _root_.ulift.encodable [encodable α] : encodable (ulift α) :=
 of_equiv _ equiv.ulift
 
 /-- The lift of an encodable type is encodable. -/
-instance plift [encodable α] : encodable (plift α) :=
+instance _root_.plift.encodable [encodable α] : encodable (plift α) :=
 of_equiv _ equiv.plift
 
 /-- If `β` is encodable and there is an injection `f : α → β`, then `α` is encodable as well. -/
diff --git a/src/logic/equiv/list.lean b/src/logic/equiv/list.lean
index 52d92d334d536..523c5832cb68d 100644
--- a/src/logic/equiv/list.lean
+++ b/src/logic/equiv/list.lean
@@ -37,7 +37,7 @@ def decode_list : ℕ → option (list α)
 
 /-- If `α` is encodable, then so is `list α`. This uses the `mkpair` and `unpair` functions from
 `data.nat.pairing`. -/
-instance list : encodable (list α) :=
+instance _root_.list.encodable : encodable (list α) :=
 ⟨encode_list, decode_list, λ l,
   by induction l with a l IH; simp [encode_list, decode_list, unpair_mkpair, encodek, *]⟩
 
@@ -84,7 +84,7 @@ def decode_multiset (n : ℕ) : option (multiset α) :=
 coe <$> decode (list α) n
 
 /-- If `α` is encodable, then so is `multiset α`. -/
-instance multiset : encodable (multiset α) :=
+instance _root_.multiset.encodable : encodable (multiset α) :=
 ⟨encode_multiset, decode_multiset,
  λ s, by simp [encode_multiset, decode_multiset, encodek]⟩
 
@@ -94,7 +94,9 @@ end finset
 def encodable_of_list [decidable_eq α] (l : list α) (H : ∀ x, x ∈ l) : encodable α :=
 ⟨λ a, index_of a l, l.nth, λ a, index_of_nth (H _)⟩
 
-def trunc_encodable_of_fintype (α : Type*) [decidable_eq α] [fintype α] : trunc (encodable α) :=
+/-- A finite type is encodable. Because the encoding is not unique, we wrap it in `trunc` to
+preserve computability. -/
+def _root_.fintype.trunc_encodable (α : Type*) [decidable_eq α] [fintype α] : trunc (encodable α) :=
 @@quot.rec_on_subsingleton _
   (λ s : multiset α, (∀ x:α, x ∈ s) → trunc (encodable α)) _
   finset.univ.1
@@ -102,14 +104,13 @@ def trunc_encodable_of_fintype (α : Type*) [decidable_eq α] [fintype α] : tru
   finset.mem_univ
 
 /-- A noncomputable way to arbitrarily choose an ordering on a finite type.
-  It is not made into a global instance, since it involves an arbitrary choice.
-  This can be locally made into an instance with `local attribute [instance] fintype.encodable`. -/
-noncomputable def _root_.fintype.encodable (α : Type*) [fintype α] : encodable α :=
-by { classical, exact (encodable.trunc_encodable_of_fintype α).out }
+It is not made into a global instance, since it involves an arbitrary choice.
+This can be locally made into an instance with `local attribute [instance] fintype.to_encodable`. -/
+noncomputable def _root_.fintype.to_encodable (α : Type*) [fintype α] : encodable α :=
+by { classical, exact (fintype.trunc_encodable α).out }
 
 /-- If `α` is encodable, then so is `vector α n`. -/
-instance vector [encodable α] {n} : encodable (vector α n) :=
-encodable.subtype
+instance _root_.vector.encodable [encodable α] {n} : encodable (vector α n) := subtype.encodable
 
 /-- If `α` is encodable, then so is `fin n → α`. -/
 instance fin_arrow [encodable α] {n} : encodable (fin n → α) :=
@@ -119,26 +120,31 @@ instance fin_pi (n) (π : fin n → Type*) [∀ i, encodable (π i)] : encodable
 of_equiv _ (equiv.pi_equiv_subtype_sigma (fin n) π)
 
 /-- If `α` is encodable, then so is `array n α`. -/
-instance array [encodable α] {n} : encodable (array n α) :=
+instance _root_.array.encodable [encodable α] {n} : encodable (array n α) :=
 of_equiv _ (equiv.array_equiv_fin _ _)
 
 /-- If `α` is encodable, then so is `finset α`. -/
-instance finset [encodable α] : encodable (finset α) :=
+instance _root_.finset.encodable [encodable α] : encodable (finset α) :=
 by haveI := decidable_eq_of_encodable α; exact
  of_equiv {s : multiset α // s.nodup}
   ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
 
+-- TODO: Unify with `fintype_pi` and find a better name
+/-- When `α` is finite and `β` is encodable, `α → β` is encodable too. Because the encoding is not
+unique, we wrap it in `trunc` to preserve computability. -/
 def fintype_arrow (α : Type*) (β : Type*) [decidable_eq α] [fintype α] [encodable β] :
   trunc (encodable (α → β)) :=
 (fintype.trunc_equiv_fin α).map $
   λ f, encodable.of_equiv (fin (fintype.card α) → β) $
   equiv.arrow_congr f (equiv.refl _)
 
+/-- When `α` is finite and all `π a` are encodable, `Π a, π a` is encodable too. Because the
+encoding is not unique, we wrap it in `trunc` to preserve computability. -/
 def fintype_pi (α : Type*) (π : α → Type*) [decidable_eq α] [fintype α] [∀ a, encodable (π a)] :
   trunc (encodable (Π a, π a)) :=
-(encodable.trunc_encodable_of_fintype α).bind $ λ a,
-  (@fintype_arrow α (Σa, π a) _ _ (@encodable.sigma _ _ a _)).bind $ λ f,
-  trunc.mk $ @encodable.of_equiv _ _ (@encodable.subtype _ _ f _) (equiv.pi_equiv_subtype_sigma α π)
+(fintype.trunc_encodable α).bind $ λ a,
+  (@fintype_arrow α (Σa, π a) _ _ (@sigma.encodable _ _ a _)).bind $ λ f,
+  trunc.mk $ @encodable.of_equiv _ _ (@subtype.encodable _ _ f _) (equiv.pi_equiv_subtype_sigma α π)
 
 /-- The elements of a `fintype` as a sorted list. -/
 def sorted_univ (α) [fintype α] [encodable α] : list α :=
@@ -248,7 +254,7 @@ lemma raise_sorted : ∀ l n, list.sorted (≤) (raise l n)
 | (m :: l) n := (list.chain_iff_pairwise (@le_trans _ _)).1 (raise_chain _ _)
 
 /-- If `α` is denumerable, then so is `multiset α`. Warning: this is *not* the same encoding as used
-in `encodable.multiset`. -/
+in `multiset.encodable`. -/
 instance multiset : denumerable (multiset α) := mk' ⟨
   λ s : multiset α, encode $ lower ((s.map encode).sort (≤)) 0,
   λ n, multiset.map (of_nat α) (raise (of_nat (list ℕ) n) 0),
@@ -301,7 +307,7 @@ def raise'_finset (l : list ℕ) (n : ℕ) : finset ℕ :=
 ⟨raise' l n, (raise'_sorted _ _).imp (@ne_of_lt _ _)⟩
 
 /-- If `α` is denumerable, then so is `finset α`. Warning: this is *not* the same encoding as used
-in `encodable.finset`. -/
+in `finset.encodable`. -/
 instance finset : denumerable (finset α) := mk' ⟨
   λ s : finset α, encode $ lower' ((s.map (eqv α).to_embedding).sort (≤)) 0,
   λ n, finset.map (eqv α).symm.to_embedding (raise'_finset (of_nat (list ℕ) n) 0),
diff --git a/src/measure_theory/constructions/borel_space.lean b/src/measure_theory/constructions/borel_space.lean
index c26b146289473..406e6b7dc175a 100644
--- a/src/measure_theory/constructions/borel_space.lean
+++ b/src/measure_theory/constructions/borel_space.lean
@@ -363,7 +363,7 @@ instance pi.opens_measurable_space_fintype {ι : Type*} {π : ι → Type*} [fin
   [Π i, measurable_space (π i)] [∀ i, second_countable_topology (π i)]
   [∀ i, opens_measurable_space (π i)] :
   opens_measurable_space (Π i, π i) :=
-by { letI := fintype.encodable ι, apply_instance }
+by { letI := fintype.to_encodable ι, apply_instance }
 
 instance prod.opens_measurable_space [second_countable_topology α] [second_countable_topology β] :
   opens_measurable_space (α × β) :=
diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean
index b6ee3eba3155a..1187a6f8411a1 100644
--- a/src/measure_theory/constructions/pi.lean
+++ b/src/measure_theory/constructions/pi.lean
@@ -83,7 +83,7 @@ lemma is_countably_spanning.pi {C : Π i, set (set (α i))}
   is_countably_spanning (pi univ '' pi univ C) :=
 begin
   choose s h1s h2s using hC,
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget,
   refine ⟨λ n, pi univ (λ i, s i (e n i)), λ n, mem_image_of_mem _ (λ i _, h1s i _), _⟩,
   simp_rw [(surjective_decode_iget (ι → ℕ)).Union_comp (λ x, pi univ (λ i, s i (x i))),
@@ -96,7 +96,7 @@ lemma generate_from_pi_eq {C : Π i, set (set (α i))}
   (hC : ∀ i, is_countably_spanning (C i)) :
   @measurable_space.pi _ _ (λ i, generate_from (C i)) = generate_from (pi univ '' pi univ C) :=
 begin
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   apply le_antisymm,
   { refine supr_le _, intro i, rw [comap_generate_from],
     apply generate_from_le, rintro _ ⟨s, hs, rfl⟩, dsimp,
@@ -277,7 +277,7 @@ begin
   refine le_antisymm _ _,
   { rw [measure.pi, to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i))],
     apply outer_measure.pi_pi_le },
-  { haveI : encodable ι := fintype.encodable ι,
+  { haveI : encodable ι := fintype.to_encodable ι,
     rw [← pi'_pi μ s],
     simp_rw [← pi'_pi μ s, measure.pi,
       to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i)), ← to_outer_measure_apply],
@@ -298,7 +298,7 @@ def finite_spanning_sets_in.pi {C : Π i, set (set (α i))}
   (measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) :=
 begin
   haveI := λ i, (hμ i).sigma_finite,
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   refine ⟨λ n, pi univ (λ i, (hμ i).set ((decode (ι → ℕ) n).iget i)), λ n, _, λ n, _, _⟩;
   -- TODO (kmill) If this let comes before the refine, while the noncomputability checker
   -- correctly sees this definition is computable, the Lean VM fails to see the binding is
@@ -357,7 +357,7 @@ eq.symm $ pi_eq $ λ s hs, pi'_pi μ s
 
 @[simp] lemma pi_pi (s : Π i, set (α i)) : measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
 begin
-  haveI : encodable ι := fintype.encodable ι,
+  haveI : encodable ι := fintype.to_encodable ι,
   rw [← pi'_eq_pi, pi'_pi]
 end
 
diff --git a/src/measure_theory/function/strongly_measurable.lean b/src/measure_theory/function/strongly_measurable.lean
index 9e150a1a356df..e3a3b6767d8e1 100644
--- a/src/measure_theory/function/strongly_measurable.lean
+++ b/src/measure_theory/function/strongly_measurable.lean
@@ -1693,7 +1693,7 @@ begin
   { rw tendsto_pi_nhds,
     exact λ p, ht_sf p.fst p.snd, },
   refine measurable_of_tendsto_metric (λ n, _) h_tendsto,
-  haveI : encodable (t_sf n).range, from fintype.encodable ↥(t_sf n).range,
+  haveI : encodable (t_sf n).range, from fintype.to_encodable ↥(t_sf n).range,
   have h_meas : measurable (λ (p : (t_sf n).range × α), u ↑p.fst p.snd),
   { have : (λ (p : ↥((t_sf n).range) × α), u ↑(p.fst) p.snd)
         = (λ (p : α × ((t_sf n).range)), u ↑(p.snd) p.fst) ∘ prod.swap := rfl,
@@ -1725,7 +1725,7 @@ begin
   { rw tendsto_pi_nhds,
     exact λ p, ht_sf p.fst p.snd, },
   refine strongly_measurable_of_tendsto _ (λ n, _) h_tendsto,
-  haveI : encodable (t_sf n).range, from fintype.encodable ↥(t_sf n).range,
+  haveI : encodable (t_sf n).range, from fintype.to_encodable ↥(t_sf n).range,
   have h_str_meas : strongly_measurable (λ (p : (t_sf n).range × α), u ↑p.fst p.snd),
   { refine strongly_measurable_iff_measurable_separable.2 ⟨_, _⟩,
     { have : (λ (p : ↥((t_sf n).range) × α), u ↑(p.fst) p.snd)
diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean
index 8e230a3f2a916..db26adea3cbf7 100644
--- a/src/measure_theory/measurable_space.lean
+++ b/src/measure_theory/measurable_space.lean
@@ -735,7 +735,7 @@ end
 
 section fintype
 
-local attribute [instance] fintype.encodable
+local attribute [instance] fintype.to_encodable
 
 lemma measurable_set.pi_fintype [fintype δ] {s : set δ} {t : Π i, set (π i)}
   (ht : ∀ i ∈ s, measurable_set (t i)) : measurable_set (pi s t) :=
diff --git a/src/measure_theory/measurable_space_def.lean b/src/measure_theory/measurable_space_def.lean
index a33fac10826da..f554b603bf85f 100644
--- a/src/measure_theory/measurable_space_def.lean
+++ b/src/measure_theory/measurable_space_def.lean
@@ -140,7 +140,7 @@ by { rw compl_Inter, exact measurable_set.Union (λ b, (h b).compl) }
 
 section fintype
 
-local attribute [instance] fintype.encodable
+local attribute [instance] fintype.to_encodable
 
 lemma measurable_set.Union_fintype [fintype β] {f : β → set α} (h : ∀ b, measurable_set (f b)) :
   measurable_set (⋃ b, f b) :=
diff --git a/src/measure_theory/measure/hausdorff.lean b/src/measure_theory/measure/hausdorff.lean
index f557606b4dbfe..10076b104abbb 100644
--- a/src/measure_theory/measure/hausdorff.lean
+++ b/src/measure_theory/measure/hausdorff.lean
@@ -542,7 +542,7 @@ lemma mk_metric_le_liminf_sum {β : Type*} {ι : β → Type*} [hι : ∀ n, fin
   (m : ℝ≥0∞ → ℝ≥0∞) :
   mk_metric m s ≤ liminf l (λ n, ∑ i, m (diam (t n i))) :=
 begin
-  haveI : ∀ n, encodable (ι n), from λ n, fintype.encodable _,
+  haveI : ∀ n, encodable (ι n), from λ n, fintype.to_encodable _,
   simpa only [tsum_fintype] using mk_metric_le_liminf_tsum s r hr t ht hst m,
 end
 
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
index fee1c87ab7ca0..b29391b96c74e 100644
--- a/src/measure_theory/measure/measure_space.lean
+++ b/src/measure_theory/measure/measure_space.lean
@@ -2606,7 +2606,7 @@ end
 instance sum.sigma_finite {ι} [fintype ι] (μ : ι → measure α) [∀ i, sigma_finite (μ i)] :
   sigma_finite (sum μ) :=
 begin
-  haveI : encodable ι := fintype.encodable ι,
+  haveI : encodable ι := fintype.to_encodable ι,
   have : ∀ n, measurable_set (⋂ (i : ι), spanning_sets (μ i) n) :=
     λ n, measurable_set.Inter (λ i, measurable_spanning_sets (μ i) n),
   refine ⟨⟨⟨λ n, ⋂ i, spanning_sets (μ i) n, λ _, trivial, λ n, _, _⟩⟩⟩,
diff --git a/src/model_theory/basic.lean b/src/model_theory/basic.lean
index 67a23e5daa485..9486e6f94133f 100644
--- a/src/model_theory/basic.lean
+++ b/src/model_theory/basic.lean
@@ -173,7 +173,7 @@ instance countable_empty : language.empty.countable :=
 ⟨begin
   rw [card_eq_card_functions_add_card_relations, add_le_omega, lift_le_omega, lift_le_omega,
     ← cardinal.encodable_iff, ← cardinal.encodable_iff],
-  exact ⟨⟨encodable.sigma⟩, ⟨encodable.sigma⟩⟩,
+  exact ⟨⟨sigma.encodable⟩, ⟨sigma.encodable⟩⟩,
 end⟩
 
 @[priority 100] instance countable.countable_functions [L.countable] :
diff --git a/src/model_theory/encoding.lean b/src/model_theory/encoding.lean
index 9a731f1687f25..61d38de7bd39f 100644
--- a/src/model_theory/encoding.lean
+++ b/src/model_theory/encoding.lean
@@ -109,8 +109,8 @@ begin
   have h := (mk_le_of_injective list_encode_injective),
   refine h.trans _,
   casesI fintype_or_infinite (α ⊕ Σ i, L.functions i) with ft inf,
-  { haveI := fintype.encodable (α ⊕ Σ i, L.functions i),
-    exact le_add_left (encodable_iff.1 ⟨encodable.list⟩) },
+  { haveI := fintype.to_encodable (α ⊕ Σ i, L.functions i),
+    exact le_add_left mk_le_omega },
   { rw mk_list_eq_mk,
     exact le_self_add }
 end
diff --git a/src/set_theory/cardinal_ordinal.lean b/src/set_theory/cardinal_ordinal.lean
index f308dc381a89d..fa9e2fcbe791c 100644
--- a/src/set_theory/cardinal_ordinal.lean
+++ b/src/set_theory/cardinal_ordinal.lean
@@ -668,7 +668,7 @@ mk_le_omega.antisymm (omega_le_mk _)
 theorem mk_list_eq_max_mk_omega (α : Type u) [nonempty α] : #(list α) = max (#α) ω :=
 begin
   casesI fintype_or_infinite α,
-  { haveI : encodable α := fintype.encodable α,
+  { haveI : encodable α := fintype.to_encodable α,
     rw [mk_list_eq_omega, eq_comm, max_eq_right],
     exact mk_le_omega },
   { rw [mk_list_eq_mk, eq_comm, max_eq_left],
@@ -678,7 +678,7 @@ end
 theorem mk_list_le_max (α : Type u) : #(list α) ≤ max ω (#α) :=
 begin
   casesI fintype_or_infinite α,
-  { haveI := fintype.encodable α,
+  { haveI := fintype.to_encodable α,
     exact mk_le_omega.trans (le_max_left _ _) },
   { rw mk_list_eq_mk,
     apply le_max_right }
diff --git a/src/topology/bases.lean b/src/topology/bases.lean
index 03ba9901ad577..7c83edd7206ab 100644
--- a/src/topology/bases.lean
+++ b/src/topology/bases.lean
@@ -291,7 +291,7 @@ def dense_seq [separable_space α] [nonempty α] : ℕ → α := classical.some
 variable {α}
 
 @[priority 100]
-instance encodable.separable_space [encodable α] : separable_space α :=
+instance encodable.to_separable_space [encodable α] : separable_space α :=
 { exists_countable_dense := ⟨set.univ, set.countable_encodable set.univ, dense_univ⟩ }
 
 lemma separable_space_of_dense_range {ι : Type*} [encodable ι] (u : ι → α) (hu : dense_range u) :
@@ -648,7 +648,7 @@ end
 instance second_countable_topology_fintype {ι : Type*} {π : ι → Type*}
   [fintype ι] [t : ∀a, topological_space (π a)] [∀a, second_countable_topology (π a)] :
   second_countable_topology (∀a, π a) :=
-by { letI := fintype.encodable ι, exact topological_space.second_countable_topology_encodable }
+by { letI := fintype.to_encodable ι, exact topological_space.second_countable_topology_encodable }
 
 @[priority 100] -- see Note [lower instance priority]
 instance second_countable_topology.to_separable_space
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 2d0bc2d6c43ba..fd876bd513ba6 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -1577,7 +1577,7 @@ lemma _root_.topological_space.is_separable.separable_space {s : set α} (hs : i
 begin
   classical,
   rcases eq_empty_or_nonempty s with rfl|⟨⟨x₀, x₀s⟩⟩,
-  { haveI : encodable (∅ : set α) := fintype.encodable ↥∅, exact encodable.separable_space },
+  { haveI : encodable (∅ : set α) := fintype.to_encodable ↥∅, exact encodable.to_separable_space },
   rcases hs with ⟨c, hc, h'c⟩,
   haveI : encodable c := hc.to_encodable,
   obtain ⟨u, -, u_pos, u_lim⟩ : ∃ (u : ℕ → ℝ), strict_anti u ∧ (∀ (n : ℕ), 0 < u n) ∧