refactor(library/data/{list,set,finset}/basic.lean): make subset reserved notation

library/data/finset/basic.lean

@@ -453,7 +453,7 @@ quot.lift_on₂ s₁ s₂
     (λ s₁ a i, mem_perm p₂ (s₁ a (mem_perm (perm.symm p₁) i)))
     (λ s₂ a i, mem_perm (perm.symm p₂) (s₂ a (mem_perm p₁ i)))))
 
-infix `⊆`:50 := subset
+infix `⊆` := subset
 
 theorem empty_subset (s : finset A) : ∅ ⊆ s :=
 quot.induction_on s (λ l, list.nil_sub (elt_of l))

library/data/list/basic.lean

@@ -286,7 +286,7 @@ assume nin nainl, absurd (or.inr nainl) nin
 
 definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈ l₂
 
-infix `⊆`:50 := sublist
+infix `⊆` := sublist
 
 theorem nil_sub (l : list T) : [] ⊆ l :=
 λ b i, false.elim (iff.mp (mem_nil_iff b) i)

library/data/set/basic.lean

@@ -22,7 +22,7 @@ theorem setext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b :=
 funext (take x, propext (H x))
 
 definition subset (a b : set X) := ∀⦃x⦄, x ∈ a → x ∈ b
-infix `⊆`:50 := subset
+infix `⊆` := subset
 
 /- bounded quantification -/
 

library/init/reserved_notation.lean

@@ -88,6 +88,7 @@ reserve infix `∈`:50
 reserve infix `∉`:50
 reserve infixl `∩`:70
 reserve infixl `∪`:65
+reserve infix `⊆`:50
 
 /- other symbols -/