feat(subtype): standardize (leanprover-community#3204)

Add simp lemma from x.val to coe x
Use correct ext/ext_iff naming scheme
Use coe in more places in the library

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

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

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` -/

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 }

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

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

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`.

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

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

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
 

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,

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 _ _),

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

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) :=

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⟩)),

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,15 +282,15 @@ 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) :=
 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⟩)

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',

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