diff --git a/archive/100-theorems-list/82_cubing_a_cube.lean b/archive/100-theorems-list/82_cubing_a_cube.lean
index a1b698a3069d1..cbfd9936ff2ae 100644
--- a/archive/100-theorems-list/82_cubing_a_cube.lean
+++ b/archive/100-theorems-list/82_cubing_a_cube.lean
@@ -314,7 +314,7 @@ begin
   swap, exact ⟨mi h v, mi_mem_bcubes⟩,
   apply lt_of_lt_of_le _ (b_add_w_le_one h), exact i, exact 0,
   rw [xm, mi_mem_bcubes.1, hi.1, _root_.add_lt_add_iff_left],
-  apply mi_strict_minimal _ hi, intro h', apply h2i, rw subtype.ext, exact h'
+  apply mi_strict_minimal _ hi, intro h', apply h2i, rw subtype.ext_iff_val, exact h'
 end
 
 /-- If `mi` lies on the boundary of the valley in dimension j, then this lemma expresses that all
diff --git a/src/algebra/category/CommRing/limits.lean b/src/algebra/category/CommRing/limits.lean
index 040cbc2021ed8..522b2dc32427e 100644
--- a/src/algebra/category/CommRing/limits.lean
+++ b/src/algebra/category/CommRing/limits.lean
@@ -118,14 +118,10 @@ begin
   refine is_limit.of_faithful
     (forget CommRing) (limit.is_limit _)
     (λ s, ⟨_, _, _, _, _⟩) (λ s, rfl); dsimp,
-  { apply subtype.eq, funext, dsimp,
-    erw (s.π.app j).map_one, refl },
-  { intros x y, apply subtype.eq, funext, dsimp,
-    erw (s.π.app j).map_mul, refl },
-  { apply subtype.eq, funext, dsimp,
-    erw (s.π.app j).map_zero, refl },
-  { intros x y, apply subtype.eq, funext, dsimp,
-    erw (s.π.app j).map_add, refl }
+  { ext j, dsimp, rw (s.π.app j).map_one },
+  { intros x y, ext j, dsimp, rw (s.π.app j).map_mul },
+  { ext j, dsimp, rw (s.π.app j).map_zero, refl },
+  { intros x y, ext j, dsimp, rw (s.π.app j).map_add, refl }
 end
 
 end CommRing_has_limits
diff --git a/src/algebra/category/Group/images.lean b/src/algebra/category/Group/images.lean
index 32c082b6430a4..dc5e29e8a7938 100644
--- a/src/algebra/category/Group/images.lean
+++ b/src/algebra/category/Group/images.lean
@@ -18,7 +18,7 @@ namespace AddCommGroup
 
 variables {G H : AddCommGroup.{0}} (f : G ⟶ H)
 
-local attribute [ext] subtype.eq'
+local attribute [ext] subtype.ext_val
 
 section -- implementation details of `has_image` for AddCommGroup; use the API, not these
 /-- the image of a morphism in AddCommGroup is just the bundling of `set.range f` -/
diff --git a/src/algebra/category/Module/basic.lean b/src/algebra/category/Module/basic.lean
index 22d043ef9d0a0..152e9ef8c67c1 100644
--- a/src/algebra/category/Module/basic.lean
+++ b/src/algebra/category/Module/basic.lean
@@ -155,7 +155,7 @@ def kernel_is_limit : is_limit (kernel_cone f) :=
     { erw @linear_map.subtype_comp_cod_restrict _ _ _ _ _ _ _ _ (fork.ι s) f.ker _ },
     { rw [←fork.app_zero_left, ←fork.app_zero_left], refl }
   end,
-  uniq' := λ s m h, linear_map.ext $ λ x, subtype.ext.2 $
+  uniq' := λ s m h, linear_map.ext $ λ x, subtype.ext_iff_val.2 $
     have h₁ : (m ≫ (kernel_cone f).π.app zero).to_fun = (s.π.app zero).to_fun,
     by { congr, exact h zero },
     by convert @congr_fun _ _ _ _ h₁ x }
diff --git a/src/algebra/continued_fractions/basic.lean b/src/algebra/continued_fractions/basic.lean
index 0b583b592dc2a..df1cc8ef1bb94 100644
--- a/src/algebra/continued_fractions/basic.lean
+++ b/src/algebra/continued_fractions/basic.lean
@@ -198,7 +198,6 @@ instance : inhabited (scf α) := ⟨of_integer 1⟩
 instance has_coe_to_generalized_continued_fraction : has_coe (scf α) (gcf α) :=
 by {unfold scf, apply_instance}
 
-@[simp, norm_cast]
 lemma coe_to_generalized_continued_fraction {s : scf α} : (↑s : gcf α) = s.val := rfl
 
 end simple_continued_fraction
@@ -241,13 +240,11 @@ instance : inhabited (cf α) := ⟨of_integer 0⟩
 instance has_coe_to_simple_continued_fraction : has_coe (cf α) (scf α) :=
 by {unfold cf, apply_instance}
 
-@[simp, norm_cast]
 lemma coe_to_simple_continued_fraction {c : cf α} : (↑c : scf α) = c.val := rfl
 
 /-- Lift a cf to a scf using the inclusion map. -/
 instance has_coe_to_generalized_continued_fraction : has_coe (cf α) (gcf α) := ⟨λ c, ↑(↑c : scf α)⟩
 
-@[simp, norm_cast squash]
 lemma coe_to_generalized_continued_fraction {c : cf α} : (↑c : gcf α) = c.val := rfl
 
 end continued_fraction
diff --git a/src/algebra/module.lean b/src/algebra/module.lean
index 2eaf6dbe80e1d..9a710c5fbd0ca 100644
--- a/src/algebra/module.lean
+++ b/src/algebra/module.lean
@@ -486,10 +486,10 @@ instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
 instance : inhabited p := ⟨0⟩
 instance : has_scalar R p := ⟨λ c x, ⟨c • x.1, smul_mem _ c x.2⟩⟩
 
-@[simp] lemma mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext
+@[simp] lemma mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext_iff_val
 
 variables {p}
-@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : M) = y ↔ x = y := subtype.ext.symm
+@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : M) = y ↔ x = y := subtype.ext_iff_val.symm
 @[simp, norm_cast] lemma coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 := @coe_eq_coe _ _ _ _ _ _ x 0
 @[simp, norm_cast] lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : p) : M) = 0 := rfl
diff --git a/src/algebraic_geometry/prime_spectrum.lean b/src/algebraic_geometry/prime_spectrum.lean
index b4b5189c52c5c..d9d4a1fecb32d 100644
--- a/src/algebraic_geometry/prime_spectrum.lean
+++ b/src/algebraic_geometry/prime_spectrum.lean
@@ -68,7 +68,7 @@ instance as_ideal.is_prime (x : prime_spectrum R) :
 
 @[ext] lemma ext {x y : prime_spectrum R} :
   x = y ↔ x.as_ideal = y.as_ideal :=
-subtype.ext
+subtype.ext_iff_val
 
 /-- The zero locus of a set `s` of elements of a commutative ring `R`
 is the set of all prime ideals of the ring that contain the set `s`.
diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
index 3c2b4fd64bbcf..9f0a2852094b4 100644
--- a/src/analysis/analytic/basic.lean
+++ b/src/analysis/analytic/basic.lean
@@ -524,7 +524,7 @@ begin
       = ∑ s : finset (fin n), nnnorm (p n) * ((nnnorm x) ^ (n - s.card) * r ^ s.card) :
         by simp [← mul_assoc]
       ... = nnnorm (p n) * (nnnorm x + r) ^ n :
-      by { rw [add_comm, ← finset.mul_sum, ← fin.sum_pow_mul_eq_add_pow], congr, ext s, ring }
+      by { rw [add_comm, ← finset.mul_sum, ← fin.sum_pow_mul_eq_add_pow], congr, ext1 s, ring }
     end
   ... ≤ (∑' (n : ℕ), (C * a ^ n : ennreal)) :
     tsum_le_tsum (λ n, by exact_mod_cast hC n) ennreal.summable ennreal.summable
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
index d007a9302939c..c76908cc8ee88 100644
--- a/src/analysis/convex/basic.lean
+++ b/src/analysis/convex/basic.lean
@@ -917,7 +917,7 @@ lemma set.finite.convex_hull_eq_image {s : set E} (hs : finite s) :
 begin
   rw [← convex_hull_basis_eq_std_simplex, ← linear_map.convex_hull_image, ← range_comp, (∘)],
   apply congr_arg,
-  convert (subtype.range_val s).symm,
+  convert subtype.range_coe.symm,
   ext x,
   simp [linear_map.sum_apply, ite_smul, finset.filter_eq]
 end
diff --git a/src/analysis/normed_space/multilinear.lean b/src/analysis/normed_space/multilinear.lean
index 61bcb5b13fbce..1970930d3b4c5 100644
--- a/src/analysis/normed_space/multilinear.lean
+++ b/src/analysis/normed_space/multilinear.lean
@@ -275,7 +275,7 @@ calc ∥f.restr s hk z v∥
         refine ⟨j.1, j.2, _⟩,
         unfold_coes,
         convert hj.symm,
-        rw subtype.ext } }
+        rw subtype.ext_iff_val } }
   end
 ... = C * ∥z∥ ^ (n - k) * ∏ i, ∥v i∥ : by rw mul_assoc
 
diff --git a/src/analysis/special_functions/exp_log.lean b/src/analysis/special_functions/exp_log.lean
index 759e7ad45b4b4..ad4f56c6f5383 100644
--- a/src/analysis/special_functions/exp_log.lean
+++ b/src/analysis/special_functions/exp_log.lean
@@ -309,9 +309,9 @@ begin
     have : f₁ = λ h:{h:ℝ // 0 < h}, log x.1 + log h.1,
       ext h, rw ← log_mul (ne_of_gt x.2) (ne_of_gt h.2),
     simp only [this, log_mul (ne_of_gt x.2) one_ne_zero, log_one],
-    exact tendsto_const_nhds.add (tendsto.comp tendsto_log_one_zero continuous_at_subtype_val),
+    exact tendsto_const_nhds.add (tendsto.comp tendsto_log_one_zero continuous_at_subtype_coe),
   have H2 : tendsto f₂ (𝓝 x) (𝓝 ⟨x.1⁻¹ * x.1, mul_pos (inv_pos.2 x.2) x.2⟩),
-    rw tendsto_subtype_rng, exact tendsto_const_nhds.mul continuous_at_subtype_val,
+    rw tendsto_subtype_rng, exact tendsto_const_nhds.mul continuous_at_subtype_coe,
   suffices h : tendsto (f₁ ∘ f₂) (𝓝 x) (𝓝 (log x.1)),
   begin
     convert h, ext y,
diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean
index 0c5d03c36ecd2..f523eb18d6da0 100644
--- a/src/analysis/special_functions/pow.lean
+++ b/src/analysis/special_functions/pow.lean
@@ -843,7 +843,7 @@ lemma continuous_at_rpow {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) :
 begin
   have : (λp:ℝ≥0×ℝ, p.1^p.2) = nnreal.of_real ∘ (λp:ℝ×ℝ, p.1^p.2) ∘ (λp:ℝ≥0 × ℝ, (p.1.1, p.2)),
   { ext p,
-    rw [← nnreal.coe_eq, coe_rpow, nnreal.coe_of_real _ (real.rpow_nonneg_of_nonneg p.1.2 _)],
+    rw [coe_rpow, nnreal.coe_of_real _ (real.rpow_nonneg_of_nonneg p.1.2 _)],
     refl },
   rw this,
   refine nnreal.continuous_of_real.continuous_at.comp (continuous_at.comp _ _),
diff --git a/src/category_theory/elements.lean b/src/category_theory/elements.lean
index 987d2a989dc54..b225ea52bebad 100644
--- a/src/category_theory/elements.lean
+++ b/src/category_theory/elements.lean
@@ -52,7 +52,7 @@ namespace category_of_elements
 
 @[ext]
 lemma ext (F : C ⥤ Type w) {x y : F.elements} (f g : x ⟶ y) (w : f.val = g.val) : f = g :=
-subtype.eq' w
+subtype.ext_val w
 
 @[simp] lemma comp_val {F : C ⥤ Type w} {p q r : F.elements} {f : p ⟶ q} {g : q ⟶ r} :
   (f ≫ g).val = f.val ≫ g.val := rfl
diff --git a/src/category_theory/limits/types.lean b/src/category_theory/limits/types.lean
index 7d03057dbdfe2..092b13713d58c 100644
--- a/src/category_theory/limits/types.lean
+++ b/src/category_theory/limits/types.lean
@@ -23,11 +23,7 @@ local attribute [elab_simple] congr_fun
 /-- (internal implementation) the fact that the proposed limit cone is the limit -/
 def limit_is_limit_ (F : J ⥤ Type u) : is_limit (limit_ F) :=
 { lift := λ s v, ⟨λ j, s.π.app j v, λ j j' f, congr_fun (cone.w s f) _⟩,
-  uniq' :=
-  begin
-    intros, ext x, apply subtype.eq, ext j,
-    exact congr_fun (w j) x
-  end }
+  uniq' := by { intros, ext x j, exact congr_fun (w j) x } }
 
 instance : has_limits.{u} (Type u) :=
 { has_limits_of_shape := λ J 𝒥,
@@ -43,7 +39,7 @@ instance : has_limits.{u} (Type u) :=
 @[simp] lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟶ G) (g : limit F) :
   (lim.map α : limit F → limit G) g =
   (⟨λ j, (α.app j) (g.val j), λ j j' f,
-    by {rw ←functor_to_types.naturality, dsimp, rw ←(g.property f)}⟩ : limit G) := rfl
+    by {rw ←functor_to_types.naturality, dsimp, rw ←(g.prop f)}⟩ : limit G) := rfl
 
 @[simp] lemma types_limit_lift (F : J ⥤ Type u) (c : cone F) (x : c.X) :
   limit.lift F c x = (⟨λ j, c.π.app j x, λ j j' f, congr_fun (cone.w c f) x⟩ : limit F) :=
diff --git a/src/computability/tm_to_partrec.lean b/src/computability/tm_to_partrec.lean
index 5657d261a0bd8..9c6240fb268a4 100644
--- a/src/computability/tm_to_partrec.lean
+++ b/src/computability/tm_to_partrec.lean
@@ -188,12 +188,13 @@ begin
   suffices : ∃ c : code, ∀ v : vector ℕ m,
     c.eval v.1 = subtype.val <$> vector.m_of_fn (λ i, g i v),
   { obtain ⟨cf, hf⟩ := hf, obtain ⟨cg, hg⟩ := this,
-    exact ⟨cf.comp cg, λ v, by simp [hg, hf, map_bind, seq_bind_eq, (∘)]; refl⟩ },
+    exact ⟨cf.comp cg, λ v,
+      by { simp [hg, hf, map_bind, seq_bind_eq, (∘), -subtype.val_eq_coe], refl }⟩ },
   clear hf f, induction n with n IH,
   { exact ⟨nil, λ v, by simp [vector.m_of_fn]; refl⟩ },
   { obtain ⟨cg, hg₁⟩ := hg 0, obtain ⟨cl, hl⟩ := IH (λ i, hg i.succ),
-    exact ⟨cons cg cl, λ v, by simp [vector.m_of_fn, hg₁, map_bind,
-      seq_bind_eq, bind_assoc, (∘), hl]; refl⟩ },
+    exact ⟨cons cg cl, λ v, by { simp [vector.m_of_fn, hg₁, map_bind,
+      seq_bind_eq, bind_assoc, (∘), hl, -subtype.val_eq_coe], refl }⟩ },
 end
 
 theorem exists_code {n} {f : vector ℕ n →. ℕ} (hf : nat.partrec' f) :
@@ -220,7 +221,7 @@ begin
       vector.cons_tail, vector.cons_head, pfun.coe_val, vector.tail_val],
     simp only [← roption.pure_eq_some] at hf hg ⊢,
     induction v.head with n IH; simp [prec, hf, bind_assoc, ← roption.map_eq_map,
-      ← bind_pure_comp_eq_map, show ∀ x, pure x = [x], from λ _, rfl],
+      ← bind_pure_comp_eq_map, show ∀ x, pure x = [x], from λ _, rfl, -subtype.val_eq_coe],
     suffices : ∀ a b, a + b = n →
       (n.succ :: 0 :: g (n :: nat.elim (f v.tail) (λ y IH, g (y::IH::v.tail)) n :: v.tail)
          :: v.val.tail : list ℕ) ∈
