refactor(library/init/subtype.lean): put subtype notation in the namespace

The notation { x : A | P x } is overloaded in set, and is ambiguous.

library/data/nat/bquant.lean

@@ -29,7 +29,7 @@ namespace nat
   ∀ x, x < n → P x
 
   lemma bex_of_bsub {n : nat} {P : nat → Prop} : bsub n P → bex n P :=
-  assume h, ex_of_sub h
+  assume h, exists_of_subtype h
 
   theorem not_bex_zero (P : nat → Prop) : ¬ bex 0 P :=
   λ H, obtain (w : nat) (Hw : w < 0 ∧ P w), from H,
@@ -114,7 +114,7 @@ section
 end
 
 namespace nat
-  open decidable
+  open decidable subtype
   variable {P : nat → Prop}
   variable [decP : decidable_pred P]
   include decP

library/init/subtype.lean

@@ -12,12 +12,12 @@ set_option structure.proj_mk_thm true
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binder ` | ` r:(scoped:1 P, subtype P) `}` := r
-
-definition ex_of_sub {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x
-| (subtype.tag a h) := exists.intro a h
-
 namespace subtype
+  notation `{` binder ` | ` r:(scoped:1 P, subtype P) `}` := r
+
+  definition exists_of_subtype {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x
+  | (subtype.tag a h) := exists.intro a h
+
   variables {A : Type} {P : A → Prop}
 
   theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 :=

library/theories/number_theory/primes.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 Prime numbers.
 -/
 import data.nat logic.identities
-open bool
+open bool subtype
 
 namespace nat
 open decidable
@@ -84,7 +84,7 @@ have ¬ m = 1 ∧ ¬ m = n,  from iff.mp !not_or_iff_not_and_not h₅,
 subtype.tag m (and.intro `m ∣ n` this)
 
 theorem exists_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
-assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂)
+assume h₁ h₂, exists_of_subtype (sub_dvd_of_not_prime h₁ h₂)
 
 definition sub_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≥ 2 ∧ m < n} :=
 assume h₁ h₂,
@@ -101,7 +101,7 @@ begin
 end
 
 theorem exists_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
-assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime2 h₁ h₂)
+assume h₁ h₂, exists_of_subtype (sub_dvd_of_not_prime2 h₁ h₂)
 
 definition sub_prime_and_dvd {n : nat} : n ≥ 2 → {p | prime p ∧ p ∣ n} :=
 nat.strong_rec_on n
@@ -117,7 +117,7 @@ nat.strong_rec_on n
       subtype.tag p (and.intro hp this)))
 
 lemma exists_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
-assume h, ex_of_sub (sub_prime_and_dvd h)
+assume h, exists_of_subtype (sub_prime_and_dvd h)
 
 open eq.ops
 
@@ -139,7 +139,7 @@ have p ≥ n, from by_contradiction
 subtype.tag p (and.intro this `prime p`)
 
 lemma exists_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p :=
-ex_of_sub (infinite_primes n)
+exists_of_subtype (infinite_primes n)
 
 lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=
 λ pp p_gt_2, by_contradiction (λ hn,