diff --git a/library/algebra/interval.lean b/library/algebra/interval.lean
index c3c4373f7c..87e8b7e140 100644
--- a/library/algebra/interval.lean
+++ b/library/algebra/interval.lean
@@ -14,11 +14,9 @@ open set
 section
   open set
 
-  theorem mem_singleton_of_eq {A : Type} {x a : A} (H : x = a) : x ∈ '{a} :=
-  eq.subst (eq.symm H) (mem_singleton a)
 end
 
-namespace intervals
+namespace interval
 
 section order_pair
 variables {A : Type} [order_pair A]
@@ -158,4 +156,4 @@ open nat eq.ops
   finite_subset this
 end nat
 
-end intervals
+end interval
diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean
index 4ff5416ccb..6784624bf6 100644
--- a/library/data/nat/bigops.lean
+++ b/library/data/nat/bigops.lean
@@ -71,7 +71,7 @@ end finset
 
 section set
   variables {A : Type} [add_comm_monoid A]
-  open set intervals
+  open set interval
 
 proposition sum_range_eq_sum_interval_aux (m n : ℕ) (f : ℕ → A) :
             (∑ i = m...m+n, f i) = (∑ i ∈ '[m, m + n], f i) :=
@@ -162,7 +162,7 @@ end finset
 
 section set
   variables {A : Type} [comm_monoid A]
-  open set intervals
+  open set interval
 
 proposition prod_range_eq_prod_interval_aux (m n : ℕ) (f : ℕ → A) :
             (∏ i = m...m+n, f i) = (∏ i ∈ '[m, m + n], f i) :=
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 5d4bba489e..f7b2f9dc95 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -296,11 +296,14 @@ iff.intro
 
 theorem mem_singleton (a : X) : a ∈ '{a} := !mem_insert
 
-theorem eq_of_mem_singleton {x y : X} : x ∈ insert y ∅ → x = y :=
-assume h, or.elim (eq_or_mem_of_mem_insert h)
+theorem eq_of_mem_singleton {x y : X} (h : x ∈ '{y}) : x = y :=
+or.elim (eq_or_mem_of_mem_insert h)
   (suppose x = y, this)
   (suppose x ∈ ∅, absurd this !not_mem_empty)
 
+theorem mem_singleton_of_eq {x y : X} (H : x = y) : x ∈ '{y} :=
+eq.symm H ▸ mem_singleton y
+
 theorem insert_eq (x : X) (s : set X) : insert x s = '{x} ∪ s :=
 ext (take y, iff.intro
   (suppose y ∈ insert x s,