@@ -269,13 +270,13 @@ begin
         subst this, exact ⟨_, ⟨h, hm⟩, rfl⟩ },
       { simp only [list.head, exists_eq_left, roption.mem_some_iff,
           list.tail_cons, false_or] at this,
-        refine IH _ this (by simp [hf, h]) _ rfl (λ m h', _),
+        refine IH _ this (by simp [hf, h, -subtype.val_eq_coe]) _ rfl (λ m h', _),
         obtain h|rfl := nat.lt_succ_iff_lt_or_eq.1 h', exacts [hm _ h, h] } },
     { rintro ⟨n, ⟨hn, hm⟩, rfl⟩, refine ⟨n.succ :: v.1, _, rfl⟩,
       have : (n.succ :: v.1 : list ℕ) ∈ pfun.fix
         (λ v, (cf.eval v).bind $ λ y, roption.some $ if y.head = 0 then
           sum.inl (v.head.succ :: v.tail) else sum.inr (v.head.succ :: v.tail)) (n :: v.val) :=
-        pfun.mem_fix_iff.2 (or.inl (by simp [hf, hn])),
+        pfun.mem_fix_iff.2 (or.inl (by simp [hf, hn, -subtype.val_eq_coe])),
       generalize_hyp : (n.succ :: v.1 : list ℕ) = w at this ⊢, clear hn,
       induction n with n IH, {exact this},
       refine IH (λ m h', hm (nat.lt_succ_of_lt h')) (pfun.mem_fix_iff.2 (or.inr ⟨_, _, this⟩)),
diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index 69aca8d95833e..df9a254aa8d14 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -198,17 +198,17 @@ ext $ λ i, by simp only [add_apply, filter_apply]; split_ifs; simp only [add_ze
 /-- `subtype_domain p f` is the restriction of the finitely supported function
   `f` to the subtype `p`. -/
 def subtype_domain [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p]
-  (f : Π₀ i, β i) : Π₀ i : subtype p, β i.1 :=
+  (f : Π₀ i, β i) : Π₀ i : subtype p, β i :=
 begin
   fapply quotient.lift_on f,
   { intro x,
-    refine ⟦⟨λ i, x.1 i.1,
-      (x.2.filter p).attach.map $ λ j, ⟨j.1, (multiset.mem_filter.1 j.2).2⟩, _⟩⟧,
-    refine λ i, or.cases_on (x.3 i.1) (λ H, _) or.inr,
-    left, rw multiset.mem_map, refine ⟨⟨i.1, multiset.mem_filter.2 ⟨H, i.2⟩⟩, _, subtype.eta _ _⟩,
+    refine ⟦⟨λ i, x.1 (i : ι),
+      (x.2.filter p).attach.map $ λ j, ⟨j, (multiset.mem_filter.1 j.2).2⟩, _⟩⟧,
+    refine λ i, or.cases_on (x.3 i) (λ H, _) or.inr,
+    left, rw multiset.mem_map, refine ⟨⟨i, multiset.mem_filter.2 ⟨H, i.2⟩⟩, _, subtype.eta _ _⟩,
     apply multiset.mem_attach },
   intros x y H,
-  exact quotient.sound (λ i, H i.1)
+  exact quotient.sound (λ i, H i)
 end
 
 @[simp] lemma subtype_domain_zero [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p] :
@@ -260,11 +260,11 @@ include dec
 
 /-- Create an element of `Π₀ i, β i` from a finset `s` and a function `x`
 defined on this `finset`. -/
-def mk (s : finset ι) (x : Π i : (↑s : set ι), β i.1) : Π₀ i, β i :=
+def mk (s : finset ι) (x : Π i : (↑s : set ι), β (i : ι)) : Π₀ i, β i :=
 ⟦⟨λ i, if H : i ∈ s then x ⟨i, H⟩ else 0, s.1,
 λ i, if H : i ∈ s then or.inl H else or.inr $ dif_neg H⟩⟧
 
-@[simp] lemma mk_apply {s : finset ι} {x : Π i : (↑s : set ι), β i.1} {i : ι} :
+@[simp] lemma mk_apply {s : finset ι} {x : Π i : (↑s : set ι), β i} {i : ι} :
   (mk s x : Π i, β i) i = if H : i ∈ s then x ⟨i, H⟩ else 0 :=
 rfl
 
@@ -282,7 +282,7 @@ end
 /-- The function `single i b : Π₀ i, β i` sends `i` to `b`
 and all other points to `0`. -/
 def single (i : ι) (b : β i) : Π₀ i, β i :=
-mk {i} $ λ j, eq.rec_on (finset.mem_singleton.1 j.2).symm b
+mk {i} $ λ j, eq.rec_on (finset.mem_singleton.1 j.prop).symm b
 
 @[simp] lemma single_apply {i i' b} :
   (single i b : Π₀ i, β i) i' = (if h : i = i' then eq.rec_on h b else 0) :=
@@ -290,7 +290,7 @@ begin
   dsimp only [single],
   by_cases h : i = i',
   { have h1 : i' ∈ ({i} : finset ι) := finset.mem_singleton.2 h.symm,
-    simp only [mk_apply, dif_pos h, dif_pos h1] },
+    simp only [mk_apply, dif_pos h, dif_pos h1], refl },
   { have h1 : i' ∉ ({i} : finset ι) := finset.not_mem_singleton.2 (ne.symm h),
     simp only [mk_apply, dif_neg h, dif_neg h1] }
 end
@@ -404,7 +404,7 @@ eq.rec_on h4 $ ha i b f h1 h2 h3
 
 end add_monoid
 
-@[simp] lemma mk_add [Π i, add_monoid (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i.1} :
+@[simp] lemma mk_add [Π i, add_monoid (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i} :
   mk s (x + y) = mk s x + mk s y :=
 ext $ λ i, by simp only [add_apply, mk_apply]; split_ifs; [refl, rw zero_add]
 
@@ -787,10 +787,10 @@ end
 @[to_additive]
 lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)]
   [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p]
-  {h : Π i, β i → γ} (hp : ∀x∈v.support, p x) :
+  {h : Π i, β i → γ} (hp : ∀ x ∈ v.support, p x) :
   (v.subtype_domain p).prod (λi b, h i.1 b) = v.prod h :=
 finset.prod_bij (λp _, p.val)
-  (by simp)
+  (by { dsimp, simp })
   (by simp)
   (assume ⟨a₀, ha₀⟩ ⟨a₁, ha₁⟩, by simp)
   (λ i hi, ⟨⟨i, hp i hi⟩, by simpa using hi, rfl⟩)
diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index 5ce6340040574..5a0ac8134b7b0 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -615,7 +615,7 @@ def subtype_preimage :
   left_inv := λ ⟨x, hx⟩, subtype.val_injective $ funext $ λ a,
     (by { dsimp, split_ifs; [ rw ← hx, skip ]; refl }),
   right_inv := λ x, funext $ λ ⟨a, h⟩,
-    show dite (p a) _ _ = _, by { dsimp, rw [dif_neg h], refl } }
+    show dite (p a) _ _ = _, by { dsimp, rw [dif_neg h] } }
 
 @[simp] lemma subtype_preimage_apply (x : {x : α → β // x ∘ coe = x₀}) :
   subtype_preimage p x₀ x = λ a, (x : α → β) a := rfl
@@ -826,8 +826,8 @@ def subtype_congr {p : α → Prop} {q : β → Prop}
   (e : α ≃ β) (h : ∀ a, p a ↔ q (e a)) : {a : α // p a} ≃ {b : β // q b} :=
 ⟨λ x, ⟨e x.1, (h _).1 x.2⟩,
  λ y, ⟨e.symm y.1, (h _).2 (by { simp, exact y.2 })⟩,
- λ ⟨x, h⟩, subtype.eq' $ by simp,
- λ ⟨y, h⟩, subtype.eq' $ by simp⟩
+ λ ⟨x, h⟩, subtype.ext_val $ by simp,
+ λ ⟨y, h⟩, subtype.ext_val $ by simp⟩
 
 /-- If two predicates `p` and `q` are pointwise equivalent, then `{x // p x}` is equivalent to
 `{x // q x}`. -/
@@ -942,7 +942,7 @@ def subtype_pi_equiv_pi {α : Sort u} {β : α → Sort v} {p : Πa, β a → Pr
   {f : Πa, β a // ∀a, p a (f a) } ≃ Πa, { b : β a // p a b } :=
 ⟨λf a, ⟨f.1 a, f.2 a⟩, λf, ⟨λa, (f a).1, λa, (f a).2⟩,
   by { rintro ⟨f, h⟩, refl },
-  by { rintro f, funext a, exact subtype.eq' rfl }⟩
+  by { rintro f, funext a, exact subtype.ext_val rfl }⟩
 
 /-- A subtype of a product defined by componentwise conditions
 is equivalent to a product of subtypes. -/
@@ -1218,7 +1218,7 @@ def subtype_quotient_equiv_quotient_subtype (p₁ : α → Prop) [s₁ : setoid
     (λ a b hab, hfunext (by rw quotient.sound hab)
     (λ h₁ h₂ _, heq_of_eq (quotient.sound ((h _ _).2 hab)))) a.2,
   inv_fun := λ a, quotient.lift_on a (λ a, (⟨⟦a.1⟧, (hp₂ _).1 a.2⟩ : {x // p₂ x}))
-    (λ a b hab, subtype.eq' (quotient.sound ((h _ _).1 hab))),
+    (λ a b hab, subtype.ext_val (quotient.sound ((h _ _).1 hab))),
   left_inv := λ ⟨a, ha⟩, quotient.induction_on a (λ a ha, rfl) ha,
   right_inv := λ a, quotient.induction_on a (λ ⟨a, ha⟩, rfl) }
 
@@ -1526,7 +1526,7 @@ begin
   by_cases h : i ∈ s,
   { simp only [h, dif_pos],
     have A : e.symm ⟨i, h⟩ = j ↔ i = e j,
-      by { rw equiv.symm_apply_eq, exact subtype.ext },
+      by { rw equiv.symm_apply_eq, exact subtype.ext_iff_val },
     by_cases h' : i = e j,
     { rw [A.2 h', h'], simp },
     { have : ¬ e.symm ⟨i, h⟩ = j, by simpa [← A] using h',
diff --git a/src/data/equiv/denumerable.lean b/src/data/equiv/denumerable.lean
index cac3b0a0cfcdf..00124abc80d77 100644
--- a/src/data/equiv/denumerable.lean
+++ b/src/data/equiv/denumerable.lean
@@ -137,7 +137,7 @@ infinite.not_fintype
   ⟨(((multiset.range x.1.succ).filter (∈ s)).pmap
       (λ (y : ℕ) (hy : y ∈ s), subtype.mk y hy)
       (by simp [-multiset.range_succ])).to_finset,
-    by simpa [subtype.ext, multiset.mem_filter, -multiset.range_succ]⟩
+    by simpa [subtype.ext_iff_val, multiset.mem_filter, -multiset.range_succ]⟩
 
 end classical
 
@@ -179,7 +179,7 @@ lemma of_nat_surjective_aux : ∀ {x : ℕ} (hx : x ∈ s), ∃ n, of_nat s n =
 | x := λ hx, let t : list s := ((list.range x).filter (λ y, y ∈ s)).pmap
   (λ (y : ℕ) (hy : y ∈ s), ⟨y, hy⟩) (by simp) in
 have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩,
-  by simp [list.mem_filter, subtype.ext, t]; intros; refl,
+  by simp [list.mem_filter, subtype.ext_iff_val, t]; intros; refl,
 have wf : ∀ m : s, list.maximum t = m → m.1 < x,
   from λ m hmax, by simpa [hmt] using list.maximum_mem hmax,
 begin
diff --git a/src/data/finset.lean b/src/data/finset.lean
index 95f38e06ea364..a99eacc75affe 100644
--- a/src/data/finset.lean
+++ b/src/data/finset.lean
@@ -324,14 +324,16 @@ def subtype_insert_equiv_option {t : finset α} {x : α} (h : x ∉ t) :
   {i // i ∈ insert x t} ≃ option {i // i ∈ t} :=
 begin
   refine
-  { to_fun := λ y, if h : y.1 = x then none else some ⟨y, (finset.mem_insert.mp y.2).resolve_left h⟩,
-    inv_fun := λ y, y.elim ⟨x, finset.mem_insert_self _ _⟩ $ λ z, ⟨z.1, finset.mem_insert_of_mem z.2⟩,
+  { to_fun := λ y, if h : ↑y = x then none else some ⟨y, (finset.mem_insert.mp y.2).resolve_left h⟩,
+    inv_fun := λ y, y.elim ⟨x, finset.mem_insert_self _ _⟩ $ λ z, ⟨z, finset.mem_insert_of_mem z.2⟩,
     .. },
-  { intro y, by_cases h : y.1 = x, simp only [subtype.ext, h, option.elim, dif_pos],
-    simp only [h, option.elim, dif_neg, not_false_iff, subtype.coe_eta] },
-  { rintro (_|y), simp only [option.elim, dif_pos],
-    have : y.val ≠ x, { rintro ⟨⟩, exact h y.2 },
-    simp only [this, option.elim, subtype.eta, dif_neg, not_false_iff, subtype.coe_mk] },
+  { intro y, by_cases h : ↑y = x,
+    simp only [subtype.ext_iff, h, option.elim, dif_pos, subtype.coe_mk],
+    simp only [h, option.elim, dif_neg, not_false_iff, subtype.coe_eta, subtype.coe_mk] },
+  { rintro (_|y), simp only [option.elim, dif_pos, subtype.coe_mk],
+    have : ↑y ≠ x, { rintro ⟨⟩, exact h y.2 },
+    simp only [this, option.elim, subtype.eta, dif_neg, not_false_iff, subtype.coe_eta,
+      subtype.coe_mk] },
 end
 
 /-! ### union -/
@@ -1014,7 +1016,7 @@ variables {n m l : ℕ}
 /-- `range n` is the set of natural numbers less than `n`. -/
 def range (n : ℕ) : finset ℕ := ⟨_, nodup_range n⟩
 
-@[simp] theorem range_val (n : ℕ) : (range n).1 = multiset.range n := rfl
+@[simp] theorem range_coe (n : ℕ) : (range n).1 = multiset.range n := rfl
 
 @[simp] theorem mem_range : m ∈ range n ↔ m < n := mem_range
 
@@ -1064,7 +1066,7 @@ def not_mem_range_equiv (k : ℕ) : {n // n ∉ range k} ≃ ℕ :=
   left_inv :=
   begin
     assume j,
-    rw subtype.ext,
+    rw subtype.ext_iff_val,
     apply nat.sub_add_cancel,
     simpa using j.2
   end,
@@ -1571,10 +1573,10 @@ lemma surj_on_of_inj_on_of_card_le {s : finset α} {t : finset β}
   (∀ b ∈ t, ∃ a ha, b = f a ha) :=
 by haveI := classical.dec_eq β; exact
 λ b hb,
-  have h : card (image (λ (a : {a // a ∈ s}), f (a.val) a.2) (attach s)) = card s,
+  have h : card (image (λ (a : {a // a ∈ s}), f a a.prop) (attach s)) = card s,
     from @card_attach _ s ▸ card_image_of_injective _
       (λ ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ h, subtype.eq $ hinj _ _ _ _ h),
-  have h₁ : image (λ a : {a // a ∈ s}, f a.1 a.2) s.attach = t :=
+  have h₁ : image (λ a : {a // a ∈ s}, f a a.prop) s.attach = t :=
   eq_of_subset_of_card_le (λ b h, let ⟨a, ha₁, ha₂⟩ := mem_image.1 h in
     ha₂ ▸ hf _ _) (by simp [hst, h]),
 begin
@@ -1605,7 +1607,7 @@ have hsg : surjective g, from λ x,
 have hif : injective f',
   from (left_inverse_of_surjective_of_right_inverse hsg
       (right_inverse_surj_inv _)).injective,
-subtype.ext.1 (@hif ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ (subtype.eq ha₁a₂))
+subtype.ext_iff_val.1 (@hif ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ (subtype.eq ha₁a₂))
 
 end card
 
diff --git a/src/data/hash_map.lean b/src/data/hash_map.lean
index 11a252b8e6348..30dbebb0402a4 100644
--- a/src/data/hash_map.lean
+++ b/src/data/hash_map.lean
@@ -13,11 +13,11 @@ universes u v w
 /-- `bucket_array α β` is the underlying data type for `hash_map α β`,
   an array of linked lists of key-value pairs. -/
 def bucket_array (α : Type u) (β : α → Type v) (n : ℕ+) :=
-array n.1 (list Σ a, β a)
+array n (list Σ a, β a)
 
 /-- Make a hash_map index from a `nat` hash value and a (positive) buffer size -/
-def hash_map.mk_idx (n : ℕ+) (i : nat) : fin n.1 :=
-⟨i % n.1, nat.mod_lt _ n.2⟩
+def hash_map.mk_idx (n : ℕ+) (i : nat) : fin n :=
+⟨i % n, nat.mod_lt _ n.2⟩
 
 namespace bucket_array
 section
@@ -71,7 +71,7 @@ parameters {α : Type u} {β : α → Type v} (hash_fn : α → nat)
 def reinsert_aux {n} (data : bucket_array α β n) (a : α) (b : β a) : bucket_array α β n :=
 data.modify hash_fn a (λl, ⟨a, b⟩ :: l)
 
-theorem mk_as_list (n : ℕ+) : bucket_array.as_list (mk_array n.1 [] : bucket_array α β n) = [] :=
+theorem mk_as_list (n : ℕ+) : bucket_array.as_list (mk_array n [] : bucket_array α β n) = [] :=
 list.eq_nil_iff_forall_not_mem.mpr $ λ x m,
 let ⟨i, h⟩ := (bucket_array.mem_as_list _).1 m in h
 
@@ -161,7 +161,7 @@ begin
   apply ij, rwa [← v.idx_enum_1 _ me₁ ml₁, ← v.idx_enum_1 _ me₂ ml₂]
 end
 
-theorem mk_valid (n : ℕ+) : @valid n (mk_array n.1 []) 0 :=
+theorem mk_valid (n : ℕ+) : @valid n (mk_array n []) 0 :=
 ⟨by simp [mk_as_list], λ i a h, by cases h, λ i, list.nodup_nil⟩
 
 theorem valid.find_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) {a : α}
@@ -177,7 +177,7 @@ by simp [contains_aux, option.is_some_iff_exists, v.find_aux_iff hash_fn]
 
 section
   parameters {n : ℕ+} {bkts : bucket_array α β n}
-             {bidx : fin n.1} {f : list (Σ a, β a) → list (Σ a, β a)}
+             {bidx : fin n} {f : list (Σ a, β a) → list (Σ a, β a)}
              (u v1 v2 w : list Σ a, β a)
 
   local notation `L` := array.read bkts bidx
@@ -375,7 +375,7 @@ m.is_valid.contains_aux_iff _ _
 
 theorem entries_empty (hash_fn : α → nat) (n) :
   (@mk_hash_map α _ β hash_fn n).entries = [] :=
-by dsimp [entries, mk_hash_map]; rw mk_as_list
+mk_as_list _
 
 theorem keys_empty (hash_fn : α → nat) (n) :
   (@mk_hash_map α _ β hash_fn n).keys = [] :=
@@ -446,14 +446,14 @@ else
 let size'    := size + 1,
     buckets' := buckets.modify hash_fn a (λl, ⟨a, b⟩::l),
     valid'   := v.insert _ a b hc in
-if size' ≤ n.1 then
+if size' ≤ n then
 { hash_fn  := hash_fn,
   size     := size',
   nbuckets := n,
   buckets  := buckets',
   is_valid := valid' }
 else
-let n'        : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
+let n'        : ℕ+ := ⟨n * 2, mul_pos n.2 dec_trivial⟩,
     buckets'' : bucket_array α β n' :=
                 buckets'.foldl (mk_array _ []) (reinsert_aux hash_fn) in
 { hash_fn  := hash_fn,
@@ -501,20 +501,20 @@ theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
       let ⟨u, w, hl, hfl⟩ := append_of_modify [] [] [⟨a, b⟩] _ rfl rfl in
       lem bkts' _ u w hl hfl $ or.inl ⟨rfl, Hc⟩,
     simp [insert, @dif_neg (contains_aux a bkt) _ Hc],
-    by_cases h : size' ≤ n.1,
+    by_cases h : size' ≤ n,
     -- TODO(Mario): Why does the by_cases assumption look different than the stated one?
-    { simpa [show size' ≤ n.1, from h] using mi },
-    { let n' : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
+    { simpa [show size' ≤ n, from h] using mi },
+    { let n' : ℕ+ := ⟨n * 2, mul_pos n.2 dec_trivial⟩,
       let bkts'' : bucket_array α β n' := bkts'.foldl (mk_array _ []) (reinsert_aux hash_fn),
       suffices : sigma.mk a' b' ∈ bkts''.as_list ↔ sigma.mk a' b' ∈ bkts'.as_list.reverse,
-      { simpa [show ¬ size' ≤ n.1, from h, mi] },
+      { simpa [show ¬ size' ≤ n, from h, mi] },
       rw [show bkts'' = bkts'.as_list.foldl _ _, from bkts'.foldl_eq _ _,
           ← list.foldr_reverse],
       induction bkts'.as_list.reverse with a l IH,
       { simp [mk_as_list] },
       { cases a with a'' b'',
         let B := l.foldr (λ (y : sigma β) (x : bucket_array α β n'),
-          reinsert_aux hash_fn x y.1 y.2) (mk_array n'.1 []),
+          reinsert_aux hash_fn x y.1 y.2) (mk_array n' []),
         rcases append_of_modify [] [] [⟨a'', b''⟩] _ rfl rfl with ⟨u, w, hl, hfl⟩,
         simp [IH.symm, or.left_comm, show B.as_list = _, from hl,
               show (reinsert_aux hash_fn B a'' b'').as_list = _, from hfl] } } }
diff --git a/src/data/holor.lean b/src/data/holor.lean
index 1e6bd8ee4ccc0..52bd8f061c279 100644
--- a/src/data/holor.lean
+++ b/src/data/holor.lean
@@ -217,22 +217,18 @@ end
 /-- The original holor can be recovered from its slices by multiplying with unit vectors and summing up. -/
 @[simp] lemma sum_unit_vec_mul_slice [ring α] (x : holor α (d :: ds)) :
   ∑ i in (finset.range d).attach,
-    unit_vec d i.1 ⊗ slice x i.1 (nat.succ_le_of_lt (finset.mem_range.1 i.2)) = x :=
+    unit_vec d i ⊗ slice x i (nat.succ_le_of_lt (finset.mem_range.1 i.prop)) = x :=
 begin
   apply slice_eq _ _ _,
   ext i hid,
   rw [←slice_sum],
   simp only [slice_unit_vec_mul hid],
-  rw finset.sum_eq_single (subtype.mk i _),
-  { simp, refl },
+  rw finset.sum_eq_single (subtype.mk i $ finset.mem_range.2 hid),
+  { simp },
   { assume (b : {x // x ∈ finset.range d}) (hb : b ∈ (finset.range d).attach) (hbi : b ≠ ⟨i, _⟩),
-    have hbi' : i ≠ b.val,
-    { apply not.imp hbi,
-      { assume h0 : i = b.val,
-        apply subtype.eq,
-        simp only [h0] },
-      { exact finset.mem_range.2 hid } },
-    simp [hbi']},
+    have hbi' : i ≠ b,
+    { simpa only [ne.def, subtype.ext_iff, subtype.coe_mk] using hbi.symm },
+    simp [hbi'] },
   { assume hid' : subtype.mk i _ ∉ finset.attach (finset.range d),
     exfalso,
     exact absurd (finset.mem_attach _ _) hid'
diff --git a/src/data/list/range.lean b/src/data/list/range.lean
index b4d8704aa7f58..d1337de1c5980 100644
--- a/src/data/list/range.lean
+++ b/src/data/list/range.lean
@@ -198,7 +198,7 @@ option.some.inj $ by rw [← nth_le_nth _, nth_range (by simpa using H)]
 theorem of_fn_eq_pmap {α n} {f : fin n → α} :
   of_fn f = pmap (λ i hi, f ⟨i, hi⟩) (range n) (λ _, mem_range.1) :=
 by rw [pmap_eq_map_attach]; from ext_le (by simp)
-  (λ i hi1 hi2, by simp at hi1; simp [nth_le_of_fn f ⟨i, hi1⟩])
+  (λ i hi1 hi2, by { simp at hi1, simp [nth_le_of_fn f ⟨i, hi1⟩, -subtype.val_eq_coe] })
 
 theorem nodup_of_fn {α n} {f : fin n → α} (hf : function.injective f) :
   nodup (of_fn f) :=
diff --git a/src/data/padics/hensel.lean b/src/data/padics/hensel.lean
index 8054cc20a4f08..49738f346a470 100644
--- a/src/data/padics/hensel.lean
+++ b/src/data/padics/hensel.lean
@@ -159,15 +159,15 @@ private def calc_eval_z'  {z z' z1 : ℤ_[p]} (hz' : z' = z - z1) {n} (hz : ih n
 have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0, from
   have hdzne : F.derivative.eval z ≠ 0,
     from mt norm_eq_zero.2 (by rw hz.1; apply deriv_norm_ne_zero; assumption),
-  λ h, hdzne $ subtype.ext.2 h,
+  λ h, hdzne $ subtype.ext_iff_val.2 h,
 let ⟨q, hq⟩ := F.binom_expansion z (-z1) in
 have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])∥ ≤ 1,
   by {rw padic_norm_e.mul, apply mul_le_one, apply padic_norm_z.le_one, apply norm_nonneg, apply h1},
 have F.derivative.eval z * (-z1) = -F.eval z, from calc
   F.derivative.eval z * (-z1)
     = (F.derivative.eval z) * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ : by rw [hzeq]
-... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp [subtype.coe_ext]
-... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) : subtype.ext.2 $ by simp
+... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp [subtype.ext_iff_val]
+... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) : subtype.ext_iff_val.2 $ by simp
 ... = -(F.eval z) : by simp [mul_div_cancel' _ hdzne'],
 have heq : F.eval z' = q * z1^2, by simpa [this, hz'] using hq,
 ⟨q, heq⟩
diff --git a/src/data/padics/padic_integers.lean b/src/data/padics/padic_integers.lean
index e631027051be5..e8ef481567fae 100644
--- a/src/data/padics/padic_integers.lean
+++ b/src/data/padics/padic_integers.lean
@@ -51,7 +51,7 @@ variables {p : ℕ} [fact p.prime]
 
 instance : has_coe ℤ_[p] ℚ_[p] := ⟨subtype.val⟩
 
-@[ext] lemma ext {x y : ℤ_[p]} : (x : ℚ_[p]) = y → x = y := subtype.ext.2
+@[ext] lemma ext {x y : ℤ_[p]} : (x : ℚ_[p]) = y → x = y := subtype.ext_iff_val.2
 
 /-- Addition on ℤ_p is inherited from ℚ_p. -/
 instance : has_add ℤ_[p] :=
@@ -153,12 +153,12 @@ instance : comm_ring ℤ_[p] :=
   ..padic_int.ring }
 
 protected lemma padic_int.zero_ne_one : (0 : ℤ_[p]) ≠ 1 :=
-show (⟨(0 : ℚ_[p]), _⟩ : ℤ_[p]) ≠ ⟨(1 : ℚ_[p]), _⟩, from mt subtype.ext.1 zero_ne_one
+show (⟨(0 : ℚ_[p]), _⟩ : ℤ_[p]) ≠ ⟨(1 : ℚ_[p]), _⟩, from mt subtype.ext_iff_val.1 zero_ne_one
 
 protected lemma padic_int.eq_zero_or_eq_zero_of_mul_eq_zero :
           ∀ (a b : ℤ_[p]), a * b = 0 → a = 0 ∨ b = 0
 | ⟨a, ha⟩ ⟨b, hb⟩ := λ h : (⟨a * b, _⟩ : ℤ_[p]) = ⟨0, _⟩,
-have a * b = 0, from subtype.ext.1 h,
+have a * b = 0, from subtype.ext_iff_val.1 h,
 (mul_eq_zero.1 this).elim
   (λ h1, or.inl (by simp [h1]; refl))
   (λ h2, or.inr (by simp [h2]; refl))
@@ -236,7 +236,7 @@ lemma mul_inv : ∀ {z : ℤ_[p]}, ∥z∥ = 1 → z * z.inv = 1
     unfold padic_int.inv, split_ifs,
     { change (⟨k * (1/k), _⟩ : ℤ_[p]) = 1,
       simp [hk], refl },
-    { apply subtype.ext.2, simp [mul_inv_cancel hk] }
+    { apply subtype.ext_iff_val.2, simp [mul_inv_cancel hk] }
   end
 
 lemma inv_mul {z : ℤ_[p]} (hz : ∥z∥ = 1) : z.inv * z = 1 :=
diff --git a/src/data/polynomial.lean b/src/data/polynomial.lean
index 0f5da0b570a97..9936fe60789ae 100644
--- a/src/data/polynomial.lean
+++ b/src/data/polynomial.lean
@@ -2719,7 +2719,7 @@ begin
   rw finsupp.sum_mul,
   delta finsupp.sum,
   congr, ext i r, dsimp,
-  rw [mul_assoc, ←(pow_sub_pow_factor x y _).property, mul_sub],
+  rw [mul_assoc, ←(pow_sub_pow_factor x y _).prop, mul_sub],
 end
 
 end identities
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
index bc3dcdeea2188..ba6e82325f706 100644
--- a/src/data/real/nnreal.lean
+++ b/src/data/real/nnreal.lean
@@ -59,7 +59,7 @@ instance : has_bot ℝ≥0   := ⟨0⟩
 instance : inhabited ℝ≥0 := ⟨0⟩
 
 @[simp, norm_cast] protected lemma coe_eq {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂ :=
-subtype.ext.symm
+subtype.ext_iff_val.symm
 @[simp, norm_cast] protected lemma coe_zero : ((0 : ℝ≥0) : ℝ) = 0 := rfl
 @[simp, norm_cast] protected lemma coe_one  : ((1 : ℝ≥0) : ℝ) = 1 := rfl
 @[simp, norm_cast] protected lemma coe_add (r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂ := rfl
diff --git a/src/data/seq/wseq.lean b/src/data/seq/wseq.lean
index 37a19a3673528..b0c0fd63a5f83 100644
--- a/src/data/seq/wseq.lean
+++ b/src/data/seq/wseq.lean
@@ -555,8 +555,8 @@ by { simp [think, join], unfold functor.map, simp [join, cons, append] }
 theorem destruct_tail (s : wseq α) :
   destruct (tail s) = destruct s >>= tail.aux :=
 begin
-  dsimp [tail], simp, rw [← bind_pure_comp_eq_map, is_lawful_monad.bind_assoc],
-  apply congr_arg, ext (_|⟨a, s⟩);
+  simp [tail], rw [← bind_pure_comp_eq_map, is_lawful_monad.bind_assoc],
+  apply congr_arg, ext1 (_|⟨a, s⟩);
   apply (@pure_bind computation _ _ _ _ _ _).trans _; simp
 end
 
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 41477d1911524..a7f8c46783a9a 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -22,7 +22,7 @@ library, as well as extra lemmas for functions in the core library (empty set, u
 intersection, insert, singleton, set-theoretic difference, complement, and powerset).
 
 Note that a set is a term, not a type. There is a coersion from `set α` to `Type*` sending
-`s` to the corresponding subtype `↑s`.
+`s` to the corresponding subtype `↥s`.
 
 See also the file `set_theory/zfc.lean`, which contains an encoding of ZFC set theory in Lean.
 
@@ -62,9 +62,11 @@ Definitions in the file:
 
 ## Implementation notes
 
-`s.nonempty` is to be preferred to `s ≠ ∅` or `∃ x, x ∈ s`. It has the advantage that
+* `s.nonempty` is to be preferred to `s ≠ ∅` or `∃ x, x ∈ s`. It has the advantage that
 the `s.nonempty` dot notation can be used.
 
+* For `s : set α`, do not use `subtype s`. Instead use `↥s` or `(s : Type*)` or `s`.
+
 ## Tags
 
 set, sets, subset, subsets, image, preimage, pre-image, range, union, intersection, insert,
@@ -116,7 +118,8 @@ iff.intro set_coe.ext (assume h, h ▸ rfl)
 
 end set_coe
 
-lemma subtype.mem {α : Type*} {s : set α} (p : s) : (p : α) ∈ s := p.property
+/-- See also `subtype.prop` -/
+lemma subtype.mem {α : Type*} {s : set α} (p : s) : (p : α) ∈ s := p.prop
 
 namespace set
 
@@ -141,6 +144,8 @@ theorem nmem_set_of_eq {a : α} {P : α → Prop} : a ∉ {a : α | P a} = ¬ P
 
 @[simp] theorem set_of_mem_eq {s : set α} : {x | x ∈ s} = s := rfl
 
+theorem set_of_set {s : set α} : set_of s = s := rfl
+
 lemma set_of_app_iff {p : α → Prop} {x : α} : { x | p x } x ↔ p x := iff.rfl
 
 theorem mem_def {a : α} {s : set α} : a ∈ s ↔ s a := iff.rfl
@@ -667,7 +672,7 @@ instance unique_singleton (a : α) : unique ↥({a} : set α) :=
   uniq :=
   begin
     intros x,
-    apply subtype.coe_ext.2,
+    apply subtype.ext,
     apply eq_of_mem_singleton (subtype.mem x),
   end}
 
@@ -1572,68 +1577,74 @@ namespace subtype
 
 variable {α : Type*}
 
-lemma val_image {p : α → Prop} {s : set (subtype p)} :
-  subtype.val '' s = {x | ∃h : p x, (⟨x, h⟩ : subtype p) ∈ s} :=
+lemma coe_image {p : α → Prop} {s : set (subtype p)} :
+  coe '' s = {x | ∃h : p x, (⟨x, h⟩ : subtype p) ∈ s} :=
 set.ext $ assume a,
 ⟨assume ⟨⟨a', ha'⟩, in_s, h_eq⟩, h_eq ▸ ⟨ha', in_s⟩,
   assume ⟨ha, in_s⟩, ⟨⟨a, ha⟩, in_s, rfl⟩⟩
 
-@[simp] lemma val_range {p : α → Prop} :
-  set.range (@subtype.val _ p) = {x | p x} :=
-by rw ← set.image_univ; simp [-set.image_univ, val_image]
-
-lemma range_val (s : set α) : range (subtype.val : s → α) = s :=
-val_range
-
-theorem val_image_subset (s : set α) (t : set (subtype s)) : t.image val ⊆ s :=
+lemma range_coe {s : set α} :
+  range (coe : s → α) = s :=
+by { rw ← set.image_univ, simp [-set.image_univ, coe_image] }
+
+/-- A variant of `range_coe`. Try to use `range_coe` if possible.
+  This version is useful when defining a new type that is defined as the subtype of something.
+  In that case, the coercion doesn't fire anymore. -/
+lemma range_val {s : set α} :
+  range (subtype.val : s → α) = s :=
+range_coe
+
+/-- We make this the simp lemma instead of `range_coe`. The reason is that if we write
+  for `s : set α` the function `coe : s → α`, then the inferred implicit arguments of `coe` are
+  `coe α (λ x, x ∈ s)`. -/
+@[simp] lemma range_coe_subtype {p : α → Prop} :
+  range (coe : subtype p → α) = {x | p x} :=
+range_coe
+
+lemma range_val_subtype {p : α → Prop} :
+  range (subtype.val : subtype p → α) = {x | p x} :=
+range_coe
+
+theorem coe_image_subset (s : set α) (t : set s) : t.image coe ⊆ s :=
 λ x ⟨y, yt, yvaleq⟩, by rw ←yvaleq; exact y.property
 
-theorem val_image_univ (s : set α) : @val _ s '' set.univ = s :=
-image_univ.trans (range_val s)
-
-@[simp] theorem image_preimage_val (s t : set α) :
-  (@subtype.val _ s) '' ((@subtype.val _ s) ⁻¹' t) = t ∩ s :=
-image_preimage_eq_inter_range.trans $ congr_arg _ (range_val s)
+theorem coe_image_univ (s : set α) : (coe : s → α) '' set.univ = s :=
+image_univ.trans range_coe
 
 @[simp] theorem image_preimage_coe (s t : set α) :
   (coe : s → α) '' (coe ⁻¹' t) = t ∩ s :=
-image_preimage_val s t
+image_preimage_eq_inter_range.trans $ congr_arg _ range_coe
 
-theorem preimage_val_eq_preimage_val_iff (s t u : set α) :
-  ((@subtype.val _ s) ⁻¹' t = (@subtype.val _ s) ⁻¹' u) ↔ (t ∩ s = u ∩ s) :=
+theorem image_preimage_val (s t : set α) :
+  (subtype.val : s → α) '' (subtype.val ⁻¹' t) = t ∩ s :=
+image_preimage_coe s t
+
+theorem preimage_coe_eq_preimage_coe_iff {s t u : set α} :
+  ((coe : s → α) ⁻¹' t = coe ⁻¹' u) ↔ t ∩ s = u ∩ s :=
 begin
-  rw [←image_preimage_val, ←image_preimage_val],
+  rw [←image_preimage_coe, ←image_preimage_coe],
   split, { intro h, rw h },
-  intro h, exact val_injective.image_injective h
+  intro h, exact coe_injective.image_injective h
 end
 
+theorem preimage_val_eq_preimage_val_iff (s t u : set α) :
+  ((subtype.val : s → α) ⁻¹' t = subtype.val ⁻¹' u) ↔ (t ∩ s = u ∩ s) :=
+preimage_coe_eq_preimage_coe_iff
+
 lemma exists_set_subtype {t : set α} (p : set α → Prop) :
-  (∃(s : set t), p (subtype.val '' s)) ↔ ∃(s : set α), s ⊆ t ∧ p s :=
+  (∃(s : set t), p (coe '' s)) ↔ ∃(s : set α), s ⊆ t ∧ p s :=
 begin
   split,
-  { rintro ⟨s, hs⟩, refine ⟨subtype.val '' s, _, hs⟩,
-    convert image_subset_range _ _, rw [range_val] },
-  rintro ⟨s, hs₁, hs₂⟩, refine ⟨subtype.val ⁻¹' s, _⟩,
-  rw [image_preimage_eq_of_subset], exact hs₂, rw [range_val], exact hs₁
+  { rintro ⟨s, hs⟩, refine ⟨coe '' s, _, hs⟩,
+    convert image_subset_range _ _, rw [range_coe] },
+  rintro ⟨s, hs₁, hs₂⟩, refine ⟨coe ⁻¹' s, _⟩,
+  rw [image_preimage_eq_of_subset], exact hs₂, rw [range_coe], exact hs₁
 end
 
 end subtype
 
 namespace set
 
-section range
-
-variable {α : Type*}
-
-@[simp] lemma range_coe_subtype (s : set α) : range (coe : s → α) = s :=
-subtype.val_range
-
-theorem preimage_coe_eq_preimage_coe_iff {s t u : set α} :
-  ((coe : s → α) ⁻¹' t = coe ⁻¹' u) ↔ t ∩ s = u ∩ s :=
-subtype.preimage_val_eq_preimage_val_iff _ _ _
-
-end range
-
 /-! ### Lemmas about cartesian product of sets -/
 
 section prod
@@ -1848,7 +1859,7 @@ by cases x; refl
 
 lemma inclusion_injective {s t : set α} (h : s ⊆ t) :
   function.injective (inclusion h)
-| ⟨_, _⟩ ⟨_, _⟩ := subtype.ext.2 ∘ subtype.ext.1
+| ⟨_, _⟩ ⟨_, _⟩ := subtype.ext_iff_val.2 ∘ subtype.ext_iff_val.1
 
 lemma range_inclusion {s t : set α} (h : s ⊆ t) : range (inclusion h) = {x : t | (x:α) ∈ s} :=
 ext $ λ ⟨x, hx⟩ , by simp [inclusion]
diff --git a/src/data/set/countable.lean b/src/data/set/countable.lean
index 57d527c89a535..51cbd298c7757 100644
--- a/src/data/set/countable.lean
+++ b/src/data/set/countable.lean
@@ -89,7 +89,7 @@ begin
   have : range g = univ := univ_subset_iff.1 hg,
   use coe ∘ g,
   rw [range_comp, this],
-  simp
+  simp only [image_univ, subtype.range_coe, mem_def]
 end
 
 @[simp] lemma countable_empty : countable (∅ : set α) :=
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index e98ed6c70fcb0..8a3cf59f9f42d 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -249,7 +249,7 @@ 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⟩) $
-  assume a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext.1 eq⟩
+  assume a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext_iff_val.1 eq⟩
 
 theorem finite_image_iff {s : set α} {f : α → β} (hi : inj_on f s) :
   finite (f '' s) ↔ finite s :=
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
index 4925ea70c3e37..36ea1024b6856 100644
--- a/src/data/set/function.lean
+++ b/src/data/set/function.lean
@@ -1,4 +1,4 @@
-/-
+  /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu, Yury Kudryashov
@@ -49,7 +49,7 @@ lemma restrict_eq (f : α → β) (s : set α) : s.restrict f = f ∘ coe := rfl
 @[simp] lemma restrict_apply (f : α → β) (s : set α) (x : s) : restrict f s x = f x := rfl
 
 @[simp] lemma range_restrict (f : α → β) (s : set α) : set.range (restrict f s) = f '' s :=
-range_comp.trans $ congr_arg (('') f) s.range_coe_subtype
+range_comp.trans $ congr_arg (('') f) subtype.range_coe
 
 /-- Restrict codomain of a function `f` to a set `s`. Same as `subtype.coind` but this version
 has codomain `↥s` instead of `subtype s`. -/
@@ -129,7 +129,7 @@ theorem maps_to.iterate_restrict {f : α → α} {s : set α} (h : maps_to f s s
   (h.restrict f s s^[n]) = (h.iterate n).restrict _ _ _ :=
 begin
   funext x,
-  rw [subtype.coe_ext, maps_to.coe_restrict_apply],
+  rw [subtype.ext_iff, maps_to.coe_restrict_apply],
   induction n with n ihn generalizing x,
   { refl },
   { simp [nat.iterate, ihn] }
diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index b1fe8a3ee60e1..2234a0182c14f 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -527,10 +527,10 @@ lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h :
 by rw [← sInter_image, image_id']
 
 lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i) :=
-by rw [← sUnion_range, range_coe_subtype]
+by simp only [←sUnion_range, subtype.range_coe, mem_def]
 
 lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i) :=
-by rw [← sInter_range, range_coe_subtype]
+by simp only [←sInter_range, subtype.range_coe, mem_def]
 
 lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
 set.ext $ λ x, by simp [bool.exists_bool, or_comm]
diff --git a/src/data/setoid/basic.lean b/src/data/setoid/basic.lean
index e940c1e58a2e2..8e07d6a3a7442 100644
--- a/src/data/setoid/basic.lean
+++ b/src/data/setoid/basic.lean
@@ -249,9 +249,9 @@ variables (r : setoid α) (f : α → β)
 noncomputable def quotient_ker_equiv_range :
   quotient (ker f) ≃ set.range f :=
 equiv.of_bijective (@quotient.lift _ (set.range f) (ker f)
-  (λ x, ⟨f x, set.mem_range_self x⟩) $ λ _ _ h, subtype.eq' h)
+  (λ x, ⟨f x, set.mem_range_self x⟩) $ λ _ _ h, subtype.ext_val h)
   ⟨λ x y h, ker_lift_injective f $ by rcases x; rcases y; injections,
-   λ ⟨w, z, hz⟩, ⟨@quotient.mk _ (ker f) z, by rw quotient.lift_beta; exact subtype.ext.2 hz⟩⟩
+   λ ⟨w, z, hz⟩, ⟨@quotient.mk _ (ker f) z, by rw quotient.lift_beta; exact subtype.ext_iff_val.2 hz⟩⟩
 
 /-- The quotient of α by the kernel of a surjective function f bijects with f's codomain. -/
 noncomputable def quotient_ker_equiv_of_surjective (hf : surjective f) :
@@ -322,7 +322,7 @@ def correspondence (r : setoid α) : ((≤) : {s // r ≤ s} → {s // r ≤ s}
   ((≤) : setoid (quotient r) → setoid (quotient r) → Prop) :=
 { to_fun := λ s, map_of_surjective s.1 quotient.mk ((ker_mk_eq r).symm ▸ s.2) exists_rep,
   inv_fun := λ s, ⟨comap quotient.mk s, λ x y h, show s.rel ⟦x⟧ ⟦y⟧, by rw eq_rel.2 h⟩,
-  left_inv := λ s, subtype.ext.2 $ ext' $ λ _ _,
+  left_inv := λ s, subtype.ext_iff_val.2 $ ext' $ λ _ _,
     ⟨λ h, let ⟨a, b, hx, hy, H⟩ := h in
       s.1.trans' (s.1.symm' $ s.2 $ eq_rel.1 hx) $ s.1.trans' H $ s.2 $ eq_rel.1 hy,
      λ h, ⟨_, _, rfl, rfl, h⟩⟩,
diff --git a/src/data/setoid/partition.lean b/src/data/setoid/partition.lean
index 6c0d4b0ad9458..48f280d9f97d2 100644
--- a/src/data/setoid/partition.lean
+++ b/src/data/setoid/partition.lean
@@ -131,11 +131,11 @@ set.ne_empty_iff_nonempty.1 $ λ hs0, hc.1 $ hs0 ▸ h
 lemma is_partition_classes (r : setoid α) : is_partition r.classes :=
 ⟨empty_not_mem_classes, classes_eqv_classes⟩
 
-lemma is_partition.pairwise_disjoint {c : set (set α)} (hc : is_partition c) : 
+lemma is_partition.pairwise_disjoint {c : set (set α)} (hc : is_partition c) :
   c.pairwise_disjoint :=
 eqv_classes_disjoint hc.2
 
-lemma is_partition.sUnion_eq_univ {c : set (set α)} (hc : is_partition c) : 
+lemma is_partition.sUnion_eq_univ {c : set (set α)} (hc : is_partition c) :
   ⋃₀ c = set.univ :=
 set.eq_univ_of_forall $ λ x, set.mem_sUnion.2 $
   let ⟨t, ht⟩ := hc.2 x in ⟨t, by clear_aux_decl; finish⟩
@@ -170,7 +170,7 @@ instance partition.partial_order : partial_order (subtype (@is_partition α)) :=
   le_trans := λ _ _ _, @le_trans (setoid α) _ _ _ _,
   lt_iff_le_not_le := λ _ _, iff.rfl,
   le_antisymm := λ x y hx hy, let h := @le_antisymm (setoid α) _ _ _ hx hy in by
-    rw [subtype.ext, ←classes_mk_classes x.1 x.2, ←classes_mk_classes y.1 y.2, h] }
+    rw [subtype.ext_iff_val, ←classes_mk_classes x.1 x.2, ←classes_mk_classes y.1 y.2, h] }
 
 variables (α)
 
@@ -180,7 +180,7 @@ def partition.order_iso :
 { to_fun := λ r, ⟨r.classes, empty_not_mem_classes, classes_eqv_classes⟩,
   inv_fun := λ x, mk_classes x.1 x.2.2,
   left_inv := mk_classes_classes,
-  right_inv := λ x, by rw [subtype.ext, ←classes_mk_classes x.1 x.2],
+  right_inv := λ x, by rw [subtype.ext_iff_val, ←classes_mk_classes x.1 x.2],
   ord' := λ x y, by conv {to_lhs, rw [←mk_classes_classes x, ←mk_classes_classes y]}; refl }
 
 variables {α}
diff --git a/src/data/subtype.lean b/src/data/subtype.lean
index 1b932fff7f78f..06828b28a5b77 100644
--- a/src/data/subtype.lean
+++ b/src/data/subtype.lean
@@ -4,60 +4,76 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Johannes Hölzl
 -/
 import tactic.lint
+import tactic.ext
 
--- Lean complains if this section is turned into a namespace
 open function
-section subtype
-variables {α : Sort*} {p : α → Prop}
 
-@[simp] theorem subtype.forall {q : {a // p a} → Prop} :
+namespace subtype
+variables {α : Sort*} {β : Sort*} {γ : Sort*} {p : α → Prop}
+
+/-- A version of `x.property` or `x.2` where `p` is syntactically applied to the coercion of `x`
+  instead of `x.1`. A similar result is `subtype.mem` in `data.set.basic`. -/
+lemma prop (x : subtype p) : p x := x.2
+
+@[simp] lemma val_eq_coe {x : subtype p} : x.1 = ↑x := rfl
+
+@[simp] protected theorem «forall» {q : {a // p a} → Prop} :
   (∀ x, q x) ↔ (∀ a b, q ⟨a, b⟩) :=
 ⟨assume h a b, h ⟨a, b⟩, assume h ⟨a, b⟩, h a b⟩
 
 /-- An alternative version of `subtype.forall`. This one is useful if Lean cannot figure out `q`
   when using `subtype.forall` from right to left. -/
-theorem subtype.forall' {q : ∀x, p x → Prop} :
+protected theorem forall' {q : ∀x, p x → Prop} :
   (∀ x h, q x h) ↔ (∀ x : {a // p a}, q x.1 x.2) :=
 (@subtype.forall _ _ (λ x, q x.1 x.2)).symm
 
-
-@[simp] theorem subtype.exists {q : {a // p a} → Prop} :
+@[simp] protected theorem «exists» {q : {a // p a} → Prop} :
   (∃ x, q x) ↔ (∃ a b, q ⟨a, b⟩) :=
 ⟨assume ⟨⟨a, b⟩, h⟩, ⟨a, b, h⟩, assume ⟨a, b, h⟩, ⟨⟨a, b⟩, h⟩⟩
 
-end subtype
+-- lemma ext {f g : equiv α β} (H : ∀ x, f x = g x) : f = g :=
+-- coe_fn_injective (funext H)
 
-namespace subtype
-variables {α : Sort*} {β : Sort*} {γ : Sort*} {p : α → Prop}
+@[ext] protected lemma ext : ∀ {a1 a2 : {x // p x}}, (a1 : α) = (a2 : α) → a1 = a2
+| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
 
-lemma val_eq_coe : @val _ p = coe := rfl
+lemma ext_iff {a1 a2 : {x // p x}} : a1 = a2 ↔ (a1 : α) = (a2 : α) :=
+⟨congr_arg _, subtype.ext⟩
 
-protected lemma eq' : ∀ {a1 a2 : {x // p x}}, a1.val = a2.val → a1 = a2
-| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
+lemma ext_val {a1 a2 : {x // p x}} : a1.1 = a2.1 → a1 = a2 :=
+subtype.ext
 
-lemma ext {a1 a2 : {x // p x}} : a1 = a2 ↔ a1.val = a2.val :=
-⟨congr_arg _, subtype.eq'⟩
+lemma ext_iff_val {a1 a2 : {x // p x}} : a1 = a2 ↔ a1.1 = a2.1 :=
+ext_iff
 
-lemma coe_ext {a1 a2 : {x // p x}} : a1 = a2 ↔ (a1 : α) = a2 :=
-ext
+@[simp] theorem coe_eta (a : {a // p a}) (h : p a) : mk ↑a h = a := subtype.ext rfl
+
+@[simp] theorem coe_mk (a h) : (@mk α p a h : α) = a := rfl
+
+@[simp, nolint simp_nf] -- built-in reduction doesn't always work
+theorem mk_eq_mk {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' :=
+⟨λ H, by injection H, λ H, by congr; assumption⟩
+
+theorem coe_injective : injective (coe : subtype p → α) :=
+λ a b, subtype.ext
 
 theorem val_injective : injective (@val _ p) :=
-λ a b, subtype.eq'
+coe_injective
 
 /-- Restrict a (dependent) function to a subtype -/
 def restrict {α} {β : α → Type*} (f : Πx, β x) (p : α → Prop) (x : subtype p) : β x.1 :=
-f x.1
+f x
 
 lemma restrict_apply {α} {β : α → Type*} (f : Πx, β x) (p : α → Prop) (x : subtype p) :
   restrict f p x = f x.1 :=
 by refl
 
-lemma restrict_def {α β} (f : α → β) (p : α → Prop) : restrict f p = f ∘ subtype.val :=
+lemma restrict_def {α β} (f : α → β) (p : α → Prop) : restrict f p = f ∘ coe :=
 by refl
 
 lemma restrict_injective {α β} {f : α → β} (p : α → Prop) (h : injective f) :
   injective (restrict f p) :=
-h.comp subtype.val_injective
+h.comp coe_injective
 
 /-- Defining a map into a subtype, this can be seen as an "coinduction principle" of `subtype`-/
 def coind {α β} (f : α → β) {p : β → Prop} (h : ∀a, p (f a)) : α → subtype p :=
@@ -70,7 +86,7 @@ theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀a, p (
 /-- Restriction of a function to a function on subtypes. -/
 def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀a, p a → q (f a)) :
   subtype p → subtype q :=
-λ x, ⟨f x.1, h x.1 x.2⟩
+λ x, ⟨f x, h x x.prop⟩
 
 theorem map_comp {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : subtype p}
   (f : α → β) (h : ∀a, p a → q (f a)) (g : β → γ) (l : ∀a, q a → r (g a)) :
@@ -82,19 +98,19 @@ funext $ assume ⟨v, h⟩, rfl
 
 lemma map_injective {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀a, p a → q (f a))
   (hf : injective f) : injective (map f h) :=
-coind_injective _ $ hf.comp val_injective
+coind_injective _ $ hf.comp coe_injective
 
 instance [has_equiv α] (p : α → Prop) : has_equiv (subtype p) :=
-⟨λ s t, s.val ≈ t.val⟩
+⟨λ s t, (s : α) ≈ (t : α)⟩
 
 theorem equiv_iff [has_equiv α] {p : α → Prop} {s t : subtype p} :
-  s ≈ t ↔ s.val ≈ t.val :=
+  s ≈ t ↔ (s : α) ≈ (t : α) :=
 iff.rfl
 
 variables [setoid α]
 
 protected theorem refl (s : subtype p) : s ≈ s :=
-setoid.refl s.val
+setoid.refl ↑s
 
 protected theorem symm {s t : subtype p} (h : s ≈ t) : t ≈ s :=
 setoid.symm h
@@ -111,21 +127,11 @@ setoid.mk (≈) (equivalence p)
 end subtype
 
 namespace subtype
+/-! Some facts about sets, which require that `α` is a type. -/
 variables {α : Type*} {β : Type*} {γ : Type*} {p : α → Prop}
 
-@[simp] theorem coe_eta {α : Type*} {p : α → Prop}
- (a : {a // p a}) (h : p a) : mk ↑a h = a := eta _ _
-
-@[simp] theorem coe_mk {α : Type*} {p : α → Prop}
- (a h) : (@mk α p a h : α) = a := rfl
-
-@[simp, nolint simp_nf] -- built-in reduction doesn't always work
-theorem mk_eq_mk {α : Type*} {p : α → Prop}
- {a h a' h'} : @mk α p a h = @mk α p a' h' ↔ a = a' :=
-⟨λ H, by injection H, λ H, by congr; assumption⟩
-
-@[simp] lemma val_prop {S : set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
+@[simp] lemma coe_prop {S : set α} (a : {a // a ∈ S}) : ↑a ∈ S := a.prop
 
-@[simp] lemma val_prop' {S : set α} (a : {a // a ∈ S}) : ↑a ∈ S := a.property
+lemma val_prop {S : set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
 
 end subtype
diff --git a/src/data/vector2.lean b/src/data/vector2.lean
index 9677b1f9bca35..f3643a190f819 100644
--- a/src/data/vector2.lean
+++ b/src/data/vector2.lean
@@ -180,11 +180,11 @@ lemma remove_nth_insert_nth_ne {v : vector α (n+1)} :
   begin
     have : i ≠ j := fin.vne_of_ne ne,
     refine subtype.eq _,
-    dsimp [insert_nth, remove_nth, fin.pred_above, fin.cast_lt],
+    dsimp [insert_nth, remove_nth, fin.pred_above, fin.cast_lt, -subtype.val_eq_coe],
     rcases lt_trichotomy i j with h | h | h,
     { have h_nji : ¬ j < i := lt_asymm h,
       have j_pos : 0 < j := lt_of_le_of_lt (zero_le i) h,
-      simp [h, h_nji, fin.lt_iff_val_lt_val],
+      simp [h, h_nji, fin.lt_iff_val_lt_val, -subtype.val_eq_coe],
       rw [show j.pred = j - 1, from rfl, list.insert_nth_remove_nth_of_ge, nat.sub_add_cancel j_pos],
       { rw [v.2], exact lt_of_lt_of_le h (nat.le_of_succ_le_succ hj) },
       { exact nat.le_sub_right_of_add_le h } },
diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
index 84d380751500d..0caee568d90ea 100644
--- a/src/data/zmod/basic.lean
+++ b/src/data/zmod/basic.lean
@@ -542,8 +542,8 @@ calc fintype.card (units (zmod n)) = fintype.card {x : zmod n // x.val.coprime n
 ... = φ n :
 begin
   apply finset.card_congr (λ (a : {x : zmod n // x.val.coprime n}) _, a.1.val),
-  { intro a, simp [a.1.val_lt, a.2.symm] {contextual := tt}, },
-  { intros _ _ _ _ h, rw subtype.ext, apply val_injective, exact h, },
+  { intro a, simp [(a : zmod n).val_lt, a.prop.symm] {contextual := tt} },
+  { intros _ _ _ _ h, rw subtype.ext_iff_val, apply val_injective, exact h, },
   { intros b hb,
     rw [finset.mem_filter, finset.mem_range] at hb,
     refine ⟨⟨b, _⟩, finset.mem_univ _, _⟩,
diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean
index 3e803846c1e13..59ef6bf636323 100644
--- a/src/field_theory/subfield.lean
+++ b/src/field_theory/subfield.lean
@@ -15,10 +15,10 @@ end prio
 
 instance is_subfield.field [is_subfield S] : field S :=
 { inv := λ x, ⟨x⁻¹, is_subfield.inv_mem x.2⟩,
-  zero_ne_one := λ h, zero_ne_one (subtype.ext.1 h),
-  mul_inv_cancel := λ a ha, subtype.ext.2 (mul_inv_cancel
-    (λ h, ha $ subtype.ext.2 h)),
-  inv_zero := subtype.ext.2 inv_zero,
+  zero_ne_one := λ h, zero_ne_one (subtype.ext_iff_val.1 h),
+  mul_inv_cancel := λ a ha, subtype.ext_iff_val.2 (mul_inv_cancel
+    (λ h, ha $ subtype.ext_iff_val.2 h)),
+  inv_zero := subtype.ext_iff_val.2 inv_zero,
   ..show comm_ring S, by apply_instance }
 
 instance univ.is_subfield : is_subfield (@set.univ F) :=
diff --git a/src/geometry/manifold/basic_smooth_bundle.lean b/src/geometry/manifold/basic_smooth_bundle.lean
index c79bfd9e03546..1b86fe76f6276 100644
--- a/src/geometry/manifold/basic_smooth_bundle.lean
+++ b/src/geometry/manifold/basic_smooth_bundle.lean
@@ -338,7 +338,7 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
     have E : x ∈ I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I,
       by simpa only [prod_mk_mem_set_prod_eq, and_true, mem_univ] using hx,
     have : I (I.symm x) = x, by simp [E.2],
-    dsimp,
+    dsimp [-subtype.val_eq_coe],
     rw [this, D x E],
     refl
   end,
diff --git a/src/geometry/manifold/real_instances.lean b/src/geometry/manifold/real_instances.lean
index 1e5f8cc5a7b48..2bd9766b31863 100644
--- a/src/geometry/manifold/real_instances.lean
+++ b/src/geometry/manifold/real_instances.lean
@@ -84,7 +84,7 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
   inv_fun     := λx, ⟨λi, if h : i = 0 then max (x i) 0 else x i, by simp [le_refl]⟩,
   source      := univ,
   target      := range (λx : euclidean_half_space n, x.val),
-  map_source' := λx hx, by simpa only [subtype.val_range] using x.property,
+  map_source' := λx hx, by simpa only [subtype.range_val] using x.property,
   map_target' := λx hx, mem_univ _,
   left_inv'   := λ⟨xval, xprop⟩ hx, begin
     rw subtype.mk_eq_mk,
@@ -94,11 +94,11 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
     { simp only [hi, dif_neg, not_false_iff] }
   end,
   right_inv'  := λx hx, begin
-    simp only [mem_set_of_eq, subtype.val_range] at hx,
+    simp only [mem_set_of_eq, subtype.range_val_subtype] at hx,
     ext1 i,
     by_cases hi : i = 0,
-    { rw hi, simp only [hx, dif_pos, max_eq_left]} ,
-    { simp only [hi, dif_neg, not_false_iff]}
+    { rw hi, simp only [hx, dif_pos, max_eq_left] } ,
+    { simp only [hi, dif_neg, not_false_iff] }
   end,
   source_eq    := rfl,
   unique_diff' := begin
@@ -144,7 +144,7 @@ def model_with_corners_euclidean_quadrant (n : ℕ) :
   inv_fun     := λx, ⟨λi, max (x i) 0, λi, by simp only [le_refl, or_true, le_max_iff]⟩,
   source      := univ,
   target      := range (λx : euclidean_quadrant n, x.val),
-  map_source' := λx hx, by simpa only [subtype.val_range] using x.property,
+  map_source' := λx hx, by simpa only [subtype.range_val] using x.property,
   map_target' := λx hx, mem_univ _,
   left_inv'   := λ⟨xval, xprop⟩ hx, begin
     rw subtype.mk_eq_mk,
@@ -198,10 +198,11 @@ def Icc_left_chart (x y : ℝ) [fact (x < y)] :
 { source      := {z : Icc x y | z.val < y},
   target      := {z : euclidean_half_space 1 | z.val 0 < y - x},
   to_fun      := λ(z : Icc x y), ⟨λi, z.val - x, sub_nonneg.mpr z.property.1⟩,
-  inv_fun     := λz, ⟨min (z.val 0 + x) y, by simp [le_refl, z.property, le_of_lt ‹x < y›]⟩,
+  inv_fun     := λz, ⟨min (z.val 0 + x) y, by simp [le_refl, z.prop, le_of_lt ‹x < y›]⟩,
   map_source' := by simp only [imp_self, sub_lt_sub_iff_right, mem_set_of_eq, forall_true_iff],
   map_target' :=
-    by { simp only [min_lt_iff, mem_set_of_eq], assume z hz, left, dsimp at hz, linarith },
+    by { simp only [min_lt_iff, mem_set_of_eq], assume z hz, left,
+         dsimp [-subtype.val_eq_coe] at hz, linarith },
   left_inv'   := begin
     rintros ⟨z, hz⟩ h'z,
     simp only [mem_set_of_eq, mem_Icc] at hz h'z,
@@ -252,10 +253,11 @@ def Icc_right_chart (x y : ℝ) [fact (x < y)] :
   target      := {z : euclidean_half_space 1 | z.val 0 < y - x},
   to_fun      := λ(z : Icc x y), ⟨λi, y - z.val, sub_nonneg.mpr z.property.2⟩,
   inv_fun     := λz,
-    ⟨max (y - z.val 0) x, by simp [le_refl, z.property, le_of_lt ‹x < y›, sub_eq_add_neg]⟩,
+    ⟨max (y - z.val 0) x, by simp [le_refl, z.prop, le_of_lt ‹x < y›, sub_eq_add_neg]⟩,
   map_source' := by simp only [imp_self, mem_set_of_eq, sub_lt_sub_iff_left, forall_true_iff],
   map_target' :=
-    by { simp only [lt_max_iff, mem_set_of_eq], assume z hz, left, dsimp at hz, linarith },
+    by { simp only [lt_max_iff, mem_set_of_eq], assume z hz, left,
+         dsimp [-subtype.val_eq_coe] at hz, linarith },
   left_inv'   := begin
     rintros ⟨z, hz⟩ h'z,
     simp only [mem_set_of_eq, mem_Icc] at hz h'z,
@@ -337,7 +339,7 @@ begin
       apply M.congr_mono _ (subset_univ _),
       assume z hz,
       simp only [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, dif_pos,
-        lt_add_iff_pos_left, max_lt_iff, lt_min_iff, sub_pos, lt_max_iff, subtype.val_range]
+        lt_add_iff_pos_left, max_lt_iff, lt_min_iff, sub_pos, lt_max_iff, subtype.range_val]
         with mfld_simps at hz,
       have A : 0 ≤ z 0 := hz.2,
       have B : z 0 + x ≤ y, by { have := hz.1.1.1, linarith },
@@ -350,7 +352,7 @@ begin
       apply M.congr_mono _ (subset_univ _),
       assume z hz,
       simp only [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, dif_pos,
-        max_lt_iff, sub_pos, subtype.val_range] with mfld_simps at hz,
+        max_lt_iff, sub_pos, subtype.range_val] with mfld_simps at hz,
       have A : 0 ≤ z 0 := hz.2,
       have B : x ≤ y - z 0, by { have := hz.1.1.1, dsimp at this, linarith },
       ext i,
diff --git a/src/group_theory/congruence.lean b/src/group_theory/congruence.lean
index 0a1e561a07e1c..07ca22fdf1bab 100644
--- a/src/group_theory/congruence.lean
+++ b/src/group_theory/congruence.lean
@@ -519,7 +519,7 @@ def correspondence : ((≤) : {d // c ≤ d} → {d // c ≤ d} → Prop) ≃o
     (by rw mul_ker_mk_eq; exact d.2) $ @exists_rep _ c.to_setoid,
   inv_fun := λ d, ⟨comap (coe : M → c.quotient) (λ x y, rfl) d, λ _ _ h,
     show d _ _, by rw c.eq.2 h; exact d.refl _ ⟩,
-  left_inv := λ d, subtype.ext.2 $ ext $ λ _ _,
+  left_inv := λ d, subtype.ext_iff_val.2 $ ext $ λ _ _,
     ⟨λ h, let ⟨a, b, hx, hy, H⟩ := h in
       d.1.trans (d.1.symm $ d.2 $ c.eq.1 hx) $ d.1.trans H $ d.2 $ c.eq.1 hy,
      λ h, ⟨_, _, rfl, rfl, h⟩⟩,
diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean
index bd63a6e0863c0..b2dfdea148ff9 100644
--- a/src/group_theory/order_of_element.lean
+++ b/src/group_theory/order_of_element.lean
@@ -341,7 +341,7 @@ if hx : ∃ (x : α), x ∈ H ∧ x ≠ (1 : α) then
           nat.find_min hex (int.coe_nat_lt.1 $ by rw [← hk₄];
             exact int.mod_lt_of_pos _ (int.coe_nat_pos.2 (nat.find_spec hex).1))
           ⟨nat.pos_of_ne_zero h, hk₅⟩),
-      ⟨k / (nat.find hex : ℤ), subtype.coe_ext.2 begin
+      ⟨k / (nat.find hex : ℤ), subtype.ext_iff_val.2 begin
         suffices : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) = x,
         { simpa [gpow_mul] },
         rw [int.mul_div_cancel' (int.dvd_of_mod_eq_zero (int.eq_zero_of_nat_abs_eq_zero hk₆)), hk]
diff --git a/src/group_theory/submonoid.lean b/src/group_theory/submonoid.lean
index 3792cdc2a325d..a24f2809b60a9 100644
--- a/src/group_theory/submonoid.lean
+++ b/src/group_theory/submonoid.lean
@@ -694,7 +694,7 @@ S.subtype.cod_mrestrict _ (λ x, h x.2)
 
 @[simp, to_additive]
 lemma range_subtype (s : submonoid M) : s.subtype.mrange = s :=
-ext' $ (coe_mrange _).trans $ set.range_coe_subtype s
+ext' $ (coe_mrange _).trans subtype.range_coe
 
 lemma closure_singleton_eq (x : M) : closure ({x} : set M) = (powers_hom M x).mrange :=
 closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, trivial, pow_one x⟩) $
@@ -708,7 +708,7 @@ by rw [closure_singleton_eq, mem_mrange]; refl
 @[to_additive]
 lemma closure_eq_mrange (s : set M) : closure s = (free_monoid.lift (coe : s → M)).mrange :=
 by rw [mrange, ← free_monoid.closure_range_of, map_mclosure,
-  ← set.range_comp, free_monoid.lift_comp_of, set.range_coe_subtype]
+  ← set.range_comp, free_monoid.lift_comp_of, subtype.range_coe_subtype, set.set_of_mem_eq]
 
 @[to_additive]
 lemma exists_list_of_mem_closure {s : set M} {x : M} (hx : x ∈ closure s) :
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index 68c5b577bfd96..17118d0098e3c 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -984,7 +984,7 @@ open submodule
 
 theorem map_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (h p') :
   submodule.map (cod_restrict p f h) p' = comap p.subtype (p'.map f) :=
-submodule.ext $ λ ⟨x, hx⟩, by simp [subtype.coe_ext]
+submodule.ext $ λ ⟨x, hx⟩, by simp [subtype.ext_iff_val]
 
 theorem comap_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (hf p') :
   submodule.comap (cod_restrict p f hf) p' = submodule.comap f (map p.subtype p') :=
@@ -1315,7 +1315,7 @@ open linear_map
 @[simp] theorem comap_bot (f : M →ₗ[R] M₂) : comap f ⊥ = ker f := rfl
 
 @[simp] theorem ker_subtype : p.subtype.ker = ⊥ :=
-ker_eq_bot_of_injective $ λ x y, subtype.eq'
+ker_eq_bot_of_injective $ λ x y, subtype.ext_val
 
 @[simp] theorem range_subtype : p.subtype.range = p :=
 by simpa using map_comap_subtype p ⊤
@@ -1396,7 +1396,7 @@ def map_subtype.order_iso :
 { to_fun    := λ p', ⟨map p.subtype p', map_subtype_le p _⟩,
   inv_fun   := λ q, comap p.subtype q,
   left_inv  := λ p', comap_map_eq_self $ by simp,
-  right_inv := λ ⟨q, hq⟩, subtype.eq' $ by simp [map_comap_subtype p, inf_of_le_right hq],
+  right_inv := λ ⟨q, hq⟩, subtype.ext_val $ by simp [map_comap_subtype p, inf_of_le_right hq],
   ord'      := λ p₁ p₂, (map_le_map_iff' (ker_subtype p)).symm }
 
 /-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
@@ -1492,7 +1492,7 @@ def comap_mkq.order_iso :
 { to_fun    := λ p', ⟨comap p.mkq p', le_comap_mkq p _⟩,
   inv_fun   := λ q, map p.mkq q,
   left_inv  := λ p', map_comap_eq_self $ by simp,
-  right_inv := λ ⟨q, hq⟩, subtype.eq' $ by simpa [comap_map_mkq p],
+  right_inv := λ ⟨q, hq⟩, subtype.ext_val $ by simpa [comap_map_mkq p],
   ord'      := λ p₁ p₂, (comap_le_comap_iff $ range_mkq _).symm }
 
 /-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
@@ -2135,10 +2135,10 @@ begin
     assume j hjJ,
     have : j ∉ I := assume hjI, hd ⟨hjI, hjJ⟩,
     rw [dif_neg this, zero_apply] },
-  { simp only [pi_comp, comp_assoc, subtype_comp_cod_restrict, proj_pi, dif_pos, subtype.val_prop'],
+  { simp only [pi_comp, comp_assoc, subtype_comp_cod_restrict, proj_pi, dif_pos, subtype.coe_prop],
     ext b ⟨j, hj⟩, refl },
-  { ext ⟨b, hb⟩,
-    apply subtype.coe_ext.2,
+  { ext1 ⟨b, hb⟩,
+    apply subtype.ext,
     ext j,
     have hb : ∀i ∈ J, b i = 0,
     { simpa only [mem_infi, mem_ker, proj_apply] using (mem_infi _).1 hb },
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
index c5a460b34d37c..0714ed441a0de 100644
--- a/src/linear_algebra/basis.lean
+++ b/src/linear_algebra/basis.lean
@@ -182,34 +182,34 @@ section subtype
 /-! The following lemmas use the subtype defined by a set in `M` as the index set `ι`. -/
 
 theorem linear_independent_comp_subtype {s : set ι} :
-  linear_independent R (v ∘ subtype.val : s → M) ↔
+  linear_independent R (v ∘ coe : s → M) ↔
   ∀ l ∈ (finsupp.supported R R s), (finsupp.total ι M R v) l = 0 → l = 0 :=
 begin
   rw [linear_independent_iff, finsupp.total_comp],
   simp only [linear_map.comp_apply],
   split,
   { intros h l hl₁ hl₂,
-    have h_bij : bij_on subtype.val (subtype.val ⁻¹' ↑l.support : set s) ↑l.support,
+    have h_bij : bij_on coe (coe ⁻¹' ↑l.support : set s) ↑l.support,
     { apply bij_on.mk,
       { apply maps_to_preimage },
-      { apply subtype.val_injective.inj_on },
+      { apply subtype.coe_injective.inj_on },
       intros i hi,
-      rw [image_preimage_eq_inter_range, subtype.range_val],
+      rw [image_preimage_eq_inter_range, subtype.range_coe],
       exact ⟨hi, (finsupp.mem_supported _ _).1 hl₁ hi⟩ },
     show l = 0,
-    { apply finsupp.eq_zero_of_comap_domain_eq_zero (subtype.val : s → ι) _ h_bij,
+    { apply finsupp.eq_zero_of_comap_domain_eq_zero (coe : s → ι) _ h_bij,
       apply h,
       convert hl₂,
       rw [finsupp.lmap_domain_apply, finsupp.map_domain_comap_domain],
-      exact subtype.val_injective,
-      rw subtype.range_val,
+      exact subtype.coe_injective,
+      rw subtype.range_coe,
       exact (finsupp.mem_supported _ _).1 hl₁ } },
   { intros h l hl,
-    have hl' : finsupp.total ι M R v (finsupp.emb_domain ⟨subtype.val, subtype.val_injective⟩ l) = 0,
-    { rw finsupp.emb_domain_eq_map_domain ⟨subtype.val, subtype.val_injective⟩ l,
+    have hl' : finsupp.total ι M R v (finsupp.emb_domain ⟨coe, subtype.coe_injective⟩ l) = 0,
+    { rw finsupp.emb_domain_eq_map_domain ⟨coe, subtype.coe_injective⟩ l,
       apply hl },
     apply finsupp.emb_domain_inj.1,
-    rw [h (finsupp.emb_domain ⟨subtype.val, subtype.val_injective⟩ l) _ hl',
+    rw [h (finsupp.emb_domain ⟨coe, subtype.coe_injective⟩ l) _ hl',
         finsupp.emb_domain_zero],
     rw [finsupp.mem_supported, finsupp.support_emb_domain],
     intros x hx,
@@ -225,7 +225,7 @@ theorem linear_independent_subtype {s : set M} :
 by apply @linear_independent_comp_subtype _ _ _ id
 
 theorem linear_independent_comp_subtype_disjoint {s : set ι} :
-  linear_independent R (v ∘ subtype.val : s → M) ↔
+  linear_independent R (v ∘ coe : s → M) ↔
   disjoint (finsupp.supported R R s) (finsupp.total ι M R v).ker :=
 by rw [linear_independent_comp_subtype, linear_map.disjoint_ker]
 
@@ -281,23 +281,23 @@ begin
 end
 
 lemma linear_independent.restrict_of_comp_subtype {s : set ι}
-  (hs : linear_independent R (v ∘ subtype.val : s → M)) :
+  (hs : linear_independent R (v ∘ coe : s → M)) :
   linear_independent R (s.restrict v) :=
 begin
-  have h_restrict : restrict v s = v ∘ (λ x, x.val) := rfl,
+  have h_restrict : restrict v s = v ∘ coe := rfl,
   rw [linear_independent_iff, h_restrict, finsupp.total_comp],
   intros l hl,
-  have h_map_domain_subtype_eq_0 : l.map_domain subtype.val = 0,
+  have h_map_domain_subtype_eq_0 : l.map_domain coe = 0,
   { rw linear_independent_comp_subtype at hs,
-    apply hs (finsupp.lmap_domain R R (λ x : subtype s, x.val) l) _ hl,
+    apply hs (finsupp.lmap_domain R R coe l) _ hl,
     rw finsupp.mem_supported,
     simp,
     intros x hx,
     have := finset.mem_coe.2 (finsupp.map_domain_support (finset.mem_coe.1 hx)),
     rw finset.coe_image at this,
-    exact subtype.val_image_subset _ _ this },
+    exact subtype.coe_image_subset _ _ this },
   apply @finsupp.map_domain_injective _ (subtype s) ι,
-  { apply subtype.val_injective },
+  { apply subtype.coe_injective },
   { simpa },
 end
 
@@ -471,7 +471,7 @@ def linear_independent.repr (hv : linear_independent R v) :
   span R (range v) →ₗ[R] ι →₀ R := hv.total_equiv.symm
 
 lemma linear_independent.total_repr (x) : finsupp.total ι M R v (hv.repr x) = x :=
-subtype.coe_ext.1 (linear_equiv.apply_symm_apply hv.total_equiv x)
+subtype.ext_iff.1 (linear_equiv.apply_symm_apply hv.total_equiv x)
 
 lemma linear_independent.total_comp_repr :
   (finsupp.total ι M R v).comp hv.repr = submodule.subtype _ :=
@@ -491,7 +491,7 @@ begin
       = finsupp.total ι M R v l := rfl,
   have : (linear_independent.total_equiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x,
   { rw eq at this,
-    exact subtype.coe_ext.2 this },
+    exact subtype.ext_iff.2 this },
   rw ←linear_equiv.symm_apply_apply hv.total_equiv l,
   rw ←this,
   refl,
@@ -557,7 +557,7 @@ end
 lemma eq_of_linear_independent_of_span_subtype {s t : set M} (zero_ne_one : (0 : R) ≠ 1)
   (hs : linear_independent R (λ x, x : s → M)) (h : t ⊆ s) (hst : s ⊆ span R t) : s = t :=
 begin
-  let f : t ↪ s := ⟨λ x, ⟨x.1, h x.2⟩, λ a b hab, subtype.val_injective (subtype.mk.inj hab)⟩,
+  let f : t ↪ s := ⟨λ x, ⟨x.1, h x.2⟩, λ a b hab, subtype.coe_injective (subtype.mk.inj hab)⟩,
   have h_surj : surjective f,
   { apply surjective_of_linear_independent_of_span hs f _ zero_ne_one,
     convert hst; simp [f, comp], },
@@ -699,7 +699,7 @@ have h4 : g a = 0, from calc
 (finset.forall_mem_insert _ _ _).2 ⟨h4, h3⟩)
 
 lemma le_of_span_le_span {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
-  (hl : linear_independent R (subtype.val : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u)
+  (hl : linear_independent R (coe : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u)
   (hst : span R s ≤ span R t) : s ⊆ t :=
 begin
   have := eq_of_linear_independent_of_span_subtype zero_ne_one
@@ -710,7 +710,7 @@ begin
 end
 
 lemma span_le_span_iff {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
-  (hl : linear_independent R (subtype.val : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u) :
+  (hl : linear_independent R (coe : u → M)) (hsu : s ⊆ u) (htu : t ⊆ u) :
   span R s ≤ span R t ↔ s ⊆ t :=
 ⟨le_of_span_le_span zero_ne_one hl hsu htu, span_mono⟩
 
@@ -915,7 +915,7 @@ split,
     by rw h₂; apply subtype.mem x,
   rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩,
   have h_x_eq_y : x = y,
-    by rw [subtype.coe_ext, ← hy₂]; simp,
+    by rw [subtype.ext_iff, ← hy₂]; simp,
   rw h_x_eq_y,
   exact hy₁ }
 end
@@ -929,7 +929,7 @@ lemma is_basis_empty_bot (h_empty : ¬ nonempty ι) :
 begin
   apply is_basis_empty h_empty,
   intro x,
-  apply subtype.ext.2,
+  apply subtype.ext_iff_val.2,
   exact (submodule.mem_bot R).1 (subtype.mem x),
 end
 
@@ -1170,7 +1170,7 @@ begin
   have : linear_independent K (λ x, x : f '' B → V'),
   { have h₁ := hB₀.image_subtype
       (show disjoint (span K (range (λ i : B, i.val))) (linear_map.ker f), by simp [hf_inj]),
-    rwa B.range_coe_subtype at h₁ },
+    rwa subtype.range_coe at h₁ },
   rcases exists_subset_is_basis this with ⟨C, BC, hC⟩,
   haveI : inhabited V := ⟨0⟩,
   use hC.constr (C.restrict (inv_fun f)),
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index a2b31855f785c..7596f469e8fa9 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -145,7 +145,7 @@ by rw [←cardinal.lift_inj, ← (is_basis_span hv).mk_eq_dim,
 
 lemma dim_span_set {s : set V} (hs : linear_independent K (λ x, x : s → V)) :
   dim K ↥(span K s) = cardinal.mk s :=
-by rw [← @set_of_mem_eq _ s, ← subtype.val_range]; exact dim_span hs
+by { rw [← @set_of_mem_eq _ s, ← subtype.range_coe_subtype], exact dim_span hs }
 
 lemma cardinal_le_dim_of_linear_independent
   {ι : Type u'} {v : ι → V} (hv : linear_independent K v) :
@@ -163,7 +163,7 @@ lemma cardinal_le_dim_of_linear_independent'
 begin
   -- extend s to a basis
   obtain ⟨b, ss, h⟩ := exists_subset_is_basis hs,
-  rw [←h.mk_range_eq_dim, range_coe_subtype],
+  rw [←h.mk_range_eq_dim, subtype.range_coe],
   apply cardinal.mk_le_of_injective (inclusion_injective ss),
 end
 
@@ -250,7 +250,7 @@ by { rw [dim_eq_of_injective f h], exact dim_submodule_le _ }
 
 lemma dim_le_of_submodule (s t : submodule K V) (h : s ≤ t) : dim K s ≤ dim K t :=
 dim_le_of_injective (of_le h) $ assume ⟨x, hx⟩ ⟨y, hy⟩ eq,
-  subtype.eq $ show x = y, from subtype.ext.1 eq
+  subtype.eq $ show x = y, from subtype.ext_iff_val.1 eq
 
 section
 variables [add_comm_group V₃] [vector_space K V₃]
@@ -418,7 +418,7 @@ begin
   { intros h x,
     cases exists_is_basis K V with w hw,
     have card_mk_range := hw.mk_range_eq_dim,
-    rw [h, cardinal.mk_emptyc_iff, set.range_coe_subtype] at card_mk_range,
+    rw [h, cardinal.mk_emptyc_iff, subtype.range_coe] at card_mk_range,
     simpa [card_mk_range] using hw.mem_span x },
   { intro h,
     have : (⊤ : submodule K V) = ⊥,
diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean
index 858f3d07d79e6..ac1633eeb2249 100644
--- a/src/linear_algebra/dual.lean
+++ b/src/linear_algebra/dual.lean
@@ -44,7 +44,7 @@ instance : inhabited (dual R M) := by dunfold dual; apply_instance
 
 instance : has_coe_to_fun (dual R M) := ⟨_, linear_map.to_fun⟩
 
-/-- Maps a module M to the dual of the dual of M. See `vector_space.eval_range` and
+/-- Maps a module M to the dual of the dual of M. See `vector_space.erange_coe` and
 `vector_space.eval_equiv`. -/
 def eval : M →ₗ[R] (dual R (dual R M)) := linear_map.flip linear_map.id
 
@@ -216,7 +216,7 @@ begin
 end
 
 
-lemma eval_range (h : dim K V < omega) : (eval K V).range = ⊤ :=
+lemma erange_coe (h : dim K V < omega) : (eval K V).range = ⊤ :=
 begin
   classical,
   rcases exists_is_basis_fintype h with ⟨b, hb, ⟨hf⟩⟩,
@@ -226,7 +226,7 @@ end
 
 /-- A vector space is linearly equivalent to the dual of its dual space. -/
 def eval_equiv (h : dim K V < omega) : V ≃ₗ[K] dual K (dual K V) :=
-linear_equiv.of_bijective (eval K V) eval_ker (eval_range h)
+linear_equiv.of_bijective (eval K V) eval_ker (erange_coe h)
 
 end vector_space
 
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
index 813563bbf5575..52d797dbcbd35 100644
--- a/src/linear_algebra/finite_dimensional.lean
+++ b/src/linear_algebra/finite_dimensional.lean
@@ -84,7 +84,7 @@ begin
   cases exists_is_basis K V with b hb,
   have := is_basis.mk_eq_dim hb,
   simp only [lift_id] at this,
-  rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ b, ← subtype.val_range],
+  rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ b, ← subtype.range_coe_subtype],
   split,
   { intro, resetI, convert finite_of_linear_independent hb.1, simp },
   { assume hbfinite,
@@ -102,11 +102,12 @@ finite_dimensional_iff_dim_lt_omega.1
 
 /-- In a finite dimensional space, there exists a finite basis. A basis is in general given as a
 function from an arbitrary type to the vector space. Here, we think of a basis as a set (instead of
-a function), and use as parametrizing type this set (and as a function the function `subtype.val`).
+a function), and use as parametrizing type this set (and as a function the coercion
+  `coe : s → V`).
 -/
 variables (K V)
 lemma exists_is_basis_finite [finite_dimensional K V] :
-  ∃ s : set V, (is_basis K (subtype.val : s → V)) ∧ s.finite :=
+  ∃ s : set V, (is_basis K (coe : s → V)) ∧ s.finite :=
 begin
   cases exists_is_basis K V with s hs,
   exact ⟨s, hs, finite_of_linear_independent hs.1⟩
@@ -116,7 +117,7 @@ end
 This is in contrast to `exists_is_basis_finite`, which provides a set and a `set.finite`.
 -/
 lemma exists_is_basis_finset [finite_dimensional K V] :
-  ∃ b : finset V, is_basis K (subtype.val : (↑b : set V) → V) :=
+  ∃ b : finset V, is_basis K (coe : (↑b : set V) → V) :=
 begin
   obtain ⟨s, s_basis, s_finite⟩ := exists_is_basis_finite K V,
   refine ⟨s_finite.to_finset, _⟩,
@@ -147,7 +148,7 @@ lemma of_finite_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K
 iff_fg.2 $ ⟨finset.univ.image b, by {convert h.2, simp} ⟩
 
 /-- If a vector space has a finite basis, then it is finite-dimensional, finset style. -/
-lemma of_finset_basis {b : finset V} (h : is_basis K (subtype.val : (↑b : set V) -> V)) :
+lemma of_finset_basis {b : finset V} (h : is_basis K (coe : (↑b : set V) -> V)) :
   finite_dimensional K V :=
 iff_fg.2 $ ⟨b, by {convert h.2, simp} ⟩
 
@@ -384,9 +385,9 @@ begin
   have : subtype.val '' bS = b, from set.eq_of_subset_of_card_le hb.1
     (by rw [set.card_image_of_injective _ subtype.val_injective, ← findim_eq_card_basis hbS,
          ← findim_eq_card_basis hb.2, h]; apply_instance),
-  erw [← hb.2.2, subtype.val_range, ← this, set.set_of_mem_eq, ← subtype_eq_val, span_image],
+  erw [← hb.2.2, subtype.range_coe, ← this, ← subtype_eq_val, span_image],
   have := hbS.2,
-  erw [subtype.val_range, set.set_of_mem_eq] at this,
+  erw [subtype.range_coe] at this,
   rw [this, map_top (submodule.subtype S), range_subtype],
 end
 
diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
index 469107bc6cdf0..8b168f3ff7ef0 100644
--- a/src/linear_algebra/finsupp.lean
+++ b/src/linear_algebra/finsupp.lean
@@ -146,14 +146,9 @@ end
 theorem restrict_dom_comp_subtype (s : set α) :
   (restrict_dom M R s).comp (submodule.subtype _) = linear_map.id :=
 begin
-  ext l,
-  apply subtype.coe_ext.2,
-  simp,
-  ext a,
-  by_cases a ∈ s,
-  { simp [h] },
-  { rw [filter_apply_neg (λ x, x ∈ s) _ h],
-    exact ((mem_supported' R l.1).1 l.2 a h).symm }
+  ext l a,
+  by_cases a ∈ s; simp [h],
+  exact ((mem_supported' R l.1).1 l.2 a h).symm
 end
 
 theorem range_restrict_dom (s : set α) :
diff --git a/src/linear_algebra/linear_pmap.lean b/src/linear_algebra/linear_pmap.lean
index 8de5b18a26058..f2aec4a03d97d 100644
--- a/src/linear_algebra/linear_pmap.lean
+++ b/src/linear_algebra/linear_pmap.lean
@@ -25,8 +25,6 @@ is bounded above.
 Another possible use (not yet in `mathlib`) would be the theory of unbounded linear operators.
 -/
 
-lemma subtype.coe_prop {α : Type*} {p : α → Prop} (x : subtype p) : p x := x.2
-
 open set
 
 universes u v w
@@ -78,7 +76,7 @@ begin
     rw [← sub_eq_zero, ← sub_smul] at h ⊢,
     exact H _ h },
   refine ⟨span R {x}, λ z, _, _, _⟩,
-  { exact (classical.some (mem_span_singleton.1 z.coe_prop) • y) },
+  { exact (classical.some (mem_span_singleton.1 z.prop) • y) },
   { intros z₁ z₂,
     rw [← add_smul],
     apply H,
@@ -203,7 +201,7 @@ private lemma sup_aux (f g : linear_pmap R E F)
     ∀ (x : f.domain) (y : g.domain) (z),
       (x:E) + y = ↑z → fg z = f x + g y :=
 begin
-  choose x hx y hy hxy using λ z : f.domain ⊔ g.domain, mem_sup.1 z.coe_prop,
+  choose x hx y hy hxy using λ z : f.domain ⊔ g.domain, mem_sup.1 z.prop,
   set fg := λ z, f ⟨x z, hx z⟩ + g ⟨y z, hy z⟩,
   have fg_eq : ∀ (x' : f.domain) (y' : g.domain) (z' : f.domain ⊔ g.domain) (H : (x':E) + y' = z'),
     fg z' = f x' + g y',
@@ -265,7 +263,7 @@ begin
   simpa
 end
 
-protected lemma sup_le {f g h : linear_pmap R E F} 
+protected lemma sup_le {f g h : linear_pmap R E F}
   (H : ∀ (x : f.domain) (y : g.domain), (x:E) = y → f x = g y)
   (fh : f ≤ h) (gh : g ≤ h) :
   f.sup g H ≤ h :=
diff --git a/src/linear_algebra/special_linear_group.lean b/src/linear_algebra/special_linear_group.lean
index dced89db1dc94..7ddc9aa1a2761 100644
--- a/src/linear_algebra/special_linear_group.lean
+++ b/src/linear_algebra/special_linear_group.lean
@@ -75,7 +75,7 @@ instance coe_fun : has_coe_to_fun (special_linear_group n R) :=
 def to_lin (A : special_linear_group n R) := matrix.to_lin A
 
 lemma ext_iff (A B : special_linear_group n R) : A = B ↔ (∀ i j, A i j = B i j) :=
-iff.trans subtype.ext ⟨(λ h i j, congr_fun (congr_fun h i) j), matrix.ext⟩
+iff.trans subtype.ext_iff_val ⟨(λ h i j, congr_fun (congr_fun h i) j), matrix.ext⟩
 
 @[ext] lemma ext (A B : special_linear_group n R) : (∀ i j, A i j = B i j) → A = B :=
 (special_linear_group.ext_iff A B).mpr
diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean
index 4e664a872f65e..e50a21c07f343 100644
--- a/src/logic/embedding.lean
+++ b/src/logic/embedding.lean
@@ -106,7 +106,7 @@ protected def some {α} : α ↪ option α :=
 
 /-- Embedding of a `subtype`. -/
 def subtype {α} (p : α → Prop) : subtype p ↪ α :=
-⟨subtype.val, λ _ _, subtype.eq'⟩
+⟨subtype.val, λ _ _, subtype.ext_val⟩
 
 /-- Choosing an element `b : β` gives an embedding of `punit` into `β`. -/
 def punit {β : Sort*} (b : β) : punit ↪ β :=
diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean
index 019b0ae7c95f0..c24b8dc29d781 100644
--- a/src/measure_theory/measurable_space.lean
+++ b/src/measure_theory/measurable_space.lean
@@ -514,7 +514,7 @@ lemma is_measurable_subtype_image [measurable_space α] {s : set α} {t : set s}
   (hs : is_measurable s) : is_measurable t → is_measurable ((coe : s → α) '' t)
 | ⟨u, (hu : is_measurable u), (eq : coe ⁻¹' u = t)⟩ :=
   begin
-    rw [← eq, image_preimage_eq_inter_range, range_coe_subtype],
+    rw [← eq, image_preimage_eq_inter_range, subtype.range_coe],
     exact is_measurable.inter hu hs
   end
 
@@ -526,8 +526,8 @@ lemma measurable_of_measurable_union_cover
 assume u (hu : is_measurable u), show is_measurable (f ⁻¹' u), from
 begin
   rw show f ⁻¹' u = coe '' (coe ⁻¹' (f ⁻¹' u) : set s) ∪ coe '' (coe ⁻¹' (f ⁻¹' u) : set t),
-    by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, range_coe_subtype,
-      range_coe_subtype, ← inter_distrib_left, univ_subset_iff.1 h, inter_univ],
+    by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, subtype.range_coe,
+      subtype.range_coe, ← inter_distrib_left, univ_subset_iff.1 h, inter_univ],
   exact is_measurable.union
     (is_measurable_subtype_image hs (hc _ hu))
     (is_measurable_subtype_image ht (hd _ hu))
diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean
index d76f089613b4a..92dab8f0dd58b 100644
--- a/src/measure_theory/measure_space.lean
+++ b/src/measure_theory/measure_space.lean
@@ -397,7 +397,7 @@ begin
   haveI := hs.to_encodable,
   rw [← measure_Union, bUnion_eq_Union],
   { rintro ⟨i, hi⟩ ⟨j, hj⟩ ij x ⟨h₁, h₂⟩,
-    exact hd i hi j hj (mt subtype.eq' ij:_) ⟨h₁, h₂⟩ },
+    exact hd i hi j hj (mt subtype.ext_val ij:_) ⟨h₁, h₂⟩ },
   { simpa }
 end
 
diff --git a/src/measure_theory/probability_mass_function.lean b/src/measure_theory/probability_mass_function.lean
index fb12be82984be..8fa5ad8192ac0 100644
--- a/src/measure_theory/probability_mass_function.lean
+++ b/src/measure_theory/probability_mass_function.lean
@@ -73,7 +73,7 @@ by ext b; simp [this]
 @[simp] lemma bind_bind (p : pmf α) (f : α → pmf β) (g : β → pmf γ) :
   (p.bind f).bind g = p.bind (λa, (f a).bind g) :=
 begin
-  ext b,
+  ext1 b,
   simp only [ennreal.coe_eq_coe.symm, coe_bind_apply, ennreal.tsum_mul_left.symm,
              ennreal.tsum_mul_right.symm],
   rw [ennreal.tsum_comm],
@@ -83,7 +83,7 @@ end
 lemma bind_comm (p : pmf α) (q : pmf β) (f : α → β → pmf γ) :
   p.bind (λa, q.bind (f a)) = q.bind (λb, p.bind (λa, f a b)) :=
 begin
-  ext b,
+  ext1 b,
   simp only [ennreal.coe_eq_coe.symm, coe_bind_apply, ennreal.tsum_mul_left.symm,
              ennreal.tsum_mul_right.symm],
   rw [ennreal.tsum_comm],
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
index 49fc50536d67f..062b5769fc367 100644
--- a/src/order/complete_lattice.lean
+++ b/src/order/complete_lattice.lean
@@ -741,7 +741,7 @@ lemma infi_subtype'' {ι} (s : set ι) (f : ι → α) :
 infi_subtype
 
 lemma is_glb_binfi {s : set β} {f : β → α} : is_glb (f '' s) (⨅ x ∈ s, f x) :=
-by simpa only [range_comp, subtype.range_val, infi_subtype'] using @is_glb_infi α s _ (f ∘ subtype.val)
+by simpa only [range_comp, subtype.range_coe, infi_subtype'] using @is_glb_infi α s _ (f ∘ coe)
 
 theorem supr_subtype {p : ι → Prop} {f : subtype p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
 le_antisymm
@@ -753,7 +753,7 @@ lemma supr_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
 (@supr_subtype _ _ _ p (λ x, f x.val x.property)).symm
 
 lemma is_lub_bsupr {s : set β} {f : β → α} : is_lub (f '' s) (⨆ x ∈ s, f x) :=
-by simpa only [range_comp, subtype.range_val, supr_subtype'] using @is_lub_supr α s _ (f ∘ subtype.val)
+by simpa only [range_comp, subtype.range_coe, supr_subtype'] using @is_lub_supr α s _ (f ∘ coe)
 
 theorem infi_sigma {p : β → Type w} {f : sigma p → α} : (⨅ x, f x) = (⨅ i (h:p i), f ⟨i, h⟩) :=
 le_antisymm
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
index 34195e7fd383a..c303190636c38 100644
--- a/src/order/filter/basic.lean
+++ b/src/order/filter/basic.lean
@@ -1453,7 +1453,7 @@ begin
     rcases V_in with ⟨W, W_in, H⟩,
     rw mem_inf_sets,
     use [W, W_in, s, mem_principal_self s],
-    erw [← image_subset_iff, subtype.image_preimage_val] at H,
+    erw [← image_subset_iff, subtype.image_preimage_coe] at H,
     exact H }
 end
 
diff --git a/src/order/filter/ultrafilter.lean b/src/order/filter/ultrafilter.lean
index f08b90e582d51..4b7fd8aa4d1c9 100644
--- a/src/order/filter/ultrafilter.lean
+++ b/src/order/filter/ultrafilter.lean
@@ -158,7 +158,7 @@ begin
   by_contradiction hs',
   let j : (-s) → α := subtype.val,
   have j_inv_s : j ⁻¹' s = ∅, by
-    erw [←preimage_inter_range, subtype.val_range, inter_compl_self, preimage_empty],
+    erw [←preimage_inter_range, subtype.range_coe, inter_compl_self, preimage_empty],
   let f' := comap j f,
   have : f' ≠ ⊥,
   { apply mt empty_in_sets_eq_bot.mpr,
@@ -166,7 +166,7 @@ begin
     suffices : t ⊆ s, from absurd (f.sets_of_superset htf this) hs',
     rw [subset_empty_iff] at ht,
     have : j '' (j ⁻¹' t) = ∅, by rw [ht, image_empty],
-    erw [image_preimage_eq_inter_range, subtype.val_range, ←subset_compl_iff_disjoint,
+    erw [image_preimage_eq_inter_range, subtype.range_coe, ←subset_compl_iff_disjoint,
       set.compl_compl] at this,
     exact this },
   rcases exists_ultrafilter this with ⟨g', g'f', u'⟩,
@@ -246,7 +246,7 @@ end
 
 lemma ultrafilter.eq_iff_val_le_val {u v : ultrafilter α} : u = v ↔ u.val ≤ v.val :=
 ⟨assume h, by rw h; exact le_refl _,
- assume h, by rw subtype.ext; apply ultrafilter_unique v.property u.property.1 h⟩
+ assume h, by rw subtype.ext_iff_val; apply ultrafilter_unique v.property u.property.1 h⟩
 
 lemma exists_ultrafilter_iff (f : filter α) : (∃ (u : ultrafilter α), u.val ≤ f) ↔ f ≠ ⊥ :=
 ⟨assume ⟨u, uf⟩, ne_bot_of_le_ne_bot u.property.1 uf,
diff --git a/src/order/zorn.lean b/src/order/zorn.lean
index 65512240d8a4e..61c638281a3f0 100644
--- a/src/order/zorn.lean
+++ b/src/order/zorn.lean
@@ -245,7 +245,7 @@ theorem zorn_subset {α : Type u} (S : set (set α))
   (h : ∀c ⊆ S, chain (⊆) c → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
   ∃ m ∈ S, ∀a ∈ S, m ⊆ a → a = m :=
 begin
-  letI : partial_order S := partial_order.lift subtype.val (λ _ _, subtype.eq'),
+  letI : partial_order S := partial_order.lift subtype.val (λ _ _, subtype.ext_val),
   have : ∀c:set S, @chain S (≤) c → ∃ub, ∀a∈c, a ≤ ub,
   { intros c hc,
     rcases h (subtype.val '' c) (image_subset_iff.2 _) _ with ⟨s, sS, hs⟩,
diff --git a/src/ring_theory/algebraic.lean b/src/ring_theory/algebraic.lean
index cab3e04a9c1e9..871bc6d4073a1 100644
--- a/src/ring_theory/algebraic.lean
+++ b/src/ring_theory/algebraic.lean
@@ -130,5 +130,5 @@ begin
       monic_integral_normalization p_ne_zero,
       integral_normalization_aeval_eq_zero p_ne_zero px inj ⟩,
   refine ⟨⟨_, x_integral⟩, ⟨_, y_integral⟩, _, rfl⟩,
-  exact λ h, a_ne_zero (inj _ (subtype.ext.mp h))
+  exact λ h, a_ne_zero (inj _ (subtype.ext_iff_val.mp h))
 end
diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean
index e4cca56893dcb..6d0f711fc3613 100644
--- a/src/ring_theory/fractional_ideal.lean
+++ b/src/ring_theory/fractional_ideal.lean
@@ -106,7 +106,7 @@ instance : has_mem P (fractional_ideal f) := ⟨λ x I, x ∈ (I : submodule R f
 -/
 @[ext]
 lemma ext {I J : fractional_ideal f} : (I : submodule R f.codomain) = J → I = J :=
-subtype.ext.mpr
+subtype.ext_iff_val.mpr
 
 lemma fractional_of_subset_one (I : submodule R f.codomain)
   (h : I ≤ (submodule.span R {1})) :
diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
index c4fec252da5d6..792b95337a5c2 100644
--- a/src/ring_theory/integral_closure.lean
+++ b/src/ring_theory/integral_closure.lean
@@ -317,7 +317,7 @@ begin
   { rw [← set.mem_range], dsimp only,
     apply (polynomial.mem_map_range _).2,
     { intros i, specialize coeffs_mem i, rw ← subalgebra.mem_coe at coeffs_mem,
-      convert coeffs_mem, exact subtype.val_range } },
+      convert coeffs_mem, exact subtype.range_coe } },
   use q,
   split,
   { suffices h : (q.map (algebra_map (adjoin R S) (comap R A B))).monic,
@@ -368,9 +368,9 @@ section integral_domain
 variables {R S : Type*} [comm_ring R] [integral_domain S] [algebra R S]
 
 instance : integral_domain (integral_closure R S) :=
-{ zero_ne_one := mt subtype.ext.mp zero_ne_one,
+{ zero_ne_one := mt subtype.ext_iff_val.mp zero_ne_one,
   eq_zero_or_eq_zero_of_mul_eq_zero := λ ⟨a, ha⟩ ⟨b, hb⟩ h,
-    or.imp subtype.ext.mpr subtype.ext.mpr (eq_zero_or_eq_zero_of_mul_eq_zero (subtype.ext.mp h)),
+    or.imp subtype.ext_iff_val.mpr subtype.ext_iff_val.mpr (eq_zero_or_eq_zero_of_mul_eq_zero (subtype.ext_iff_val.mp h)),
   ..(integral_closure R S).comm_ring R S }
 
 end integral_domain
diff --git a/src/ring_theory/integral_domain.lean b/src/ring_theory/integral_domain.lean
index 71ae02cd4c605..6039a70ee3855 100644
--- a/src/ring_theory/integral_domain.lean
+++ b/src/ring_theory/integral_domain.lean
@@ -94,7 +94,7 @@ begin
     ext g,
     rw [monoid_hom.one_apply],
     cases hx ⟨f.to_hom_units g, g, rfl⟩ with n hn,
-    rwa [subtype.coe_ext, units.ext_iff, subtype.coe_mk, monoid_hom.coe_to_hom_units,
+    rwa [subtype.ext_iff, units.ext_iff, subtype.coe_mk, monoid_hom.coe_to_hom_units,
       is_submonoid.coe_pow, units.coe_pow, is_submonoid.coe_one, units.coe_one,
       _root_.one_pow, eq_comm] at hn, },
   replace hx1 : (x : R) - 1 ≠ 0,
diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean
index cdf72e9b72c53..5cb7df20ea5a8 100644
--- a/src/ring_theory/localization.lean
+++ b/src/ring_theory/localization.lean
@@ -297,7 +297,7 @@ f.to_localization_map.mk'_self' _ hx
 @[simp] lemma mk'_self' {x : M} : f.mk' x x = 1 :=
 f.to_localization_map.mk'_self _
 
-@[simp] lemma mk'_self'' {x : M} : f.mk' x.1 x = 1 :=
+lemma mk'_self'' {x : M} : f.mk' x.1 x = 1 :=
 f.mk'_self'
 
 lemma mul_mk'_eq_mk'_of_mul (x y : R) (z : M) :
@@ -940,11 +940,11 @@ def fraction_map_of_algebraic [algebra A L] (alg : is_algebraic A L)
   fraction_map (integral_closure A L) L :=
 (algebra_map (integral_closure A L) L).to_localization_map
   (λ ⟨⟨y, integral⟩, nonzero⟩,
-    have y ≠ 0 := λ h, mem_non_zero_divisors_iff_ne_zero.mp nonzero (subtype.ext.mpr h),
+    have y ≠ 0 := λ h, mem_non_zero_divisors_iff_ne_zero.mp nonzero (subtype.ext_iff_val.mpr h),
     show is_unit y, from ⟨⟨y, y⁻¹, mul_inv_cancel this, inv_mul_cancel this⟩, rfl⟩)
   (λ z, let ⟨x, y, hy, hxy⟩ := exists_integral_multiple (alg z) inj in
     ⟨⟨x, ⟨y, mem_non_zero_divisors_iff_ne_zero.mpr hy⟩⟩, hxy⟩)
-  (λ x y, ⟨ λ (h : x.1 = y.1), ⟨1, by simpa using subtype.ext.mpr h⟩,
+  (λ x y, ⟨ λ (h : x.1 = y.1), ⟨1, by simpa using subtype.ext_iff_val.mpr h⟩,
             λ ⟨c, hc⟩, congr_arg (algebra_map _ L)
               (eq_of_mul_eq_mul_right_of_ne_zero (mem_non_zero_divisors_iff_ne_zero.mp c.2) hc) ⟩)
 
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index a1a65bfa8ad6a..b0f1a334e3b2c 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -340,21 +340,21 @@ lemma well_founded_submodule_gt (R M) [ring R] [add_comm_group M] [module R M] :
 is_noetherian_iff_well_founded.mp
 
 lemma finite_of_linear_independent {R M} [comm_ring R] [nonzero R] [add_comm_group M] [module R M]
-  [is_noetherian R M] {s : set M} (hs : linear_independent R (subtype.val : s → M)) : s.finite :=
+  [is_noetherian R M] {s : set M} (hs : linear_independent R (coe : s → M)) : s.finite :=
 begin
   refine classical.by_contradiction (λ hf, order_embedding.well_founded_iff_no_descending_seq.1
     (well_founded_submodule_gt R M) ⟨_⟩),
   have f : ℕ ↪ s, from @infinite.nat_embedding s ⟨λ f, hf ⟨f⟩⟩,
-  have : ∀ n, (subtype.val ∘ f) '' {m | m ≤ n} ⊆ s,
+  have : ∀ n, (coe ∘ f) '' {m | m ≤ n} ⊆ s,
   { rintros n x ⟨y, hy₁, hy₂⟩, subst hy₂, exact (f y).2 },
   have : ∀ a b : ℕ, a ≤ b ↔
-    span R ((subtype.val ∘ f) '' {m | m ≤ a}) ≤ span R ((subtype.val ∘ f) '' {m | m ≤ b}),
+    span R ((coe ∘ f) '' {m | m ≤ a}) ≤ span R ((coe ∘ f) '' {m | m ≤ b}),
   { assume a b,
     rw [span_le_span_iff zero_ne_one hs (this a) (this b),
-      set.image_subset_image_iff (subtype.val_injective.comp f.injective),
+      set.image_subset_image_iff (subtype.coe_injective.comp f.injective),
       set.subset_def],
     exact ⟨λ hab x (hxa : x ≤ a), le_trans hxa hab, λ hx, hx a (le_refl a)⟩ },
-  exact ⟨⟨λ n, span R ((subtype.val ∘ f) '' {m | m ≤ n}),
+  exact ⟨⟨λ n, span R ((coe ∘ f) '' {m | m ≤ n}),
       λ x y, by simp [le_antisymm_iff, (this _ _).symm] {contextual := tt}⟩,
     by dsimp [gt]; simp only [lt_iff_le_not_le, (this _ _).symm]; tauto⟩
 end
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
index 3a1ea1c95a516..79ac599fc92db 100644
--- a/src/ring_theory/subring.lean
+++ b/src/ring_theory/subring.lean
@@ -64,9 +64,9 @@ instance subtype.comm_ring {S : set cR} [is_subring S] : comm_ring (subtype S) :
 
 instance subring.domain {D : Type*} [integral_domain D] (S : set D) [is_subring S] :
   integral_domain S :=
-{ zero_ne_one := mt subtype.ext.1 zero_ne_one,
+{ zero_ne_one := mt subtype.ext_iff_val.1 zero_ne_one,
   eq_zero_or_eq_zero_of_mul_eq_zero := λ ⟨x, hx⟩ ⟨y, hy⟩,
-    by { simp only [subtype.ext, subtype.coe_mk], exact eq_zero_or_eq_zero_of_mul_eq_zero },
+    by { simp only [subtype.ext_iff_val, subtype.coe_mk], exact eq_zero_or_eq_zero_of_mul_eq_zero },
   .. subset.comm_ring }
 
 instance is_subring.inter (S₁ S₂ : set R) [is_subring S₁] [is_subring S₂] :
diff --git a/src/ring_theory/subsemiring.lean b/src/ring_theory/subsemiring.lean
index 5c81c83106460..dd13e320cd2b6 100644
--- a/src/ring_theory/subsemiring.lean
+++ b/src/ring_theory/subsemiring.lean
@@ -531,7 +531,7 @@ def inclusion {S T : subsemiring R} (h : S ≤ T) : S →* T :=
 S.subtype.cod_srestrict _ (λ x, h x.2)
 
 @[simp] lemma srange_subtype (s : subsemiring R) : s.subtype.srange = s :=
-ext' $ (coe_srange _).trans $ set.range_coe_subtype s
+ext' $ (coe_srange _).trans subtype.range_coe
 
 @[simp]
 lemma range_fst : (fst R S).srange = ⊤ :=
diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean
index 765296d16ce5d..da6d72dd69075 100644
--- a/src/ring_theory/unique_factorization_domain.lean
+++ b/src/ring_theory/unique_factorization_domain.lean
@@ -223,12 +223,12 @@ lemma factor_set.sup_add_inf_eq_add [decidable_eq (associates α)] :
 
 def factor_set.prod : factor_set α → associates α
 | none     := 0
-| (some s) := (s.map subtype.val).prod
+| (some s) := (s.map coe).prod
 
 @[simp] theorem prod_top : (⊤ : factor_set α).prod = 0 := rfl
 
 @[simp] theorem prod_coe {s : multiset { a : associates α // irreducible a }} :
-  (s : factor_set α).prod = (s.map subtype.val).prod :=
+  (s : factor_set α).prod = (s.map coe).prod :=
 rfl
 
 @[simp] theorem prod_add : ∀(a b : factor_set α), (a + b).prod = a.prod * b.prod
@@ -291,8 +291,8 @@ def factors' (a : α) (ha : a ≠ 0) : multiset { a : associates α // irreducib
 (factors a).pmap (λa ha, ⟨associates.mk a, (irreducible_mk_iff _).2 ha⟩)
   (irreducible_factors $ ha)
 
-@[simp] theorem map_subtype_val_factors' {a : α} (ha : a ≠ 0) :
-  (factors' a ha).map subtype.val = (factors a).map associates.mk :=
+@[simp] theorem map_subtype_coe_factors' {a : α} (ha : a ≠ 0) :
+  (factors' a ha).map coe = (factors a).map associates.mk :=
 by simp [factors', multiset.map_pmap, multiset.pmap_eq_map]
 
 theorem factors'_cong {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : a ~ᵤ b) :
@@ -300,7 +300,7 @@ theorem factors'_cong {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : a ~ᵤ b) :
 have multiset.rel associated (factors a) (factors b), from
   unique (irreducible_factors ha) (irreducible_factors hb)
     ((factors_prod ha).trans $ h.trans $ (factors_prod hb).symm),
-by simpa [(multiset.map_eq_map subtype.val_injective).symm, rel_associated_iff_map_eq_map.symm]
+by simpa [(multiset.map_eq_map subtype.coe_injective).symm, rel_associated_iff_map_eq_map.symm]
 
 variable [dec : decidable_eq (associates α)]
 include dec
@@ -329,19 +329,19 @@ theorem prod_factors : ∀(s : factor_set α), s.prod.factors = s
 | (some s) :=
   begin
     unfold factor_set.prod,
-    generalize eq_a : (s.map subtype.val).prod = a,
+    generalize eq_a : (s.map coe).prod = a,
     rcases a with ⟨a⟩,
     rw quot_mk_eq_mk at *,
 
-    have : (s.map subtype.val).prod ≠ 0, from assume ha,
+    have : (s.map (coe : _ → associates α)).prod ≠ 0, from assume ha,
       let ⟨⟨a, ha⟩, h, eq⟩ := multiset.mem_map.1 (prod_eq_zero_iff.1 ha) in
       have irreducible (0 : associates α), from eq ▸ ha,
       not_irreducible_zero ((irreducible_mk_iff _).1 this),
     have ha : a ≠ 0, by simp [*] at *,
-    suffices : (unique_factorization_domain.factors a).map associates.mk = s.map subtype.val,
+    suffices : (unique_factorization_domain.factors a).map associates.mk = s.map coe,
     { rw [factors_mk a ha],
       apply congr_arg some _,
-      simpa [(multiset.map_eq_map subtype.val_injective).symm] },
+      simpa [(multiset.map_eq_map subtype.coe_injective).symm] },
 
     refine unique'
       (forall_map_mk_factors_irreducible _ ha)
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index 8a3a1b4705f01..23f4803584eeb 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -3174,9 +3174,9 @@ lemma mk_bounded_subset_le {α : Type u} (s : set α) (c : cardinal.{u}) :
 begin
   refine le_trans _ (mk_bounded_set_le s c),
   refine ⟨embedding.cod_restrict _ _ _⟩,
-  use λ t, subtype.val ⁻¹' t.1,
+  use λ t, coe ⁻¹' t.1,
   { rintros ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h, apply subtype.eq, dsimp only at h ⊢,
-    refine (preimage_eq_preimage' _ _).1 h; rw [subtype.range_val]; assumption },
+    refine (preimage_eq_preimage' _ _).1 h; rw [subtype.range_coe]; assumption },
   rintro ⟨t, h1t, h2t⟩, exact le_trans (mk_preimage_of_injective _ _ subtype.val_injective) h2t
 end
 
diff --git a/src/tactic/subtype_instance.lean b/src/tactic/subtype_instance.lean
index 16421e76a6a76..2e67e74b1d7a3 100644
--- a/src/tactic/subtype_instance.lean
+++ b/src/tactic/subtype_instance.lean
@@ -25,7 +25,7 @@ do
   field ← get_current_field,
   b ← target >>= is_prop,
   if b then  do
-    `[simp [subtype.ext], dsimp [set.set_coe_eq_subtype]],
+    `[simp [subtype.ext_iff_val], dsimp [set.set_coe_eq_subtype]],
     intros,
     applyc field; assumption
   else do
diff --git a/src/topology/algebra/module.lean b/src/topology/algebra/module.lean
index 8f4588005612e..2d8dbc6c11bfb 100644
--- a/src/topology/algebra/module.lean
+++ b/src/topology/algebra/module.lean
@@ -548,12 +548,12 @@ rfl
 @[simp] lemma proj_ker_of_right_inverse_apply_idem [topological_add_group M]
   (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (x : f₁.ker) :
   f₁.proj_ker_of_right_inverse f₂ h x = x :=
-subtype.coe_ext.2 $ by simp
+subtype.ext_iff_val.2 $ by simp
 
 @[simp] lemma proj_ker_of_right_inverse_comp_inv [topological_add_group M]
   (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (y : M₂) :
   f₁.proj_ker_of_right_inverse f₂ h (f₂ y) = 0 :=
-subtype.coe_ext.2 $ by simp [h y]
+subtype.ext_iff_val.2 $ by simp [h y]
 
 end ring
 
@@ -918,7 +918,7 @@ end
 ⟨0, λ x, by simp only [zero_apply, eq_zero_of_bot_submodule x]⟩
 
 @[simp] lemma closed_complemented_top : closed_complemented (⊤ : submodule R M) :=
-⟨(id R M).cod_restrict ⊤ (λ x, trivial), λ x, subtype.coe_ext.2 $ by simp⟩
+⟨(id R M).cod_restrict ⊤ (λ x, trivial), λ x, subtype.ext_iff_val.2 $ by simp⟩
 
 end submodule
 
diff --git a/src/topology/category/Top/opens.lean b/src/topology/category/Top/opens.lean
index 96630bf1f97f3..1def8a7a375c1 100644
--- a/src/topology/category/Top/opens.lean
+++ b/src/topology/category/Top/opens.lean
@@ -24,7 +24,7 @@ instance opens_category : category.{u} (opens X) :=
 def to_Top (X : Top.{u}) : opens X ⥤ Top :=
 { obj := λ U, ⟨U.val, infer_instance⟩,
   map := λ U V i, ⟨λ x, ⟨x.1, i.down.down x.2⟩,
-    (embedding.continuous_iff embedding_subtype_val).2 continuous_induced_dom⟩ }
+    (embedding.continuous_iff embedding_subtype_coe).2 continuous_induced_dom⟩ }
 
 /-- `opens.map f` gives the functor from open sets in Y to open set in X,
     given by taking preimages under f. -/
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index 41349c53af227..df7fee9a5d4f2 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -80,7 +80,7 @@ end
 instance {p : α → Prop} [topological_space α] [discrete_topology α] :
   discrete_topology (subtype p) :=
 ⟨bot_unique $ assume s hs,
-  ⟨subtype.val '' s, is_open_discrete _, (set.preimage_image_eq _ subtype.val_injective)⟩⟩
+  ⟨coe '' s, is_open_discrete _, (set.preimage_image_eq _ subtype.coe_injective)⟩⟩
 
 instance sum.discrete_topology [topological_space α] [topological_space β]
   [hα : discrete_topology α] [hβ : discrete_topology β] : discrete_topology (α ⊕ β) :=
@@ -99,12 +99,12 @@ The 𝓝 filter and the subspace topology.
 -/
 
 theorem mem_nhds_subtype (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
-  t ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 a.val, (@subtype.val α s) ⁻¹' u ⊆ t :=
-mem_nhds_induced subtype.val a t
+  t ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (a : α), coe ⁻¹' u ⊆ t :=
+mem_nhds_induced coe a t
 
 theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
-  𝓝 a = comap subtype.val (𝓝 a.val) :=
-nhds_induced subtype.val a
+  𝓝 a = comap coe (𝓝 (a : α)) :=
+nhds_induced coe a
 
 end topα
 
@@ -438,8 +438,8 @@ end sum
 section subtype
 variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop}
 
-lemma embedding_subtype_val : embedding (@subtype.val α p) :=
-⟨⟨rfl⟩, subtype.val_injective⟩
+lemma embedding_subtype_coe : embedding (coe : subtype p → α) :=
+⟨⟨rfl⟩, subtype.coe_injective⟩
 
 lemma continuous_subtype_val : continuous (@subtype.val α p) :=
 continuous_induced_dom
@@ -447,90 +447,90 @@ continuous_induced_dom
 lemma continuous_subtype_coe : continuous (coe : subtype p → α) :=
 continuous_subtype_val
 
-lemma is_open.open_embedding_subtype_val {s : set α} (hs : is_open s) :
-  open_embedding (subtype.val : s → α) :=
+lemma is_open.open_embedding_subtype_coe {s : set α} (hs : is_open s) :
+  open_embedding (coe : s → α) :=
 { induced := rfl,
-  inj := subtype.val_injective,
-  open_range := (subtype.val_range : range subtype.val = s).symm ▸  hs }
+  inj := subtype.coe_injective,
+  open_range := (subtype.range_coe : range coe = s).symm ▸  hs }
 
-lemma is_open.is_open_map_subtype_val {s : set α} (hs : is_open s) :
-  is_open_map (subtype.val : s → α) :=
-hs.open_embedding_subtype_val.is_open_map
+lemma is_open.is_open_map_subtype_coe {s : set α} (hs : is_open s) :
+  is_open_map (coe : s → α) :=
+hs.open_embedding_subtype_coe.is_open_map
 
 lemma is_open_map.restrict {f : α → β} (hf : is_open_map f) {s : set α} (hs : is_open s) :
   is_open_map (s.restrict f) :=
-hf.comp hs.is_open_map_subtype_val
+hf.comp hs.is_open_map_subtype_coe
 
-lemma is_closed.closed_embedding_subtype_val {s : set α} (hs : is_closed s) :
-  closed_embedding (subtype.val : {x // x ∈ s} → α) :=
+lemma is_closed.closed_embedding_subtype_coe {s : set α} (hs : is_closed s) :
+  closed_embedding (coe : {x // x ∈ s} → α) :=
 { induced := rfl,
-  inj := subtype.val_injective,
-  closed_range := (subtype.val_range : range subtype.val = s).symm ▸ hs }
+  inj := subtype.coe_injective,
+  closed_range := (subtype.range_coe : range coe = s).symm ▸ hs }
 
 lemma continuous_subtype_mk {f : β → α}
   (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
 continuous_induced_rng h
 
 lemma continuous_inclusion {s t : set α} (h : s ⊆ t) : continuous (inclusion h) :=
-continuous_subtype_mk _ continuous_subtype_val
+continuous_subtype_mk _ continuous_subtype_coe
 
-lemma continuous_at_subtype_val {p : α → Prop} {a : subtype p} :
-  continuous_at subtype.val a :=
-continuous_iff_continuous_at.mp continuous_subtype_val _
+lemma continuous_at_subtype_coe {p : α → Prop} {a : subtype p} :
+  continuous_at (coe : subtype p → α) a :=
+continuous_iff_continuous_at.mp continuous_subtype_coe _
 
-lemma map_nhds_subtype_val_eq {a : α} (ha : p a) (h : {a | p a} ∈ 𝓝 a) :
-  map (@subtype.val α p) (𝓝 ⟨a, ha⟩) = 𝓝 a :=
-map_nhds_induced_eq (by simp [subtype.val_image, h])
+lemma map_nhds_subtype_coe_eq {a : α} (ha : p a) (h : {a | p a} ∈ 𝓝 a) :
+  map (coe : subtype p → α) (𝓝 ⟨a, ha⟩) = 𝓝 a :=
+map_nhds_induced_eq $ by simpa only [subtype.coe_mk, subtype.range_coe] using h
 
 lemma nhds_subtype_eq_comap {a : α} {h : p a} :
-  𝓝 (⟨a, h⟩ : subtype p) = comap subtype.val (𝓝 a) :=
+  𝓝 (⟨a, h⟩ : subtype p) = comap coe (𝓝 a) :=
 nhds_induced _ _
 
 lemma tendsto_subtype_rng {β : Type*} {p : α → Prop} {b : filter β} {f : β → subtype p} :
-  ∀{a:subtype p}, tendsto f b (𝓝 a) ↔ tendsto (λx, subtype.val (f x)) b (𝓝 a.val)
-| ⟨a, ha⟩ := by rw [nhds_subtype_eq_comap, tendsto_comap_iff]
+  ∀{a:subtype p}, tendsto f b (𝓝 a) ↔ tendsto (λx, (f x : α)) b (𝓝 (a : α))
+| ⟨a, ha⟩ := by rw [nhds_subtype_eq_comap, tendsto_comap_iff, subtype.coe_mk]
 
 lemma continuous_subtype_nhds_cover {ι : Sort*} {f : α → β} {c : ι → α → Prop}
   (c_cover : ∀x:α, ∃i, {x | c i x} ∈ 𝓝 x)
-  (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
+  (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x)) :
   continuous f :=
 continuous_iff_continuous_at.mpr $ assume x,
   let ⟨i, (c_sets : {x | c i x} ∈ 𝓝 x)⟩ := c_cover x in
   let x' : subtype (c i) := ⟨x, mem_of_nhds c_sets⟩ in
-  calc map f (𝓝 x) = map f (map subtype.val (𝓝 x')) :
-      congr_arg (map f) (map_nhds_subtype_val_eq _ $ c_sets).symm
-    ... = map (λx:subtype (c i), f x.val) (𝓝 x') : rfl
+  calc map f (𝓝 x) = map f (map coe (𝓝 x')) :
+      congr_arg (map f) (map_nhds_subtype_coe_eq _ $ c_sets).symm
+    ... = map (λx:subtype (c i), f x) (𝓝 x') : rfl
     ... ≤ 𝓝 (f x) : continuous_iff_continuous_at.mp (f_cont i) x'
 
 lemma continuous_subtype_is_closed_cover {ι : Sort*} {f : α → β} (c : ι → α → Prop)
   (h_lf : locally_finite (λi, {x | c i x}))
   (h_is_closed : ∀i, is_closed {x | c i x})
   (h_cover : ∀x, ∃i, c i x)
-  (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
+  (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x)) :
   continuous f :=
 continuous_iff_is_closed.mpr $
   assume s hs,
-  have ∀i, is_closed (@subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
+  have ∀i, is_closed ((coe : {x | c i x} → α) '' (f ∘ coe ⁻¹' s)),
     from assume i,
-    embedding_is_closed embedding_subtype_val
-      (by simp [subtype.val_range]; exact h_is_closed i)
+    embedding_is_closed embedding_subtype_coe
+      (by simp [subtype.range_coe]; exact h_is_closed i)
       (continuous_iff_is_closed.mp (f_cont i) _ hs),
-  have is_closed (⋃i, @subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
+  have is_closed (⋃i, (coe : {x | c i x} → α) '' (f ∘ coe ⁻¹' s)),
     from is_closed_Union_of_locally_finite
       (locally_finite_subset h_lf $ assume i x ⟨⟨x', hx'⟩, _, heq⟩, heq ▸ hx')
       this,
-  have f ⁻¹' s = (⋃i, @subtype.val α {x | c i x} '' (f ∘ subtype.val ⁻¹' s)),
+  have f ⁻¹' s = (⋃i, (coe : {x | c i x} → α) '' (f ∘ coe ⁻¹' s)),
   begin
     apply set.ext,
     have : ∀ (x : α), f x ∈ s ↔ ∃ (i : ι), c i x ∧ f x ∈ s :=
       λ x, ⟨λ hx, let ⟨i, hi⟩ := h_cover x in ⟨i, hi, hx⟩,
             λ ⟨i, hi, hx⟩, hx⟩,
-    simp [and.comm, and.left_comm], simpa [(∘)],
+    simpa [and.comm, @and.left_comm (c _ _), ← exists_and_distrib_right],
   end,
   by rwa [this]
 
 lemma closure_subtype {x : {a // p a}} {s : set {a // p a}}:
-  x ∈ closure s ↔ x.val ∈ closure (subtype.val '' s) :=
+  x ∈ closure s ↔ (x : α) ∈ closure ((coe : _ → α) '' s) :=
 closure_induced $ assume x y, subtype.eq
 
 end subtype
diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean
index baeac779e2677..d900b31a04991 100644
--- a/src/topology/continuous_on.lean
+++ b/src/topology/continuous_on.lean
@@ -169,8 +169,8 @@ theorem tendsto_nhds_within_of_tendsto_nhds {f : α → β} {a : α}
 by rw [←nhds_within_univ] at h; exact tendsto_nhds_within_mono_left (set.subset_univ _) h
 
 theorem principal_subtype {α : Type*} (s : set α) (t : set {x // x ∈ s}) :
-  𝓟 t = comap subtype.val (𝓟 (subtype.val '' t)) :=
-by rw comap_principal; rw set.preimage_image_eq; apply subtype.val_injective
+  𝓟 t = comap coe (𝓟 ((coe : s → α) '' t)) :=
+by rw comap_principal; rw set.preimage_image_eq; apply subtype.coe_injective
 
 lemma mem_closure_iff_nhds_within_ne_bot {s : set α} {x : α} :
   x ∈ closure s ↔ nhds_within x s ≠ ⊥ :=
@@ -190,27 +190,27 @@ nhds_within and subtypes
 
 theorem mem_nhds_within_subtype (s : set α) (a : {x // x ∈ s}) (t u : set {x // x ∈ s}) :
   t ∈ nhds_within a u ↔
-    t ∈ comap (@subtype.val _ s) (nhds_within a.val (subtype.val '' u)) :=
+    t ∈ comap (coe : s → α) (nhds_within a (coe '' u)) :=
 by rw [nhds_within, nhds_subtype, principal_subtype, ←comap_inf, ←nhds_within]
 
 theorem nhds_within_subtype (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
-  nhds_within a t = comap (@subtype.val _ s) (nhds_within a.val (subtype.val '' t)) :=
+  nhds_within a t = comap (coe : s → α) (nhds_within a (coe '' t)) :=
 filter_eq $ by ext u; rw mem_nhds_within_subtype
 
-theorem nhds_within_eq_map_subtype_val {s : set α} {a : α} (h : a ∈ s) :
-  nhds_within a s = map subtype.val (𝓝 ⟨a, h⟩) :=
+theorem nhds_within_eq_map_subtype_coe {s : set α} {a : α} (h : a ∈ s) :
+  nhds_within a s = map (coe : s → α) (𝓝 ⟨a, h⟩) :=
 have h₀ : s ∈ nhds_within a s,
   by { rw [mem_nhds_within], existsi set.univ, simp [set.diff_eq] },
-have h₁ : ∀ y ∈ s, ∃ x, @subtype.val _ s x = y,
+have h₁ : ∀ y ∈ s, ∃ x : s, ↑x = y,
   from λ y h, ⟨⟨y, h⟩, rfl⟩,
 begin
-  rw [←nhds_within_univ, nhds_within_subtype, subtype.val_image_univ],
+  rw [←nhds_within_univ, nhds_within_subtype, subtype.coe_image_univ],
   exact (map_comap_of_surjective' h₀ h₁).symm,
 end
 
 theorem tendsto_nhds_within_iff_subtype {s : set α} {a : α} (h : a ∈ s) (f : α → β) (l : filter β) :
   tendsto f (nhds_within a s) l ↔ tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l :=
-by { simp only [tendsto, nhds_within_eq_map_subtype_val h, filter.map_map], refl }
+by { simp only [tendsto, nhds_within_eq_map_subtype_coe h, filter.map_map], refl }
 
 variables [topological_space β] [topological_space γ] [topological_space δ]
 
@@ -279,7 +279,7 @@ have ∀ t, is_open (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_open u ∧
   begin
     intro t,
     rw [is_open_induced_iff, set.restrict_eq, set.preimage_comp],
-    simp only [preimage_coe_eq_preimage_coe_iff],
+    simp only [subtype.preimage_coe_eq_preimage_coe_iff],
     split; { rintros ⟨u, ou, useq⟩, exact ⟨u, ou, useq.symm⟩ }
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous]; simp only [this]
@@ -290,7 +290,7 @@ have ∀ t, is_closed (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_closed u
   begin
     intro t,
     rw [is_closed_induced_iff, set.restrict_eq, set.preimage_comp],
-    simp only [preimage_coe_eq_preimage_coe_iff]
+    simp only [subtype.preimage_coe_eq_preimage_coe_iff]
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous_iff_is_closed]; simp only [this]
 
@@ -357,7 +357,7 @@ begin
   replace h := h.nhds_le ⟨x, xs⟩,
   apply mem_nhds_within_of_mem_nhds,
   apply h,
-  erw [map_compose.symm, function.comp, mem_map, ← nhds_within_eq_map_subtype_val],
+  erw [map_compose.symm, function.comp, mem_map, ← nhds_within_eq_map_subtype_coe],
   apply mem_sets_of_superset (inter_mem_nhds_within _ ht),
   assume y hy,
   rw [mem_set_of_eq, mem_preimage, hleft hy.1],
diff --git a/src/topology/dense_embedding.lean b/src/topology/dense_embedding.lean
index 6d3bcb439b858..c115942a113c8 100644
--- a/src/topology/dense_embedding.lean
+++ b/src/topology/dense_embedding.lean
@@ -262,16 +262,16 @@ protected lemma prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_embedd
 /-- The dense embedding of a subtype inside its closure. -/
 def subtype_emb {α : Type*} (p : α → Prop) (e : α → β) (x : {x // p x}) :
   {x // x ∈ closure (e '' {x | p x})} :=
-⟨e x.1, subset_closure $ mem_image_of_mem e x.2⟩
+⟨e x, subset_closure $ mem_image_of_mem e x.prop⟩
 
 protected lemma subtype (p : α → Prop) : dense_embedding (subtype_emb p e) :=
 { dense_embedding .
   dense   := assume ⟨x, hx⟩, closure_subtype.mpr $
-    have (λ (x : {x // p x}), e (x.val)) = e ∘ subtype.val, from rfl,
+    have (λ (x : {x // p x}), e x) = e ∘ coe, from rfl,
     begin
       rw ← image_univ,
       simp [(image_comp _ _ _).symm, (∘), subtype_emb, -image_univ],
-      rw [this, image_comp, subtype.val_image],
+      rw [this, image_comp, subtype.coe_image],
       simp,
       assumption
     end,
diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean
index bfe1418b22b0e..ddfdda24dd0be 100644
--- a/src/topology/instances/ennreal.lean
+++ b/src/topology/instances/ennreal.lean
@@ -112,7 +112,7 @@ end
 
 lemma continuous_on_to_nnreal : continuous_on ennreal.to_nnreal {a | a ≠ ∞}  :=
 continuous_on_iff_continuous_restrict.2 $ continuous_iff_continuous_at.2 $ λ x,
-  (tendsto_to_nnreal x.2).comp continuous_at_subtype_val
+  (tendsto_to_nnreal x.2).comp continuous_at_subtype_coe
 
 lemma tendsto_to_real {a : ennreal} : a ≠ ⊤ → tendsto (ennreal.to_real) (𝓝 a) (𝓝 a.to_real) :=
 λ ha, tendsto.comp ((@nnreal.tendsto_coe _ (𝓝 a.to_nnreal) id (a.to_nnreal)).2 tendsto_id)
@@ -652,7 +652,7 @@ local attribute [instance] metric_space_emetric_ball
 
 lemma nhds_eq_nhds_emetric_ball (a x : β) (r : ennreal) (h : x ∈ ball a r) :
   𝓝 x = map (coe : ball a r → β) (𝓝 ⟨x, h⟩) :=
-(map_nhds_subtype_val_eq _ $ mem_nhds_sets emetric.is_open_ball h).symm
+(map_nhds_subtype_coe_eq _ $ mem_nhds_sets emetric.is_open_ball h).symm
 end
 
 section
diff --git a/src/topology/list.lean b/src/topology/list.lean
index b1764cd487ec8..04ceebda3bf08 100644
--- a/src/topology/list.lean
+++ b/src/topology/list.lean
@@ -151,9 +151,8 @@ by unfold vector; apply_instance
 
 lemma tendsto_cons [topological_space α] {n : ℕ} {a : α} {l : vector α n}:
   tendsto (λp:α×vector α n, vector.cons p.1 p.2) ((𝓝 a).prod (𝓝 l)) (𝓝 (a :: l)) :=
-by
-  simp [tendsto_subtype_rng, cons_val];
-  exact tendsto_cons tendsto_fst (tendsto.comp continuous_at_subtype_val tendsto_snd)
+by { simp [tendsto_subtype_rng, ←subtype.val_eq_coe, cons_val],
+  exact tendsto_cons tendsto_fst (tendsto.comp continuous_at_subtype_coe tendsto_snd) }
 
 lemma tendsto_insert_nth
   [topological_space α] {n : ℕ} {i : fin (n+1)} {a:α} :
@@ -163,7 +162,7 @@ lemma tendsto_insert_nth
 begin
   rw [insert_nth, tendsto_subtype_rng],
   simp [insert_nth_val],
-  exact list.tendsto_insert_nth tendsto_fst (tendsto.comp continuous_at_subtype_val tendsto_snd : _)
+  exact list.tendsto_insert_nth tendsto_fst (tendsto.comp continuous_at_subtype_coe tendsto_snd : _)
 end
 
 lemma continuous_insert_nth' [topological_space α] {n : ℕ} {i : fin (n+1)} :
@@ -183,8 +182,8 @@ lemma continuous_at_remove_nth [topological_space α] {n : ℕ} {i : fin (n+1)}
 --| ⟨l, hl⟩ :=
 begin
   rw [continuous_at, remove_nth, tendsto_subtype_rng],
-  simp [remove_nth_val],
-  exact tendsto.comp list.tendsto_remove_nth continuous_at_subtype_val
+  simp [remove_nth_val, ← subtype.val_eq_coe],
+  exact tendsto.comp list.tendsto_remove_nth continuous_at_subtype_coe
 end
 
 lemma continuous_remove_nth [topological_space α] {n : ℕ} {i : fin (n+1)} :
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 8e9e15ea0cb58..3d81fc55c78f9 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -977,7 +977,7 @@ def metric_space.induced {α β} (f : α → β) (hf : function.injective f)
 
 instance subtype.metric_space {α : Type*} {p : α → Prop} [t : metric_space α] :
   metric_space (subtype p) :=
-metric_space.induced coe (λ x y, subtype.coe_ext.2) t
+metric_space.induced coe (λ x y, subtype.ext) t
 
 theorem subtype.dist_eq {p : α → Prop} (x y : subtype p) : dist x y = dist (x : α) y := rfl
 
diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean
index ed00e10cbeb85..51db46eb5b21c 100644
--- a/src/topology/metric_space/closeds.lean
+++ b/src/topology/metric_space/closeds.lean
@@ -53,7 +53,7 @@ begin
   ... ≤ (inf_edist y (t.val) + edist x y) + Hausdorff_edist (t.val) (s.val) :
     add_le_add_right' inf_edist_le_inf_edist_add_edist
   ... = inf_edist y (t.val) + (edist x y + Hausdorff_edist (s.val) (t.val)) :
-    by simp [add_comm, add_left_comm, Hausdorff_edist_comm]
+    by simp [add_comm, add_left_comm, Hausdorff_edist_comm, -subtype.val_eq_coe]
   ... ≤ inf_edist y (t.val) + (edist (x, s) (y, t) + edist (x, s) (y, t)) :
     add_le_add_left' (add_le_add (by simp [edist, le_refl]) (by simp [edist, le_refl]))
   ... = inf_edist y (t.val) + 2 * edist (x, s) (y, t) :
diff --git a/src/topology/metric_space/contracting.lean b/src/topology/metric_space/contracting.lean
index 1b6da62d7e2a2..d7c1b89460515 100644
--- a/src/topology/metric_space/contracting.lean
+++ b/src/topology/metric_space/contracting.lean
@@ -156,7 +156,7 @@ theorem exists_fixed_point' {s : set α} (hsc : is_complete s) (hsf : maps_to f
 begin
   haveI := hsc.complete_space_coe,
   rcases hf.exists_fixed_point ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩,
-  refine ⟨y, y.2, subtype.ext.1 hfy, _, λ n, _⟩,
+  refine ⟨y, y.2, subtype.ext_iff_val.1 hfy, _, λ n, _⟩,
   { convert (continuous_subtype_coe.tendsto _).comp h_tendsto, ext n,
     simp only [(∘), maps_to.iterate_restrict, maps_to.coe_restrict_apply, subtype.coe_mk] },
   { convert hle n,
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
index ea07119b797a8..84b15ebd54e0a 100644
--- a/src/topology/metric_space/emetric_space.lean
+++ b/src/topology/metric_space/emetric_space.lean
@@ -418,7 +418,7 @@ def emetric_space.induced {α β} (f : α → β) (hf : function.injective f)
 
 /-- Emetric space instance on subsets of emetric spaces -/
 instance {α : Type*} {p : α → Prop} [t : emetric_space α] : emetric_space (subtype p) :=
-t.induced coe (λ x y, subtype.coe_ext.2)
+t.induced coe (λ x y, subtype.ext_iff_val.2)
 
 /-- The extended distance on a subset of an emetric space is the restriction of
 the original distance, by definition -/
diff --git a/src/topology/metric_space/gromov_hausdorff.lean b/src/topology/metric_space/gromov_hausdorff.lean
index 363b944d0575f..89684aa60ce0e 100644
--- a/src/topology/metric_space/gromov_hausdorff.lean
+++ b/src/topology/metric_space/gromov_hausdorff.lean
@@ -91,8 +91,8 @@ begin
     have f := (Kuratowski_embedding.isometry α).isometric_on_range.trans e,
     use λx, f x,
     split,
-    { apply isometry_subtype_val.comp f.isometry },
-    { rw [range_comp, f.range_coe, set.image_univ, set.range_coe_subtype] } },
+    { apply isometry_subtype_coe.comp f.isometry },
+    { rw [range_comp, f.range_coe, set.image_univ, subtype.range_coe] } },
   { rintros ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩,
     have f := ((Kuratowski_embedding.isometry α).isometric_on_range.symm.trans
                isomΨ.isometric_on_range).symm,
@@ -104,8 +104,8 @@ end
 
 lemma eq_to_GH_space {p : nonempty_compacts ℓ_infty_ℝ} : ⟦p⟧ = to_GH_space p.val :=
 begin
- refine eq_to_GH_space_iff.2 ⟨((λx, x) : p.val → ℓ_infty_ℝ), _, subtype.val_range⟩,
- apply isometry_subtype_val
+ refine eq_to_GH_space_iff.2 ⟨((λx, x) : p.val → ℓ_infty_ℝ), _, subtype.range_coe⟩,
+ apply isometry_subtype_coe
 end
 
 section
@@ -200,7 +200,7 @@ begin
   have ΨΨ' : Ψ = subtype.val ∘ Ψ', by { funext, refl },
   have : Hausdorff_dist (range Φ) (range Ψ) = Hausdorff_dist (range Φ') (range Ψ'),
   { rw [ΦΦ', ΨΨ', range_comp, range_comp],
-    exact Hausdorff_dist_image (isometry_subtype_val) },
+    exact Hausdorff_dist_image (isometry_subtype_coe) },
   rw this,
   -- Embed `s` in `ℓ^∞(ℝ)` through its Kuratowski embedding
   let F := Kuratowski_embedding (subtype s),
@@ -480,11 +480,11 @@ variables {α : Type u} [metric_space α]
 theorem GH_dist_le_nonempty_compacts_dist (p q : nonempty_compacts α) :
   dist p.to_GH_space q.to_GH_space ≤ dist p q :=
 begin
-  have ha : isometry (subtype.val : p.val → α) := isometry_subtype_val,
-  have hb : isometry (subtype.val : q.val → α) := isometry_subtype_val,
+  have ha : isometry (coe : p.val → α) := isometry_subtype_coe,
+  have hb : isometry (coe : q.val → α) := isometry_subtype_coe,
   have A : dist p q = Hausdorff_dist p.val q.val := rfl,
-  have I : p.val = range (subtype.val : p.val → α), by simp,
-  have J : q.val = range (subtype.val : q.val → α), by simp,
+  have I : p.val = range (coe : p.val → α), by simp,
+  have J : q.val = range (coe : q.val → α), by simp,
   rw [I, J] at A,
   rw A,
   exact GH_dist_le_Hausdorff_dist ha hb
diff --git a/src/topology/metric_space/isometry.lean b/src/topology/metric_space/isometry.lean
index ad16eda6a8088..c8571eaed8994 100644
--- a/src/topology/metric_space/isometry.lean
+++ b/src/topology/metric_space/isometry.lean
@@ -96,7 +96,7 @@ lemma isometry.ediam_range (hf : isometry f) :
 by { rw ← image_univ, exact hf.ediam_image univ }
 
 /-- The injection from a subtype is an isometry -/
-lemma isometry_subtype_val {s : set α} : isometry (subtype.val : s → α) :=
+lemma isometry_subtype_coe {s : set α} : isometry (coe : s → α) :=
 λx y, rfl
 
 end emetric_isometry --section
diff --git a/src/topology/opens.lean b/src/topology/opens.lean
index 3c318a8c1227e..a8097fe14e90e 100644
--- a/src/topology/opens.lean
+++ b/src/topology/opens.lean
@@ -50,7 +50,7 @@ instance : has_subset (opens α) :=
 instance : has_mem α (opens α) :=
 { mem := λ a U, a ∈ U.val }
 
-@[ext] lemma ext {U V : opens α} (h : U.val = V.val) : U = V := subtype.ext.mpr h
+@[ext] lemma ext {U V : opens α} (h : U.val = V.val) : U = V := subtype.ext_iff_val.mpr h
 
 instance : partial_order (opens α) := subtype.partial_order _
 
@@ -73,13 +73,13 @@ complete_lattice.copy
   (@galois_insertion.lift_complete_lattice
     (order_dual (set α)) (order_dual (opens α)) interior (subtype.val : opens α → set α) _ _ gi))
 /- le  -/ (λ U V, U.1 ⊆ V.1) rfl
-/- top -/ ⟨set.univ, is_open_univ⟩ (subtype.ext.mpr interior_univ.symm)
+/- top -/ ⟨set.univ, is_open_univ⟩ (subtype.ext_iff_val.mpr interior_univ.symm)
 /- bot -/ ⟨∅, is_open_empty⟩ rfl
 /- sup -/ (λ U V, ⟨U.1 ∪ V.1, is_open_union U.2 V.2⟩) rfl
 /- inf -/ (λ U V, ⟨U.1 ∩ V.1, is_open_inter U.2 V.2⟩)
 begin
   funext,
-  apply subtype.ext.mpr,
+  apply subtype.ext_iff_val.mpr,
   symmetry,
   apply interior_eq_of_open,
   exact (is_open_inter U.2 V.2),
@@ -88,7 +88,7 @@ end
 by { rcases hU with ⟨⟨V, hV⟩, h, h'⟩, dsimp at h', subst h', exact hV}⟩)
 begin
   funext,
-  apply subtype.ext.mpr,
+  apply subtype.ext_iff_val.mpr,
   simp [Sup_range],
   refl,
 end
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index 43e5118677f8a..54ca013db2362 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -53,7 +53,7 @@ begin
 end
 
 instance subtype.t0_space [t0_space α] {p : α → Prop} : t0_space (subtype p) :=
-⟨λ x y hxy, let ⟨U, hU, hxyU⟩ := t0_space.t0 (x:α) y ((not_congr subtype.coe_ext).1 hxy) in
+⟨λ x y hxy, let ⟨U, hU, hxyU⟩ := t0_space.t0 (x:α) y ((not_congr subtype.ext_iff_val).1 hxy) in
   ⟨(coe : subtype p → α) ⁻¹' U, is_open_induced hU, hxyU⟩⟩
 
 /-- A T₁ space, also known as a Fréchet space, is a topological space
@@ -71,7 +71,7 @@ compl_singleton_eq x ▸ is_open_compl_iff.2 (t1_space.t1 x)
 instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :
   t1_space (subtype p) :=
 ⟨λ ⟨x, hx⟩, is_closed_induced_iff.2 $ ⟨{x}, is_closed_singleton, set.ext $ λ y,
-  by simp [subtype.coe_ext]⟩⟩
+  by simp [subtype.ext_iff_val]⟩⟩
 
 @[priority 100] -- see Note [lower instance priority]
 instance t1_space.t0_space [t1_space α] : t0_space α :=
diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean
index 6afcbbc8c4ade..7cedf34855e0f 100644
--- a/src/topology/subset_properties.lean
+++ b/src/topology/subset_properties.lean
@@ -457,11 +457,11 @@ iff.intro (assume h, h.image hf.continuous) $ assume h, begin
 end
 
 lemma compact_iff_compact_in_subtype {p : α → Prop} {s : set {a // p a}} :
-  compact s ↔ compact (subtype.val '' s) :=
-embedding_subtype_val.compact_iff_compact_image
+  compact s ↔ compact ((coe : _ → α) '' s) :=
+embedding_subtype_coe.compact_iff_compact_image
 
-lemma compact_iff_compact_univ {s : set α} : compact s ↔ compact (univ : set (subtype s)) :=
-by rw [compact_iff_compact_in_subtype, image_univ, subtype.val_range]; refl
+lemma compact_iff_compact_univ {s : set α} : compact s ↔ compact (univ : set s) :=
+by rw [compact_iff_compact_in_subtype, image_univ, subtype.range_coe]; refl
 
 lemma compact_iff_compact_space {s : set α} : compact s ↔ compact_space s :=
 compact_iff_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.compact_univ _ _⟩
diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean
index 19057b968a9d9..746d5c8148fea 100644
--- a/src/topology/uniform_space/basic.lean
+++ b/src/topology/uniform_space/basic.lean
@@ -1137,7 +1137,7 @@ lemma tendsto_of_uniform_continuous_subtype
   [uniform_space α] [uniform_space β] {f : α → β} {s : set α} {a : α}
   (hf : uniform_continuous (λx:s, f x.val)) (ha : s ∈ 𝓝 a) :
   tendsto f (𝓝 a) (𝓝 (f a)) :=
-by rw [(@map_nhds_subtype_val_eq α _ s a (mem_of_nhds ha) ha).symm]; exact
+by rw [(@map_nhds_subtype_coe_eq α _ s a (mem_of_nhds ha) ha).symm]; exact
 tendsto_map' (continuous_iff_continuous_at.mp hf.continuous _)
 
 
diff --git a/src/topology/uniform_space/completion.lean b/src/topology/uniform_space/completion.lean
index bf31b95032e66..fe11bdcdf216e 100644
--- a/src/topology/uniform_space/completion.lean
+++ b/src/topology/uniform_space/completion.lean
@@ -69,7 +69,7 @@ calc map prod.swap ((𝓤 α).lift' gen) =
   begin
     delta gen,
     simp [map_lift'_eq, monotone_set_of, monotone_mem_sets,
-          function.comp, image_swap_eq_preimage_swap]
+          function.comp, image_swap_eq_preimage_swap, -subtype.val_eq_coe]
   end
   ... ≤ (𝓤 α).lift' gen :
     uniformity_lift_le_swap
@@ -77,7 +77,7 @@ calc map prod.swap ((𝓤 α).lift' gen) =
         @monotone_mem_sets (α×α) ((filter.prod ((p.2).val) ((p.1).val)))))
       begin
         have h := λ(p:Cauchy α×Cauchy α), @filter.prod_comm _ _ (p.2.val) (p.1.val),
-        simp [function.comp, h],
+        simp [function.comp, h, -subtype.val_eq_coe],
         exact le_refl _
       end
 
@@ -149,7 +149,7 @@ lemma uniform_inducing_pure_cauchy : uniform_inducing (pure_cauchy : α → Cauc
       ... = 𝓤 α : by simp [this]⟩
 
 lemma uniform_embedding_pure_cauchy : uniform_embedding (pure_cauchy : α → Cauchy α) :=
-{ inj := assume a₁ a₂ h, pure_injective $ subtype.ext.1 h,
+{ inj := assume a₁ a₂ h, pure_injective $ subtype.ext_iff_val.1 h,
   ..uniform_inducing_pure_cauchy }
 
 lemma pure_cauchy_dense : ∀x, x ∈ closure (range pure_cauchy) :=
diff --git a/src/topology/uniform_space/separation.lean b/src/topology/uniform_space/separation.lean
index be6b8fcca6000..acde3e17d1961 100644
--- a/src/topology/uniform_space/separation.lean
+++ b/src/topology/uniform_space/separation.lean
@@ -252,7 +252,7 @@ begin
     let Δ := diagonal,
     change _ ⊆ Δ _,
     change (prod.map (C s) (C s)) ⁻¹' (𝓢 α) = Δ _ at h,
-    rw [inter_comm, ← subtype.image_preimage_val,  image_subset_iff],
+    rw [inter_comm, ← subtype.image_preimage_coe,  image_subset_iff],
     change (C _) ⁻¹' _ ⊆ (C _) ⁻¹' _,
 
     let φ : ↥s × ↥s → (s.prod s)  := (λ x : s × s, ⟨(x.1.1, x.2.1), mk_mem_prod x.1.2 x.2.2⟩),
diff --git a/src/topology/uniform_space/uniform_embedding.lean b/src/topology/uniform_space/uniform_embedding.lean
index 5bb4c49bc44b5..be0fafb875d79 100644
--- a/src/topology/uniform_space/uniform_embedding.lean
+++ b/src/topology/uniform_space/uniform_embedding.lean
@@ -210,7 +210,7 @@ by rw [complete_space_iff_is_complete_range he, e.range_eq_univ,
 lemma complete_space_coe_iff_is_complete {s : set α} :
   complete_space s ↔ is_complete s :=
 (complete_space_iff_is_complete_range uniform_embedding_subtype_coe).trans $
-  by rw [range_coe_subtype]
+  by rw [subtype.range_coe]
 
 lemma is_complete.complete_space_coe {s : set α} (hs : is_complete s) :
   complete_space s :=