diff --git a/algebra/module.lean b/algebra/module.lean
index 422eb4296cef5..01ab3f31f8260 100644
--- a/algebra/module.lean
+++ b/algebra/module.lean
@@ -12,9 +12,6 @@ open function
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
-lemma set.sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂i ∈ s, i) :=
-set.ext $ by simp
-
 /-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
 class has_scalar (α : out_param $ Type u) (γ : Type v) := (smul : α → γ → γ)
 
@@ -217,7 +214,7 @@ instance Inter_submodule' {ι : Sort w} {s : ι → set β} [h : ∀i, is_submod
 Inter_submodule h
 
 instance sInter_submodule {s : set (set β)} [hs : ∀t∈s, is_submodule t] : is_submodule (⋂₀ s) :=
-by rw [set.sInter_eq_Inter]; exact Inter_submodule (assume t, Inter_submodule $ hs t)
+by rw set.sInter_eq_bInter; exact Inter_submodule (assume t, Inter_submodule $ hs t)
 
 instance inter_submodule : is_submodule (p ∩ p') :=
 suffices is_submodule (⋂₀ {p, p'} : set β), by simpa [set.inter_comm],
diff --git a/analysis/topology/topological_space.lean b/analysis/topology/topological_space.lean
index e2a0ae1d52dae..23d73c9cfee36 100644
--- a/analysis/topology/topological_space.lean
+++ b/analysis/topology/topological_space.lean
@@ -109,7 +109,7 @@ is_closed_sInter $ assume t ⟨i, (heq : t = f i)⟩, heq.symm ▸ h i
 @[simp] lemma is_closed_compl_iff {s : set α} : is_closed (-s) ↔ is_open s :=
 by rw [←is_open_compl_iff, compl_compl]
 
-lemma is_open_diff {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) : is_open (s - t) :=
+lemma is_open_diff {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) : is_open (s \ t) :=
 is_open_inter h₁ $ is_open_compl_iff.mpr h₂
 
 lemma is_closed_inter (h₁ : is_closed s₁) (h₂ : is_closed s₂) : is_closed (s₁ ∩ s₂) :=
@@ -180,11 +180,11 @@ lemma interior_union_is_closed_of_interior_empty {s t : set α} (h₁ : is_close
 have interior (s ∪ t) ⊆ s, from
   assume x ⟨u, ⟨(hu₁ : is_open u), (hu₂ : u ⊆ s ∪ t)⟩, (hx₁ : x ∈ u)⟩,
   classical.by_contradiction $ assume hx₂ : x ∉ s,
-    have u - s ⊆ t,
+    have u \ s ⊆ t,
       from assume x ⟨h₁, h₂⟩, or.resolve_left (hu₂ h₁) h₂,
-    have u - s ⊆ interior t,
+    have u \ s ⊆ interior t,
       by simp [subset_interior_iff_subset_of_open, this, is_open_diff hu₁ h₁],
-    have u - s ⊆ ∅,
+    have u \ s ⊆ ∅,
       by rw [h₂] at this; assumption,
     this ⟨hx₁, hx₂⟩,
 subset.antisymm
@@ -240,7 +240,7 @@ lemma closure_eq_compl_interior_compl {s : set α} : closure s = - interior (- s
 begin
   simp [interior, closure],
   rw [compl_sUnion, compl_image_set_of],
-  simp [compl_subset_compl_iff_subset]
+  simp [compl_subset_compl]
 end
 
 @[simp] lemma interior_compl_eq {s : set α} : interior (- s) = - closure s :=
@@ -251,10 +251,9 @@ by simp [closure_eq_compl_interior_compl]
 
 lemma closure_compl {s : set α} : closure (-s) = - interior s :=
 subset.antisymm
-  (by simp [closure_subset_iff_subset_of_is_closed, compl_subset_compl_iff_subset, subset.refl])
+  (by simp [closure_subset_iff_subset_of_is_closed, compl_subset_compl, subset.refl])
   begin
-    rw [←compl_subset_compl_iff_subset, compl_compl, subset_interior_iff_subset_of_open,
-      ←compl_subset_compl_iff_subset, compl_compl],
+    rw [compl_subset_comm, subset_interior_iff_subset_of_open, compl_subset_comm],
     exact subset_closure,
     exact is_open_compl_iff.mpr is_closed_closure
   end
@@ -276,7 +275,7 @@ def frontier (s : set α) : set α := closure s \ interior s
 
 lemma frontier_eq_closure_inter_closure {s : set α} :
   frontier s = closure s ∩ closure (- s) :=
-by rw [closure_compl, frontier, sdiff_eq]
+by rw [closure_compl, frontier, diff_eq]
 
 /-- neighbourhood filter -/
 def nhds (a : α) : filter α := (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal s)
@@ -354,7 +353,7 @@ calc closure s = - interior (- s) : closure_eq_compl_interior_compl
 theorem mem_closure_iff_nhds {s : set α} {a : α} : a ∈ closure s ↔ ∀ t ∈ (nhds a).sets, t ∩ s ≠ ∅ :=
 mem_closure_iff.trans
 ⟨λ H t ht, subset_ne_empty
-  (inter_subset_inter_right _ interior_subset)
+  (inter_subset_inter_left _ interior_subset)
   (H _ is_open_interior (mem_interior_iff_mem_nhds.2 ht)),
  λ H o oo ao, H _ (mem_nhds_sets oo ao)⟩
 
@@ -428,7 +427,7 @@ is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
   ... ≤ principal (- ⋃i, f i) :
   begin
     simp only [principal_mono, subset_def, mem_compl_eq, mem_inter_eq,
-      mem_Inter_eq, mem_set_of_eq, mem_Union_eq, and_imp, not_exists,
+      mem_Inter, mem_set_of_eq, mem_Union, and_imp, not_exists,
       not_eq_empty_iff_exists, exists_imp_distrib, (≠)],
     exact assume x xt ht i xfi, ht i x xfi xt xfi
   end
@@ -494,9 +493,9 @@ classical.by_contradiction $ assume h,
   in
   have f ≠ ⊥, from infi_neq_bot_of_directed ⟨a⟩
     (assume ⟨c₁, hc₁, hc'₁⟩ ⟨c₂, hc₂, hc'₂⟩, ⟨⟨c₁ ∪ c₂, union_subset hc₁ hc₂, finite_union hc'₁ hc'₂⟩,
-      principal_mono.mpr $ diff_right_antimono $ sUnion_mono $ subset_union_left _ _,
-      principal_mono.mpr $ diff_right_antimono $ sUnion_mono $ subset_union_right _ _⟩)
-    (assume ⟨c', hc'₁, hc'₂⟩, show principal (s \ _) ≠ ⊥, by simp [diff_neq_empty]; exact h hc'₁ hc'₂),
+      principal_mono.mpr $ diff_subset_diff_right $ sUnion_mono $ subset_union_left _ _,
+      principal_mono.mpr $ diff_subset_diff_right $ sUnion_mono $ subset_union_right _ _⟩)
+    (assume ⟨c', hc'₁, hc'₂⟩, show principal (s \ _) ≠ ⊥, by simp [diff_eq_empty]; exact h hc'₁ hc'₂),
   have f ≤ principal s, from infi_le_of_le ⟨∅, empty_subset _, finite_empty⟩ $
     show principal (s \ ⋃₀∅) ≤ principal s, by simp; exact subset.refl s,
   let
@@ -823,7 +822,7 @@ def topological_space.induced {α : Type u} {β : Type v} (f : α → β) (t : t
     simp [classical.skolem] at h,
     cases h with f hf,
     apply exists.intro (⋃(x : set α) (h : x ∈ s), f x h),
-    simp [sUnion_eq_Union, (λx h, (hf x h).right.symm)],
+    simp [sUnion_eq_bUnion, (λx h, (hf x h).right.symm)],
     exact (@is_open_Union β _ t _ $ assume i,
       show is_open (⋃h, f i h), from @is_open_Union β _ t _ $ assume h, (hf i h).left)
   end }
@@ -1094,7 +1093,7 @@ lemma Union_basis_of_is_open {B : set (set α)}
   (hB : is_topological_basis B) {u : set α} (ou : _root_.is_open u) :
   ∃ (β : Type u) (f : β → set α), u = (⋃ i, f i) ∧ ∀ i, f i ∈ B :=
 let ⟨S, sb, su⟩ := sUnion_basis_of_is_open hB ou in
-⟨S, subtype.val, su.trans set.sUnion_eq_Union', λ ⟨b, h⟩, sb h⟩
+⟨S, subtype.val, su.trans set.sUnion_eq_Union, λ ⟨b, h⟩, sb h⟩
 
 variables (α)
 
@@ -1122,7 +1121,7 @@ lemma is_open_generated_countable_inter [second_countable_topology α] :
 let ⟨b, hb₁, hb₂⟩ := second_countable_topology.is_open_generated_countable α in
 let b' := (λs, ⋂₀ s) '' {s:set (set α) | finite s ∧ s ⊆ b ∧ ⋂₀ s ≠ ∅} in
 ⟨b',
-  countable_image $ countable_subset (by simp {contextual:=tt}) (countable_set_of_finite_subset hb₁),
+  countable_image _ $ countable_subset (by simp {contextual:=tt}) (countable_set_of_finite_subset hb₁),
   assume ⟨s, ⟨_, _, hn⟩, hp⟩, hn hp,
   is_topological_basis_of_subbasis hb₂⟩
 
@@ -1148,11 +1147,11 @@ let ⟨f, hf⟩ := this in
       let ⟨s₃, hs₃, has₃, hs⟩ := hb₃ _ hs₁ _ hs₂ _ this in
       ⟨⟨s₃, has₃, hs₃⟩, begin
         simp only [le_principal_iff, mem_principal_sets],
-        simp at hs, split; apply inter_subset_inter_right; simp [hs]
+        simp at hs, split; apply inter_subset_inter_left; simp [hs]
       end⟩)
     (assume ⟨s, has, hs⟩,
       have s ∩ (⋃ (s : set α) (H h : s ∈ b), {f s h}) ≠ ∅,
-        from ne_empty_of_mem ⟨hf _ hs, mem_bUnion hs $ (mem_Union_eq _ _).mpr ⟨hs, by simp⟩⟩,
+        from ne_empty_of_mem ⟨hf _ hs, mem_bUnion hs $ mem_Union.mpr ⟨hs, by simp⟩⟩,
       by simp [this]) ⟩⟩
 
 end topological_space
diff --git a/analysis/topology/uniform_space.lean b/analysis/topology/uniform_space.lean
index 079600cc64f34..fe9e5f7c947f0 100644
--- a/analysis/topology/uniform_space.lean
+++ b/analysis/topology/uniform_space.lean
@@ -794,11 +794,11 @@ lemma totally_bounded_iff_filter {s : set α} :
   have f ≠ ⊥,
     from infi_neq_bot_of_directed ⟨a⟩
       (assume ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩, ⟨⟨t₁ ∪ t₂, finite_union ht₁ ht₂⟩,
-        principal_mono.mpr $ diff_right_antimono $ Union_subset_Union $
+        principal_mono.mpr $ diff_subset_diff_right $ Union_subset_Union $
           assume t, Union_subset_Union_const or.inl,
-        principal_mono.mpr $ diff_right_antimono $ Union_subset_Union $
+        principal_mono.mpr $ diff_subset_diff_right $ Union_subset_Union $
           assume t, Union_subset_Union_const or.inr⟩)
-      (assume ⟨t, ht⟩, by simp [diff_neq_empty]; exact hd_cover ht),
+      (assume ⟨t, ht⟩, by simp [diff_eq_empty]; exact hd_cover ht),
   have f ≤ principal s, from infi_le_of_le ⟨∅, finite_empty⟩ $ by simp; exact subset.refl s,
   let
     ⟨c, (hc₁ : c ≤ f), (hc₂ : cauchy c)⟩ := h f ‹f ≠ ⊥› this,
diff --git a/data/analysis/topology.lean b/data/analysis/topology.lean
index 63ecb30152651..4e1527dc374a3 100644
--- a/data/analysis/topology.lean
+++ b/data/analysis/topology.lean
@@ -178,7 +178,7 @@ theorem locally_finite_iff_exists_realizer [topological_space α]
        let ⟨h, h'⟩ := h₁ x in F.mem_nhds.1 h) in
   ⟨⟨λ x, ⟨g₂ x, (h₂ x).1⟩, λ x, finite.fintype $
     let ⟨h, h'⟩ := h₁ x in finite_subset h' $ λ i,
-    subset_ne_empty (inter_subset_inter_left _ (h₂ x).2)⟩⟩,
+    subset_ne_empty (inter_subset_inter_right _ (h₂ x).2)⟩⟩,
  λ ⟨R⟩, R.to_locally_finite⟩
 
 def compact.realizer [topological_space α] (R : realizer α) (s : set α) :=
diff --git a/data/set/basic.lean b/data/set/basic.lean
index 20956f96715d6..ae5b5de7c802a 100644
--- a/data/set/basic.lean
+++ b/data/set/basic.lean
@@ -233,9 +233,15 @@ by finish [subset_def, union_def]
 @[simp] theorem union_subset_iff {s t u : set α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u :=
 by finish [iff_def, subset_def]
 
-theorem union_subset_union {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∪ s₂ ⊆ t₁ ∪ t₂ :=
+theorem union_subset_union {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) : s₁ ∪ t₁ ⊆ s₂ ∪ t₂ :=
 by finish [subset_def]
 
+theorem union_subset_union_left {s₁ s₂ : set α} (t) (h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t :=
+union_subset_union h (by refl)
+
+theorem union_subset_union_right (s) {t₁ t₂ : set α} (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂ :=
+union_subset_union (by refl) h
+
 @[simp] theorem union_empty_iff {s t : set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ :=
 ⟨by finish [ext_iff], by finish [ext_iff]⟩
 
@@ -300,10 +306,10 @@ ext (assume x, and_true _)
 @[simp] theorem univ_inter (a : set α) : univ ∩ a = a :=
 ext (assume x, true_and _)
 
-theorem inter_subset_inter_right {s t : set α} (u : set α) (H : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
+theorem inter_subset_inter_left {s t : set α} (u : set α) (H : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
 by finish [subset_def]
 
-theorem inter_subset_inter_left {s t : set α} (u : set α) (H : s ⊆ t) : u ∩ s ⊆ u ∩ t :=
+theorem inter_subset_inter_right {s t : set α} (u : set α) (H : s ⊆ t) : u ∩ s ⊆ u ∩ t :=
 by finish [subset_def]
 
 theorem inter_subset_inter {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∩ s₂ ⊆ t₁ ∩ t₂ :=
@@ -315,6 +321,12 @@ by finish [subset_def, ext_iff, iff_def]
 theorem inter_eq_self_of_subset_right {s t : set α} (h : t ⊆ s) : s ∩ t = t :=
 by finish [subset_def, ext_iff, iff_def]
 
+theorem union_inter_cancel_left {s t : set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) ∩ s = s :=
+by finish [ext_iff, iff_def]
+
+theorem union_inter_cancel_right {s t : set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) ∩ t = t :=
+by finish [ext_iff, iff_def]
+
 -- TODO(Mario): remove?
 theorem nonempty_of_inter_nonempty_right {s t : set α} (h : s ∩ t ≠ ∅) : t ≠ ∅ :=
 by finish [ext_iff, iff_def]
@@ -508,6 +520,9 @@ theorem compl_subset_comm {s t : set α} : -s ⊆ t ↔ -t ⊆ s :=
 by haveI := classical.prop_decidable; exact
 forall_congr (λ a, not_imp_comm)
 
+lemma compl_subset_compl {s t : set α} : -s ⊆ -t ↔ t ⊆ s :=
+by rw [compl_subset_comm, compl_compl]
+
 theorem compl_subset_iff_union {s t : set α} : -s ⊆ t ↔ s ∪ t = univ :=
 iff.symm $ eq_univ_iff_forall.trans $ forall_congr $ λ a,
 by haveI := classical.prop_decidable; exact or_iff_not_imp_left
@@ -538,19 +553,43 @@ theorem mem_diff_iff (s t : set α) (x : α) : x ∈ s \ t ↔ x ∈ s ∧ x ∉
 theorem union_diff_cancel {s t : set α} (h : s ⊆ t) : s ∪ (t \ s) = t :=
 by finish [ext_iff, iff_def, subset_def]
 
+theorem union_diff_cancel_left {s t : set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ s = t :=
+by finish [ext_iff, iff_def, subset_def]
+
+theorem union_diff_cancel_right {s t : set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ t = s :=
+by finish [ext_iff, iff_def, subset_def]
+
+theorem union_diff_left {s t : set α} : (s ∪ t) \ s = t \ s :=
+by finish [ext_iff, iff_def]
+
+theorem union_diff_right {s t : set α} : (s ∪ t) \ t = s \ t :=
+by finish [ext_iff, iff_def]
+
+theorem inter_diff_assoc (a b c : set α) : (a ∩ b) \ c = a ∩ (b \ c) :=
+inter_assoc _ _ _
+
+theorem inter_diff_self (a b : set α) : a ∩ (b \ a) = ∅ :=
+by finish [ext_iff]
+
+theorem inter_union_diff (s t : set α) : (s ∩ t) ∪ (s \ t) = s :=
+by finish [ext_iff, iff_def]
+
 theorem diff_subset (s t : set α) : s \ t ⊆ s :=
 by finish [subset_def]
 
 theorem diff_subset_diff {s₁ s₂ t₁ t₂ : set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂ :=
 by finish [subset_def]
 
-theorem diff_right_antimono {s t u : set α} (h : t ⊆ u) : s \ u ⊆ s \ t :=
+theorem diff_subset_diff_left {s₁ s₂ t : set α} (h : s₁ ⊆ s₂) : s₁ \ t ⊆ s₂ \ t :=
+diff_subset_diff h (by refl)
+
+theorem diff_subset_diff_right {s t u : set α} (h : t ⊆ u) : s \ u ⊆ s \ t :=
 diff_subset_diff (subset.refl s) h
 
 theorem compl_eq_univ_diff (s : set α) : -s = univ \ s :=
 by finish [ext_iff]
 
-theorem diff_neq_empty {s t : set α} : s \ t = ∅ ↔ s ⊆ t :=
+theorem diff_eq_empty {s t : set α} : s \ t = ∅ ↔ s ⊆ t :=
 ⟨assume h x hx, classical.by_contradiction $ assume : x ∉ t, show x ∈ (∅ : set α), from h ▸ ⟨hx, this⟩,
   assume h, eq_empty_of_subset_empty $ assume x ⟨hx, hnx⟩, hnx $ h hx⟩
 
@@ -567,9 +606,28 @@ lemma diff_subset_iff {s t u : set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u :=
 lemma diff_subset_comm {s t u : set α} : s \ t ⊆ u ↔ s \ u ⊆ t :=
 by rw [diff_subset_iff, diff_subset_iff, union_comm]
 
-@[simp] theorem insert_sdiff (h : a ∈ t) : insert a s \ t = s \ t :=
+@[simp] theorem insert_diff (h : a ∈ t) : insert a s \ t = s \ t :=
 set.ext $ by intro; constructor; simp [or_imp_distrib, h] {contextual := tt}
 
+theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
+by finish [ext_iff, iff_def]
+
+theorem diff_union_self {s t : set α} : (s \ t) ∪ t = s ∪ t :=
+by rw [union_comm, union_diff_self, union_comm]
+
+theorem diff_inter_self {a b : set α} : (b \ a) ∩ a = ∅ :=
+set.ext $ by simp [iff_def] {contextual:=tt}
+
+theorem diff_eq_self {s t : set α} : s \ t = s ↔ t ∩ s ⊆ ∅ :=
+by finish [ext_iff, iff_def, subset_def]
+
+@[simp] theorem diff_singleton_eq_self {a : α} {s : set α} (h : a ∉ s) : s \ {a} = s :=
+diff_eq_self.2 $ by simp [singleton_inter_eq_empty.2 h]
+
+@[simp] theorem insert_diff_singleton {a : α} {s : set α} :
+  insert a (s \ {a}) = insert a s :=
+by simp [insert_eq, union_diff_self]
+
 /- powerset -/
 
 theorem mem_powerset {x s : set α} (h : x ⊆ s) : x ∈ powerset s := h
diff --git a/data/set/disjointed.lean b/data/set/disjointed.lean
index 29019a4a18ade..9ea226aabea4c 100644
--- a/data/set/disjointed.lean
+++ b/data/set/disjointed.lean
@@ -24,44 +24,32 @@ namespace set
 def disjointed (f : ℕ → set α) (n : ℕ) : set α := f n ∩ (⋂i<n, - f i)
 
 lemma disjoint_disjointed {f : ℕ → set α} : pairwise (disjoint on disjointed f) :=
-assume i j h,
-have ∀i j, i < j → disjointed f i ∩ disjointed f j = ∅,
-  from assume i j hij, eq_empty_iff_forall_not_mem.2 $ assume x h,
-  have x ∈ f i, from h.left.left,
-  have x ∈ (⋂i<j, - f i), from h.right.right,
-  have x ∉ f i, begin simp at this; exact this _ hij end,
-  absurd ‹x ∈ f i› this,
-show disjointed f i ∩ disjointed f j = ∅,
-  from (ne_iff_lt_or_gt.mp h).elim (this i j) begin rw [inter_comm], exact this j i end
+λ i j h, begin
+  wlog h' : i ≤ j; [skip, {revert a, exact (this h.symm).symm}],
+  rintro a ⟨⟨h₁, _⟩, h₂, h₃⟩, simp at h₃,
+  exact h₃ _ (lt_of_le_of_ne h' h) h₁
+end
 
 lemma disjointed_Union {f : ℕ → set α} : (⋃n, disjointed f n) = (⋃n, f n) :=
 subset.antisymm (Union_subset_Union $ assume i, inter_subset_left _ _) $
   assume x h,
-  have ∃n, x ∈ f n, from (mem_Union_eq _ _).mp h,
+  have ∃n, x ∈ f n, from mem_Union.mp h,
   have hn : ∀ (i : ℕ), i < nat.find this → x ∉ f i,
     from assume i, nat.find_min this,
-  (mem_Union_eq _ _).mpr ⟨nat.find this, nat.find_spec this, by simp; assumption⟩
+  mem_Union.mpr ⟨nat.find this, nat.find_spec this, by simp; assumption⟩
 
 lemma disjointed_induct {f : ℕ → set α} {n : ℕ} {p : set α → Prop}
-  (h₁ : p (f n)) (h₂ : ∀t i, p t → p (t - f i)) :
+  (h₁ : p (f n)) (h₂ : ∀t i, p t → p (t \ f i)) :
   p (disjointed f n) :=
-have ∀n t, p t → p (t ∩ (⋂i<n, - f i)),
 begin
-  intro n, induction n,
-  case nat.zero {
-    have h : (⋂ (i : ℕ) (H : i < 0), -f i) = univ,
-      { apply eq_univ_of_forall,
-        simp [mem_Inter, nat.not_lt_zero] },
-    simp [h, inter_univ] },
+  rw disjointed,
+  generalize_hyp : f n = t at h₁ ⊢,
+  induction n,
+  case nat.zero { simp [nat.not_lt_zero, h₁] },
   case nat.succ : n ih {
-    intro t,
-    have h : (⨅i (H : i < n.succ), -f i) = (⨅i (H : i < n), -f i) ⊓ - f n,
-      by simp [nat.lt_succ_iff_lt_or_eq, infi_or, infi_inf_eq, inf_comm],
-    change (⋂ (i : ℕ) (H : i < n.succ), -f i) = (⋂ (i : ℕ) (H : i < n), -f i) ∩ - f n at h,
-    rw [h, ←inter_assoc],
-    exact assume ht, h₂ _ _ (ih _ ht) }
-end,
-this _ _ h₁
+    rw [Inter_lt_succ, inter_comm (-f n), ← inter_assoc],
+    exact h₂ _ n ih }
+end
 
 lemma disjointed_of_mono {f : ℕ → set α} {n : ℕ} (hf : monotone f) :
   disjointed f (n + 1) = f (n + 1) \ f n :=
@@ -69,6 +57,6 @@ have (⋂i (h : i < n + 1), -f i) = - f n,
   from le_antisymm
     (infi_le_of_le n $ infi_le_of_le (nat.lt_succ_self _) $ subset.refl _)
     (le_infi $ assume i, le_infi $ assume hi, neg_le_neg $ hf $ nat.le_of_succ_le_succ hi),
-by simp [disjointed, this, sdiff_eq]
+by simp [disjointed, this, diff_eq]
 
 end set
diff --git a/data/set/finite.lean b/data/set/finite.lean
index 489ae38de4f9f..f1e3dc5470a1d 100644
--- a/data/set/finite.lean
+++ b/data/set/finite.lean
@@ -191,7 +191,7 @@ theorem finite_Union {ι : Type*} [fintype ι] {f : ι → set α} (H : ∀i, fi
 ⟨@set.fintype_Union _ (classical.dec_eq α) _ _ _ (λ i, finite.fintype (H i))⟩
 
 theorem finite_sUnion {s : set (set α)} (h : finite s) (H : ∀t∈s, finite t) : finite (⋃₀ s) :=
-by rw sUnion_eq_Union'; haveI := finite.fintype h;
+by rw sUnion_eq_Union; haveI := finite.fintype h;
    apply finite_Union; simpa using H
 
 instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
diff --git a/data/set/lattice.lean b/data/set/lattice.lean
index 2f56ff568269a..e114df89d0534 100644
--- a/data/set/lattice.lean
+++ b/data/set/lattice.lean
@@ -7,7 +7,7 @@ Authors Jeremy Avigad, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 import logic.basic data.set.basic data.equiv.basic tactic
 import order.complete_boolean_algebra category.basic
-import tactic.finish
+import tactic.finish data.sigma.basic
 
 open function tactic set lattice auto
 
@@ -67,20 +67,17 @@ assume s t, assume h : s ⊆ t, image_subset _ h
 notation `⋃` binders `, ` r:(scoped f, Union f) := r
 notation `⋂` binders `, ` r:(scoped f, Inter f) := r
 
-@[simp] theorem mem_Union_eq (x : β) (s : ι → set β) : (x ∈ ⋃ i, s i) = (∃ i, x ∈ s i) :=
-propext
-  ⟨assume ⟨t, ⟨⟨a, (t_eq : t = s a)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq ▸ h⟩,
+@[simp] theorem mem_Union {x : β} {s : ι → set β} : x ∈ Union s ↔ ∃ i, x ∈ s i :=
+⟨assume ⟨t, ⟨⟨a, (t_eq : t = s a)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq ▸ h⟩,
   assume ⟨a, h⟩, ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩
 /- alternative proof: dsimp [Union, supr, Sup]; simp -/
   -- TODO: more rewrite rules wrt forall / existentials and logical connectives
   -- TODO: also eliminate ∃i, ... ∧ i = t ∧ ...
 
-@[simp] theorem mem_Inter_eq (x : β) (s : ι → set β) : (x ∈ ⋂ i, s i) = (∀ i, x ∈ s i) :=
-propext
-  ⟨assume (h : ∀a ∈ {a : set β | ∃i, a = s i}, x ∈ a) a, h (s a) ⟨a, rfl⟩,
+@[simp] theorem mem_Inter {x : β} {s : ι → set β} : x ∈ Inter s ↔ ∀ i, x ∈ s i :=
+⟨assume (h : ∀a ∈ {a : set β | ∃i, a = s i}, x ∈ a) a, h (s a) ⟨a, rfl⟩,
   assume h t ⟨a, (eq : t = s a)⟩, eq.symm ▸ h a⟩
 
-
 theorem Union_subset {s : ι → set β} {t : set β} (h : ∀ i, s i ⊆ t) : (⋃ i, s i) ⊆ t :=
 -- TODO: should be simpler when sets' order is based on lattices
 @supr_le (set β) _ set.lattice_set _ _ h
@@ -88,41 +85,87 @@ theorem Union_subset {s : ι → set β} {t : set β} (h : ∀ i, s i ⊆ t) : (
 theorem Union_subset_iff {α : Sort u} {s : α → set β} {t : set β} : (⋃ i, s i) ⊆ t ↔ (∀ i, s i ⊆ t):=
 ⟨assume h i, subset.trans (le_supr s _) h, Union_subset⟩
 
-theorem mem_Inter {α : Sort u} {x : β} {s : α → set β} : (∀ i, x ∈ s i) → (x ∈ ⋂ i, s i) :=
+theorem mem_Inter_of_mem {α : Sort u} {x : β} {s : α → set β} : (∀ i, x ∈ s i) → (x ∈ ⋂ i, s i) :=
 assume h t ⟨a, (eq : t = s a)⟩, eq.symm ▸ h a
 
 theorem subset_Inter {t : set β} {s : α → set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=
 -- TODO: should be simpler when sets' order is based on lattices
 @le_infi (set β) _ set.lattice_set _ _ h
 
+theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr
+
+theorem Inter_subset : ∀ (s : ι → set β) (i : ι), (⋂ i, s i) ⊆ s i := infi_le
+
+theorem Union_const [inhabited ι] (s : set β) : (⋃ i:ι, s) = s :=
+ext $ by simp
+
+theorem Inter_const [inhabited ι] (s : set β) : (⋂ i:ι, s) = s :=
+ext $ by simp
+
 @[simp] -- complete_boolean_algebra
-theorem compl_Union (s : α → set β) : - (⋃ i, s i) = (⋂ i, - s i) :=
-ext (λ x, by simp)
+theorem compl_Union (s : ι → set β) : - (⋃ i, s i) = (⋂ i, - s i) :=
+ext (by simp)
 
 -- classical -- complete_boolean_algebra
-theorem compl_Inter (s : α → set β) : -(⋂ i, s i) = (⋃ i, - s i) :=
+theorem compl_Inter (s : ι → set β) : -(⋂ i, s i) = (⋃ i, - s i) :=
 ext (λ x, by simp [classical.not_forall])
 
 -- classical -- complete_boolean_algebra
-theorem Union_eq_comp_Inter_comp (s : α → set β) : (⋃ i, s i) = - (⋂ i, - s i) :=
+theorem Union_eq_comp_Inter_comp (s : ι → set β) : (⋃ i, s i) = - (⋂ i, - s i) :=
 by simp [compl_Inter, compl_compl]
 
 -- classical -- complete_boolean_algebra
-theorem Inter_eq_comp_Union_comp (s : α → set β) : (⋂ i, s i) = - (⋃ i, -s i) :=
+theorem Inter_eq_comp_Union_comp (s : ι → set β) : (⋂ i, s i) = - (⋃ i, -s i) :=
 by simp [compl_compl]
 
-theorem inter_distrib_Union_left (s : set β) (t : ι → set β) :
+theorem inter_Union_left (s : set β) (t : ι → set β) :
   s ∩ (⋃ i, t i) = ⋃ i, s ∩ t i :=
-set.ext (by simp)
+ext $ by simp
 
-theorem inter_distrib_Union_right (s : set β) (t : ι → set β) :
+theorem inter_Union_right (s : set β) (t : ι → set β) :
   (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
-set.ext (by simp)
+ext $ by simp
+
+theorem Union_union_distrib (s : ι → set β) (t : ι → set β) :
+  (⋃ i, s i ∪ t i) = (⋃ i, s i) ∪ (⋃ i, t i) :=
+ext $ by simp [exists_or_distrib]
+
+theorem Inter_inter_distrib (s : ι → set β) (t : ι → set β) :
+  (⋂ i, s i ∩ t i) = (⋂ i, s i) ∩ (⋂ i, t i) :=
+ext $ by simp [forall_and_distrib]
+
+theorem union_Union_left [inhabited ι] (s : set β) (t : ι → set β) :
+  s ∪ (⋃ i, t i) = ⋃ i, s ∪ t i :=
+by rw [Union_union_distrib, Union_const]
+
+theorem union_Union_right [inhabited ι] (s : set β) (t : ι → set β) :
+  (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
+by rw [Union_union_distrib, Union_const]
+
+theorem inter_Inter_left [inhabited ι] (s : set β) (t : ι → set β) :
+  s ∩ (⋂ i, t i) = ⋂ i, s ∩ t i :=
+by rw [Inter_inter_distrib, Inter_const]
+
+theorem inter_Inter_right [inhabited ι] (s : set β) (t : ι → set β) :
+  (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
+by rw [Inter_inter_distrib, Inter_const]
 
 -- classical
-theorem union_distrib_Inter_left (s : set β) (t : α → set β) :
+theorem union_Inter_left (s : set β) (t : ι → set β) :
   s ∪ (⋂ i, t i) = ⋂ i, s ∪ t i :=
-set.ext $ assume x, by simp [classical.forall_or_distrib_left]
+ext $ assume x, by simp [classical.forall_or_distrib_left]
+
+theorem diff_Union_right (s : set β) (t : ι → set β) :
+  (⋃ i, t i) \ s = ⋃ i, t i \ s :=
+inter_Union_right _ _
+
+theorem diff_Union_left [inhabited ι] (s : set β) (t : ι → set β) :
+  s \ (⋃ i, t i) = ⋂ i, s \ t i :=
+by rw [diff_eq, compl_Union, inter_Inter_left]; refl
+
+theorem diff_Inter_left (s : set β) (t : ι → set β) :
+  s \ (⋂ i, t i) = ⋃ i, s \ t i :=
+by rw [diff_eq, compl_Inter, inter_Union_left]; refl
 
 /- bounded unions and intersections -/
 
@@ -150,9 +193,6 @@ theorem subset_bInter {s : set α} {t : set β} {u : α → set β} (h : ∀ x 
 show t ≤ (⨅ x ∈ s, u x), -- TODO: should not be necessary when sets' order is based on lattices
   from le_infi $ assume x, le_infi (h x)
 
-theorem subset_Union {ι : Sort*} (u : ι → set α) (i : ι) : u i ⊆ (⋃i, u i) :=
-show u i ≤ (⨆i, u i), from le_supr u i
-
 theorem subset_bUnion_of_mem {s : set α} {u : α → set β} {x : α} (xs : x ∈ s) :
   u x ⊆ (⋃ x ∈ s, u x) :=
 show u x ≤ (⨆ x ∈ s, u x),
@@ -179,6 +219,12 @@ theorem bInter_subset_bInter_right {s : set α} {t1 t2 : α → set β}
   (h : ∀ x ∈ s, t1 x ⊆ t2 x) : (⋂ x ∈ s, t1 x) ⊆ (⋂ x ∈ s, t2 x) :=
 subset_bInter (λ x xs, subset.trans (bInter_subset_of_mem xs) (h x xs))
 
+theorem bUnion_eq_Union (s : set α) (t : α → set β) : (⋃ x ∈ s, t x) = (⋃ x : s, t x.1) :=
+set.ext $ by simp
+
+theorem bInter_eq_Inter (s : set α) (t : α → set β) : (⋂ x ∈ s, t x) = (⋂ x : s, t x.1) :=
+set.ext $ by simp
+
 @[simp] theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=
 show (⨅x ∈ (∅ : set α), u x) = ⊤, -- simplifier should be able to rewrite x ∈ ∅ to false.
   from infi_emptyset
@@ -246,39 +292,40 @@ ext (λ x, by simp [classical.not_forall])
 
 prefix `⋂₀`:110 := sInter
 
-theorem mem_sUnion {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :
+theorem mem_sUnion_of_mem {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :
   x ∈ ⋃₀ S :=
 ⟨t, ⟨ht, hx⟩⟩
 
-@[simp] theorem mem_sUnion_eq {x : α} {S : set (set α)} : x ∈ ⋃₀ S = (∃t ∈ S, x ∈ t) := rfl
+@[simp] theorem mem_sUnion {x : α} {S : set (set α)} : x ∈ ⋃₀ S ↔ ∃t ∈ S, x ∈ t := iff.rfl
 
 -- is this theorem really necessary?
 theorem not_mem_of_not_mem_sUnion {x : α} {t : set α} {S : set (set α)}
-    (hx : x ∉ ⋃₀ S) (ht : t ∈ S) :
-  x ∉ t :=
-assume : x ∈ t,
-have x ∈ ⋃₀ S, from mem_sUnion this ht,
-show false, from hx this
-
-theorem mem_sInter {x : α} {t : set α} {S : set (set α)} (h : ∀ t ∈ S, x ∈ t) : x ∈ ⋂₀ S := h
+  (hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t :=
+λ h, hx ⟨t, ht, h⟩
 
-@[simp] theorem mem_sInter_eq {x : α} {S : set (set α)} : x ∈ ⋂₀ S = (∀ t ∈ S, x ∈ t) := rfl
+@[simp] theorem mem_sInter {x : α} {S : set (set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t := iff.rfl
 
-theorem sInter_subset_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : (⋂₀ S) ⊆ t :=
+theorem sInter_subset_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : ⋂₀ S ⊆ t :=
 Inf_le tS
 
-theorem subset_sUnion_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : t ⊆ (⋃₀ S) :=
+theorem subset_sUnion_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : t ⊆ ⋃₀ S :=
 le_Sup tS
 
 theorem sUnion_subset {S : set (set α)} {t : set α} (h : ∀t' ∈ S, t' ⊆ t) : (⋃₀ S) ⊆ t :=
 Sup_le h
 
-theorem sUnion_subset_iff {s : set (set α)} {t : set α} : (⋃₀ s) ⊆ t ↔ ∀t' ∈ s, t' ⊆ t :=
+theorem sUnion_subset_iff {s : set (set α)} {t : set α} : ⋃₀ s ⊆ t ↔ ∀t' ∈ s, t' ⊆ t :=
 ⟨assume h t' ht', subset.trans (subset_sUnion_of_mem ht') h, sUnion_subset⟩
 
 theorem subset_sInter {S : set (set α)} {t : set α} (h : ∀t' ∈ S, t ⊆ t') : t ⊆ (⋂₀ S) :=
 le_Inf h
 
+theorem sUnion_subset_sUnion {S T : set (set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T :=
+sUnion_subset $ λ s hs, subset_sUnion_of_mem (h hs)
+
+theorem sInter_subset_sInter {S T : set (set α)} (h : S ⊆ T) : ⋂₀ T ⊆ ⋂₀ S :=
+subset_sInter $ λ s hs, sInter_subset_of_mem (h hs)
+
 @[simp] theorem sUnion_empty : ⋃₀ ∅ = (∅ : set α) := Sup_empty
 
 @[simp] theorem sInter_empty : ⋂₀ ∅ = (univ : set α) := Inf_empty
@@ -327,15 +374,22 @@ by rw [←compl_compl (⋂₀ S), compl_sInter]
 theorem inter_empty_of_inter_sUnion_empty {s t : set α} {S : set (set α)} (hs : t ∈ S)
     (h : s ∩ ⋃₀ S = ∅) :
   s ∩ t = ∅ :=
-eq_empty_of_subset_empty
-  begin rw ←h, apply inter_subset_inter_left, apply subset_sUnion_of_mem hs end
+eq_empty_of_subset_empty $ by rw ← h; exact
+inter_subset_inter_right _ (subset_sUnion_of_mem hs)
 
-theorem Union_eq_sUnion_image (s : α → set β) : (⋃ i, s i) = ⋃₀ (range s) :=
+theorem Union_eq_sUnion_range (s : α → set β) : (⋃ i, s i) = ⋃₀ (range s) :=
 by rw [← image_univ, sUnion_image]; simp
 
-theorem Inter_eq_sInter_image {α I : Type} (s : I → set α) : (⋂ i, s i) = ⋂₀ (range s) :=
+theorem Inter_eq_sInter_range {α I : Type} (s : I → set α) : (⋂ i, s i) = ⋂₀ (range s) :=
 by rw [← image_univ, sInter_image]; simp
 
+theorem range_sigma_eq_Union_range {γ : α → Type*} (f : sigma γ → β) :
+  range f = ⋃ a, range (λ b, f ⟨a, b⟩) :=
+set.ext $ by simp
+
+theorem Union_eq_range_sigma (s : α → set β) : (⋃ i, s i) = range (λ a : Σ i, s i, a.2) :=
+by simp [set.ext_iff]
+
 lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) :=
 sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht'
 
@@ -349,11 +403,23 @@ lemma Union_subset_Union2 {ι₂ : Sort*} {s : ι → set α} {t : ι₂ → set
 lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) :=
 @supr_le_supr_const (set α) ι ι₂ _ s h
 
-lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=
+lemma sUnion_eq_bUnion {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=
+set.ext $ by simp
+
+lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h : i ∈ s), i) :=
 set.ext $ by simp
 
-lemma sUnion_eq_Union' {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i) :=
-set.ext $ λ x, by simp; unfold_coes; simp
+lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i.1) :=
+set.ext $ λ x, by simp
+
+lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i.1) :=
+set.ext $ λ x, by simp
+
+lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
+set.ext $ λ x, by simp [bool.exists_bool, or_comm]
+
+lemma inter_eq_Inter {s₁ s₂ : set α} : s₁ ∩ s₂ = ⋂ b : bool, cond b s₁ s₂ :=
+set.ext $ λ x, by simp [bool.forall_bool, and_comm]
 
 instance : complete_boolean_algebra (set α) :=
 { neg                 := compl,
@@ -371,51 +437,7 @@ instance : complete_boolean_algebra (set α) :=
     by simp [-and_imp, and.left_comm],
   ..set.lattice_set }
 
-theorem union_sdiff_same {a b : set α} : a ∪ (b \ a) = a ∪ b :=
-lattice.sup_sub_same
-
-theorem sdiff_union_same {a b : set α} : (b \ a) ∪ a = a ∪ b :=
-by rw [union_comm, union_sdiff_same]
-
-theorem sdiff_inter_same {a b : set α} : (b \ a) ∩ a = ∅ :=
-set.ext $ by simp [iff_def] {contextual:=tt}
-
-theorem sdiff_subset_sdiff {a b c d : set α} : a ⊆ c → d ⊆ b → a \ b ⊆ c \ d :=
-@lattice.sub_le_sub (set α) _ _ _ _ _
-
-@[simp] theorem union_same_compl {a : set α} : a ∪ (-a) = univ :=
-sup_neg_eq_top
-
-@[simp] theorem sdiff_singleton_eq_same {a : α} {s : set α} (h : a ∉ s) : s \ {a} = s :=
-sub_eq_left $ eq_empty_iff_forall_not_mem.2 $ assume x ⟨ht, ha⟩,
-  begin simp at ha, simp [ha] at ht, exact h ht end
-
-@[simp] theorem insert_sdiff_singleton {a : α} {s : set α} :
-  insert a (s \ {a}) = insert a s :=
-by simp [insert_eq, union_sdiff_same]
-
-lemma compl_subset_compl_iff_subset {α : Type u} {x y : set α} : - y ⊆ - x ↔ x ⊆ y :=
-@neg_le_neg_iff_le (set α) _ _ _
-
-lemma union_of_subset_right {a b : set α} (h : a ⊆ b) : a ∪ b = b :=
-sup_of_le_right h
-
-section sdiff
-
-variables {s s₁ s₂ : set α}
-
-@[simp] lemma sdiff_empty : s \ ∅ = s :=
-set.ext $ by simp
-
-lemma sdiff_eq: s₁ \ s₂ = s₁ ∩ -s₂ := rfl
-
-lemma union_sdiff_left : (s₁ ∪ s₂) \ s₂ = s₁ \ s₂ :=
-set.ext $ by simp [or_and_distrib_right]
-
-lemma union_sdiff_right : (s₂ ∪ s₁) \ s₂ = s₁ \ s₂ :=
-set.ext $ by simp [or_and_distrib_right]
-
-end sdiff
+@[simp] theorem sub_eq_diff (s t : set α) : s - t = s \ t := rfl
 
 section
 
@@ -507,19 +529,28 @@ section disjoint
 variable [semilattice_inf_bot α]
 /-- Two elements of a lattice are disjoint if their inf is the bottom element.
   (This generalizes disjoint sets, viewed as members of the subset lattice.) -/
-def disjoint (a b : α) : Prop := a ⊓ b = ⊥
+def disjoint (a b : α) : Prop := a ⊓ b ≤ ⊥
 
-theorem disjoint_symm {a b : α} : disjoint a b → disjoint b a :=
-assume : a ⊓ b = ⊥, show b ⊓ a = ⊥, from this ▸ inf_comm
+theorem disjoint.eq_bot {a b : α} (h : disjoint a b) : a ⊓ b = ⊥ :=
+eq_bot_iff.2 h
 
-@[simp] lemma disjoint_comm {a b : α} : disjoint a b ↔ disjoint b a :=
-⟨disjoint_symm, disjoint_symm⟩
+theorem disjoint_iff {a b : α} : disjoint a b ↔ a ⊓ b = ⊥ :=
+eq_bot_iff.symm
 
-theorem disjoint_bot_left {a : α} : disjoint ⊥ a := bot_inf_eq
-theorem disjoint_bot_right {a : α} : disjoint a ⊥ := inf_bot_eq
+theorem disjoint.comm {a b : α} : disjoint a b ↔ disjoint b a :=
+by rw [disjoint, disjoint, inf_comm]
+
+theorem disjoint.symm {a b : α} : disjoint a b → disjoint b a :=
+disjoint.comm.1
+
+theorem disjoint_bot_left {a : α} : disjoint ⊥ a := disjoint_iff.2 bot_inf_eq
+theorem disjoint_bot_right {a : α} : disjoint a ⊥ := disjoint_iff.2 inf_bot_eq
 
 end disjoint
 
+theorem set.disjoint_diff {a b : set α} : disjoint a (b \ a) :=
+disjoint_iff.2 (inter_diff_self _ _)
+
 section
 open set
 set_option eqn_compiler.zeta true
@@ -532,8 +563,7 @@ have injective f,
   have b_eq : b₁ = b₂, from congr_arg subtype.val eq,
   have a_eq : a₁ = a₂, from classical.by_contradiction $ assume ne,
     have b₁ ∈ t a₁ ∩ t a₂, from ⟨hb₁, b_eq.symm ▸ hb₂⟩,
-    have t a₁ ∩ t a₂ ≠ ∅, from ne_empty_of_mem this,
-    this $ h _ ha₁ _ ha₂ ne,
+    h _ ha₁ _ ha₂ ne this,
   sigma.eq (subtype.eq a_eq) (subtype.eq $ by subst b_eq; subst a_eq),
 have surjective f,
   from assume ⟨b, hb⟩,
diff --git a/linear_algebra/basic.lean b/linear_algebra/basic.lean
index 6eb14ef9606dd..7cb2828ffe66a 100644
--- a/linear_algebra/basic.lean
+++ b/linear_algebra/basic.lean
@@ -178,7 +178,7 @@ span_eq is_submodule_span (set.insert_subset.mpr ⟨h, subset_span⟩) (span_mon
 lemma span_insert : span (insert b s) = {z | ∃a, ∃x∈span s, z = a • b + x } :=
 set.ext $ assume b',
 begin
-  apply iff.intro; simp [insert_eq, span_union, span_singleton, set.ext_iff, range, -add_comm],
+  split; simp [insert_eq, span_union, span_singleton, set.ext_iff, range, -add_comm],
   exact (assume y a eq_y x hx eq, ⟨a, x, hx, by simp [eq_y, eq]⟩),
   exact (assume a b₂ hb₂ eq, ⟨a • b, ⟨a, rfl⟩, b₂, hb₂, eq⟩)
 end
diff --git a/logic/schroeder_bernstein.lean b/logic/schroeder_bernstein.lean
index ba43717647c3b..52a4f5a0c00c4 100644
--- a/logic/schroeder_bernstein.lean
+++ b/logic/schroeder_bernstein.lean
@@ -23,8 +23,8 @@ theorem schroeder_bernstein {f : α → β} {g : β → α}
 let s : set α := lfp $ λs, - (g '' - (f '' s)) in
 have hs : s = - (g '' - (f '' s)),
   from lfp_eq $ assume s t h,
-    compl_subset_compl_iff_subset.mpr $ image_subset _ $
-    compl_subset_compl_iff_subset.mpr $ image_subset _ h,
+    compl_subset_compl.mpr $ image_subset _ $
+    compl_subset_compl.mpr $ image_subset _ h,
 
 have hns : - s = g '' - (f '' s),
   from lattice.neg_eq_neg_of_eq $ by simp [hs.symm],
diff --git a/order/filter.lean b/order/filter.lean
index 37494974bde36..dfe1e4fc1c0d9 100644
--- a/order/filter.lean
+++ b/order/filter.lean
@@ -823,7 +823,7 @@ lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ (infi f).
 begin
   have hs' : s ∈ (Inf {a : filter α | ∃ (i : ι), a = f i}).sets := hs,
   rw [Inf_sets_eq_finite] at hs',
-  simp only [mem_Union_eq] at hs',
+  simp only [mem_Union] at hs',
   rcases hs' with ⟨is, ⟨fin_is, his⟩, hs⟩, revert his s,
   refine finite.induction_on fin_is _ (λ fi is fi_ne_is fin_is ih, _); intros his s hs' hs,
   { rw [Inf_empty, mem_top_sets_iff] at hs, subst hs, assumption },
@@ -947,7 +947,7 @@ le_principal_iff.mp $ show f.lift g ≤ principal s,
 
 lemma mem_lift_sets (hg : monotone g) {s : set β} :
   s ∈ (f.lift g).sets ↔ (∃t∈f.sets, s ∈ (g t).sets) :=
-by rw [lift_sets_eq hg]; simp only [mem_Union_eq]
+by rw [lift_sets_eq hg]; simp only [mem_Union]
 
 lemma lift_le {f : filter α} {g : set α → filter β} {h : filter β} {s : set α}
   (hs : s ∈ f.sets) (hg : g s ≤ h) : f.lift g ≤ h :=
@@ -1086,7 +1086,7 @@ le_antisymm
         (assume s₁ s₂ hs₁ hs₂, le_trans hs₂ $ g_mono hs₁),
     begin
       rw [lift_sets_eq g_mono],
-      simp only [mem_Union_eq, exists_imp_distrib],
+      simp only [mem_Union, exists_imp_distrib],
       exact assume t ht hs, this t ht hs
     end)
 
@@ -1211,7 +1211,7 @@ le_antisymm
   (assume s,
   begin
     rw [lift_sets_eq hg],
-    simp only [mem_Union_eq, exists_imp_distrib, infi_sets_eq hf hι],
+    simp only [mem_Union, exists_imp_distrib, infi_sets_eq hf hι],
     exact assume t i ht hs, mem_infi_sets i $ mem_lift ht hs
   end)
 
diff --git a/order/galois_connection.lean b/order/galois_connection.lean
index 5152ff69637a2..dd523dc94ebe7 100644
--- a/order/galois_connection.lean
+++ b/order/galois_connection.lean
@@ -5,7 +5,7 @@ Author: Johannes Hölzl
 
 Galois connections - order theoretic adjoints.
 -/
-import order data.set
+import order.bounds
 open function set lattice
 
 universes u v w x