fix(library/tests/lean/*): fix tests

tests/lean/1369.lean

@@ -20,7 +20,7 @@ end
 
 example : { k : ℕ // k ≤ 555555 } :=
 begin
-  refine subtype.tag _ _,
+  refine subtype.mk _ _,
   exact 17,
   target >>= trace,
   trace_state,
@@ -32,7 +32,7 @@ set_option pp.instantiate_mvars false
 
 example : { k : ℕ // k ≤ 555555 } :=
 begin
-  refine subtype.tag _ _,
+  refine subtype.mk _ _,
   exact 17,
   target >>= trace,
   trace_state,

tests/lean/run/coe_univ_bug.lean

@@ -12,7 +12,7 @@ instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
 ⟨Type u, (λ p : A → Prop, subtype p)⟩
 
 instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ pred2subtype p) A :=
-⟨λ s, subtype.elt_of s⟩
+⟨λ s, subtype.val s⟩
 
 def g {n : nat} (v : below n) : nat :=
 v + 1

tests/lean/run/match2.lean

@@ -4,4 +4,4 @@ inductive imf (f : nat → nat) : nat → Type
 
 definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat // x > b} → nat
 | .(f a)     (imf.mk1 .f a) x := a
-| .(f 0 + 1) (imf.mk2 .f)   x := subtype.elt_of x
+| .(f 0 + 1) (imf.mk2 .f)   x := subtype.val x

tests/lean/run/pred_to_subtype_coercion.lean

@@ -18,4 +18,4 @@ sorry
 check f ⟨0, zlt10⟩
 
 definition g (a : below 10) : nat :=
-subtype.elt_of a
+subtype.val a