diff --git a/analysis/measure_theory/measurable_space.lean b/analysis/measure_theory/measurable_space.lean
index cd3976b125caa..747d12d441c6f 100644
--- a/analysis/measure_theory/measurable_space.lean
+++ b/analysis/measure_theory/measurable_space.lean
@@ -458,7 +458,7 @@ inductive generate_has (s : set (set α)) : set α → Prop
 | basic : ∀t∈s, generate_has t
 | empty : generate_has ∅
 | compl : ∀{a}, generate_has a → generate_has (-a)
-| Union : ∀{f:ℕ → set α}, (∀i j, i ≠ j → f i ∩ f j = ∅) →
+| Union : ∀{f:ℕ → set α}, (∀i j, i ≠ j → f i ∩ f j ⊆ ∅) →
     (∀i, generate_has (f i)) → generate_has (⋃i, f i)
 
 def generate (s : set (set α)) : dynkin_system α :=
@@ -479,7 +479,7 @@ let f := [s₁, s₂].inth in
 have hf0 : f 0 = s₁, from rfl,
 have hf1 : f 1 = s₂, from rfl,
 have hf2 : ∀n:ℕ, f n.succ.succ = ∅, from assume n, rfl,
-have (∀i j, i ≠ j → f i ∩ f j = ∅),
+have (∀i j, i ≠ j → f i ∩ f j ⊆ ∅),
   from assume i, i.two_step_induction
     (assume j, j.two_step_induction (by simp) (by simp [hf0, hf1, h]) (by simp [hf2]))
     (assume j, j.two_step_induction (by simp [hf0, hf1, h, inter_comm]) (by simp) (by simp [hf2]))
@@ -532,15 +532,15 @@ def restrict_on {s : set δ} (h : d.has s) : dynkin_system δ :=
     have -t ∩ s = (- (t ∩ s)) \ -s,
       from set.ext $ assume x, by by_cases x ∈ s; simp [h],
     by rw [this]; from d.has_sdiff (d.has_compl hts) (d.has_compl h)
-      (compl_subset_compl_iff_subset.mpr $ inter_subset_right _ _),
+      (compl_subset_compl.mpr $ inter_subset_right _ _),
   has_Union := assume f hd hf,
     begin
-      rw [inter_comm, inter_distrib_Union_left],
+      rw [inter_comm, inter_Union_left],
       apply d.has_Union,
       exact assume i j h,
-        have f i ∩ f j = ∅, from hd i j h,
+        have f i ∩ f j = ∅, from subset_empty_iff.1 (hd i j h),
         calc s ∩ f i ∩ (s ∩ f j) = s ∩ s ∩ (f i ∩ f j) : by cc
-          ... = ∅ : by rw [this]; simp,
+          ... ⊆ ∅ : by rw [this]; simp,
       intro i, rw [inter_comm], exact hf i
     end }
 
@@ -581,7 +581,7 @@ lemma induction_on_inter {C : set α → Prop} {s : set (set α)} {m : measurabl
   (h_eq : m = generate_from s)
   (h_inter : ∀t₁ t₂, t₁ ∈ s → t₂ ∈ s → t₁ ∩ t₂ ≠ ∅ → t₁ ∩ t₂ ∈ s)
   (h_empty : C ∅) (h_basic : ∀t∈s, C t) (h_compl : ∀t, m.is_measurable t → C t → C (- t))
-  (h_union : ∀f:ℕ → set α, (∀i j, i ≠ j → f i ∩ f j = ∅) →
+  (h_union : ∀f:ℕ → set α, (∀i j, i ≠ j → f i ∩ f j ⊆ ∅) →
     (∀i, m.is_measurable (f i)) → (∀i, C (f i)) → C (⋃i, f i)) :
   ∀{t}, m.is_measurable t → C t :=
 have eq : m.is_measurable = dynkin_system.generate_has s,
diff --git a/analysis/measure_theory/measure_space.lean b/analysis/measure_theory/measure_space.lean
index c89fa06f425bc..0d2586b45f012 100644
--- a/analysis/measure_theory/measure_space.lean
+++ b/analysis/measure_theory/measure_space.lean
@@ -66,12 +66,10 @@ have hd : pairwise (disjoint on s),
   match i, j, h with
   | 0, 0, h := (h rfl).elim
   | 0, (nat.succ 0), h := hd
-  | (nat.succ 0), 0, h := show s₂ ⊓ s₁ = ⊥, by rw [inf_comm]; assumption
+  | (nat.succ 0), 0, h := hd.symm
   | (nat.succ 0), (nat.succ 0), h := (h rfl).elim
-  | (nat.succ (nat.succ i)), j, h :=
-    begin simp [s, disjoint, (on), option.get_or_else]; exact set.empty_inter _ end
-  | i, (nat.succ (nat.succ j)), h :=
-    begin simp [s, disjoint, (on), option.get_or_else]; exact set.inter_empty _ end
+  | (nat.succ (nat.succ i)), j, h := disjoint_bot_left
+  | i, (nat.succ (nat.succ j)), h := disjoint_bot_right
   end,
 have Un_s : (⋃n, s n) = s₁ ∪ s₂,
   from subset.antisymm
@@ -90,7 +88,7 @@ have hms : ∀n, is_measurable (s n),
 calc μ.measure' (s₁ ∪ s₂) = μ.measure' (⋃n, s n) : by rw [Un_s]
   ... = (∑n, μ.measure' (s n)) :
     measure_space.measure'_Union μ hd hms
-  ... = (range (nat.succ (nat.succ 0))).sum (λn, μ.measure' (s n)) :
+  ... = (finset.range (nat.succ (nat.succ 0))).sum (λn, μ.measure' (s n)) :
     tsum_eq_sum $ assume n hn,
     match n, hn with
     | 0,                     h := by simp at h; contradiction
@@ -102,7 +100,7 @@ calc μ.measure' (s₁ ∪ s₂) = μ.measure' (⋃n, s n) : by rw [Un_s]
 
 protected lemma measure'_mono (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) (hs : s₁ ⊆ s₂) :
   μ.measure' s₁ ≤ μ.measure' s₂ :=
-have hd : s₁ ∩ (s₂ \ s₁) = ∅, from set.ext $ by simp [mem_sdiff] {contextual:=tt},
+have hd : s₁ ∩ (s₂ \ s₁) ⊆ ∅, by simp [set.subset_def, mem_sdiff] {contextual:=tt},
 have hu : s₁ ∪ (s₂ \ s₁) = s₂,
   from set.ext $ assume x, by by_cases x ∈ s₁; simp [mem_sdiff, h, @hs x] {contextual:=tt},
 calc μ.measure' s₁ ≤ μ.measure' s₁ + μ.measure' (s₂ \ s₁) :
@@ -217,9 +215,9 @@ have eq₁ : (⋃b∈i, s b) = (⋃i, g i),
       subset_bUnion_of_mem hb),
 have hd : pairwise (disjoint on g),
   from assume n m h,
-  set.eq_empty_of_subset_empty $ calc g n ∩ g m =
+  calc g n ∩ g m =
       (⋃b (h : b ∈ i) (h : f b = n) b' (h : b' ∈ i) (h : f b' = m), s b ∩ s b') :
-        by simp [g, inter_distrib_Union_left, inter_distrib_Union_right]
+        by simp [g, inter_Union_left, inter_Union_right]
       ... ⊆ ∅ :
         bUnion_subset $ assume b hb, Union_subset $ assume hbn,
         bUnion_subset $ assume b' hb', Union_subset $ assume hbm,
@@ -227,9 +225,7 @@ have hd : pairwise (disjoint on g),
           from assume h_eq,
           have f b = f b', from congr_arg f h_eq,
           by simp [hbm, hbn, h] at this; assumption,
-        have s b ∩ s b' = ∅,
-          from hd b hb b' hb' this,
-        by rw [this]; exact subset.refl _,
+        hd b hb b' hb' this,
 have hm : ∀n, is_measurable (g n),
   from assume n,
   by_cases
@@ -268,13 +264,13 @@ calc μ (⋃b, s b) = μ (⋃b∈(univ:set β), s b) :
 
 lemma measure_sdiff {s₁ s₂ : set α} (h : s₂ ⊆ s₁) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂)
   (h_fin : μ s₁ < ⊤) : μ (s₁ \ s₂) = μ s₁ - μ s₂ :=
-have hd : disjoint (s₁ \ s₂) s₂, from sdiff_inter_same,
+have hd : disjoint (s₁ \ s₂) s₂, from disjoint_diff.symm,
 have μ s₂ < ⊤, from lt_of_le_of_lt (measure_mono h) h_fin,
 calc μ (s₁ \ s₂) = (μ (s₁ \ s₂) + μ s₂) - μ s₂ :
     by rw [ennreal.add_sub_self this]
   ... = μ (s₁ \ s₂ ∪ s₂) - μ s₂ :
     by rw [measure_union hd]; simp [is_measurable_sdiff, h₁, h₂]
-  ... = _ : by rw [sdiff_union_same, union_of_subset_right h]
+  ... = _ : by rw [diff_union_self, union_eq_self_of_subset_right h]
 
 lemma measure_Union_eq_supr_nat {s : ℕ → set α} (h : ∀i, is_measurable (s i)) (hs : monotone s) :
   μ (⋃i, s i) = (⨆i, μ (s i)) :=
@@ -286,11 +282,11 @@ begin
   case nat.succ : i ih {
     rw [range_succ, sum_insert, ih, ←measure_union],
     { show μ (disjointed s (i + 1) ∪ s i) = μ (s (i + 1)),
-      rw [disjointed_of_mono hs, sdiff_union_same, union_of_subset_right],
+      rw [disjointed_of_mono hs, diff_union_self, union_eq_self_of_subset_right],
       exact hs (nat.le_succ _) },
     { show disjoint (disjointed s (i + 1)) (s i),
       simp [disjoint, disjointed_of_mono hs],
-      exact sdiff_inter_same },
+      exact diff_inter_self },
     { exact is_measurable_disjointed h },
     { exact h _ },
     { exact not_mem_range_self } }
@@ -318,7 +314,7 @@ have sub : (⋃i, s 0 \ s i) ⊆ s 0,
 have hd : ∀i, is_measurable (s 0 \ s i), from assume i, is_measurable_sdiff (h 0) (h i),
 have hu : is_measurable (⋃i, s 0 \ s i), from is_measurable_Union hd,
 have hm : monotone (λ (i : ℕ), s 0 \ s i),
-  from assume i j h, sdiff_subset_sdiff (subset.refl _) (hs i j h),
+  from assume i j h, diff_subset_diff (subset.refl _) (hs i j h),
 have eq₂ : ∀i, μ (s 0) - (μ (s 0) - μ (s i)) = μ (s i),
   from assume i,
   have μ (s i) ≤ μ (s 0), from measure_mono (hs _ _ $ nat.zero_le _),
@@ -356,7 +352,7 @@ assume s hs, outer_measure.caratheodory_is_measurable $ assume t, by_cases
     have hst₁ : is_measurable (t ∩ s), from is_measurable_inter this hs,
     have hst₂ : is_measurable (t \ s), from is_measurable_sdiff this hs,
     have t_eq : (t ∩ s) ∪ (t \ s) = t, from set.ext $ assume x, by by_cases x∈s; simp [h],
-    have h : (t ∩ s) ∩ (t \ s) = ∅, from set.ext $ by simp {contextual:=tt},
+    have h : (t ∩ s) ∩ (t \ s) ⊆ ∅, by simp [set.subset_def] {contextual:=tt},
     by rw [← μ.measure_eq_measure' this, ← μ.measure_eq_measure' hst₁, ← μ.measure_eq_measure' hst₂,
            ← measure_union h hst₁ hst₂, t_eq])
   (assume : ¬ is_measurable t, le_infi $ assume h, false.elim $ this h)
@@ -406,8 +402,8 @@ if hf : measurable f then
     measure_of_Union := assume s hs h,
       have h' : pairwise (disjoint on λ (i : ℕ), f ⁻¹' s i),
         from assume i j hij,
-        have s i ∩ s j = ∅, from h i j hij,
-        show f ⁻¹' s i ∩ f ⁻¹' s j = ∅, by rw [← preimage_inter, this, preimage_empty],
+        have s i ∩ s j = ∅, from subset_empty_iff.1 (h i j hij),
+        show f ⁻¹' s i ∩ f ⁻¹' s j ⊆ ∅, by rw [← preimage_inter, this, preimage_empty],
       by rw [preimage_Union]; exact measure_Union_nat h' (assume i, hf (s i) (hs i)) }
 else 0
 
@@ -435,9 +431,7 @@ def dirac (a : α) : measure_space α :=
       let ⟨i, hi⟩ := this in
       have ∀j, (a ∈ f j) ↔ (i = j), from
         assume j, ⟨assume hj, classical.by_contradiction $ assume hij,
-            have eq: f i ∩ f j = ∅, from h i j hij,
-            have a ∈ f i ∩ f j, from ⟨hi, hj⟩,
-            (mem_empty_eq a).mp $ by rwa [← eq],
+            h i j hij ⟨hi, hj⟩,
           assume h, h ▸ hi⟩,
       by simp [this])
     (by simp [ennreal.bot_eq_zero] {contextual := tt}) }
diff --git a/analysis/measure_theory/outer_measure.lean b/analysis/measure_theory/outer_measure.lean
index a3b0f1507ca30..beca3a9fee0d6 100644
--- a/analysis/measure_theory/outer_measure.lean
+++ b/analysis/measure_theory/outer_measure.lean
@@ -230,9 +230,9 @@ variables {s s₁ s₂ : set α}
 
 private def C (s : set α) := ∀t, μ t = μ (t ∩ s) + μ (t \ s)
 
-@[simp] private lemma C_empty : C ∅ := by simp [C, m.empty, sdiff_empty]
+@[simp] private lemma C_empty : C ∅ := by simp [C, m.empty, diff_empty]
 
-private lemma C_compl : C s₁ → C (- s₁) := by simp [C, sdiff_eq]
+private lemma C_compl : C s₁ → C (- s₁) := by simp [C, diff_eq]
 
 @[simp] private lemma C_compl_iff : C (- s) ↔ C s :=
 ⟨assume h, let h' := C_compl h in by simp at h'; assumption, C_compl⟩
@@ -244,15 +244,15 @@ have e₁ : (s₁ ∪ s₂) ∩ s₁ ∩ s₂ = s₁ ∩ s₂,
 have e₂ : (s₁ ∪ s₂) ∩ s₁ ∩ -s₂ = s₁ ∩ -s₂,
   from set.ext $ assume x, by simp [iff_def] {contextual := tt},
 calc μ t = μ (t ∩ s₁ ∩ s₂) + μ (t ∩ s₁ ∩ -s₂) + μ (t ∩ -s₁ ∩ s₂) + μ (t ∩ -s₁ ∩ -s₂) :
-    by rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁)]; simp [sdiff_eq]
+    by rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁)]; simp [diff_eq]
   ... = μ (t ∩ ((s₁ ∪ s₂) ∩ s₁ ∩ s₂)) + μ (t ∩ ((s₁ ∪ s₂) ∩ s₁ ∩ -s₂)) +
       μ (t ∩ s₂ ∩ -s₁) + μ (t ∩ -s₁ ∩ -s₂) :
     by rw [e₁, e₂]; simp
   ... = ((μ (t ∩ (s₁ ∪ s₂) ∩ s₁ ∩ s₂) + μ ((t ∩ (s₁ ∪ s₂) ∩ s₁) \ s₂)) +
       μ (t ∩ ((s₁ ∪ s₂) \ s₁))) + μ (t \ (s₁ ∪ s₂)) :
-    by rw [union_sdiff_right]; simp [sdiff_eq]
+    by rw [union_diff_left]; simp [diff_eq]; simp
   ... = μ (t ∩ (s₁ ∪ s₂)) + μ (t \ (s₁ ∪ s₂)) :
-    by rw [h₁ (t ∩ (s₁ ∪ s₂)), h₂ ((t ∩ (s₁ ∪ s₂)) ∩ s₁)]; simp [sdiff_eq]
+    by rw [h₁ (t ∩ (s₁ ∪ s₂)), h₂ ((t ∩ (s₁ ∪ s₂)) ∩ s₁)]; simp [diff_eq]
 
 private lemma C_Union_lt {s : ℕ → set α} : ∀{n:ℕ}, (∀i<n, C (s i)) → C (⋃i<n, s i)
 | 0       h := by simp [nat.not_lt_zero]
@@ -275,8 +275,8 @@ begin
     have disj : ∀x i, x ∈ s n → i < n → x ∉ s i,
       from assume x i hn h hi,
       have hx : x ∈ s i ∩ s n, from ⟨hi, hn⟩,
-      have s i ∩ s n = ∅, from hd _ _ (ne_of_lt h),
-      by rwa [this] at hx,
+      have s i ∩ s n ⊆ ∅, from hd _ _ (ne_of_lt h),
+      this hx,
     have : (⋃i<n+1, s i) \ (⋃i<n, s i) = s n,
     { apply set.ext, intro x, simp,
       constructor,
@@ -286,7 +286,7 @@ begin
       from assume hx, ⟨⟨n, nat.lt_succ_self _, hx⟩, assume i, disj x i hx⟩ },
     have e₁ : t ∩ s n = (t ∩ ⋃i<n+1, s i) \ ⋃i<n, s i,
       from calc t ∩ s n = t ∩ ((⋃i<n+1, s i) \ (⋃i<n, s i)) : by rw [this]
-        ... = (t ∩ ⋃i<n+1, s i) \ ⋃i<n, s i : by simp [sdiff_eq],
+        ... = (t ∩ ⋃i<n+1, s i) \ ⋃i<n, s i : by simp [diff_eq],
     have : (⋃i<n+1, s i) ∩ (⋃i<n, s i) = (⋃i<n, s i),
       from (inf_of_le_right $ supr_le_supr $ assume i, supr_le_supr_const $
         assume hin, lt_trans hin (nat.lt_succ_self n)),
@@ -295,7 +295,7 @@ begin
         ... = _ : by simp,
     have : C _ (⋃i<n, s i),
       from C_Union_lt m (assume i _, h i),
-    from calc (range (nat.succ n)).sum (λi, μ (t ∩ s i)) = μ (t ∩ s n) + μ (t ∩ ⋃i < n, s i) :
+    from calc (finset.range (nat.succ n)).sum (λi, μ (t ∩ s i)) = μ (t ∩ s n) + μ (t ∩ ⋃i < n, s i) :
         by simp [range_succ, sum_insert, lt_irrefl, ih]
       ... = μ ((t ∩ ⋃i<n+1, s i) ∩ ⋃i<n, s i) + μ ((t ∩ ⋃i<n+1, s i) \ ⋃i<n, s i) :
         by rw [e₁, e₂]; simp
@@ -312,13 +312,13 @@ suffices μ t ≥ μ (t ∩ (⋃i, s i)) + μ (t \ (⋃i, s i)),
       ... ≤ μ (t ∩ (⋃i, s i)) + μ (t \ (⋃i, s i)) : m.subadditive)
     this,
 have hp : μ (t ∩ ⋃i, s i) ≤ (⨆n, μ (t ∩ ⋃i<n, s i)),
-  from calc μ (t ∩ ⋃i, s i) = μ (⋃i, t ∩ s i) : by rw [inter_distrib_Union_left]
+  from calc μ (t ∩ ⋃i, s i) = μ (⋃i, t ∩ s i) : by rw [inter_Union_left]
     ... ≤ ∑i, μ (t ∩ s i) : m.Union_nat _
     ... = ⨆n, (finset.range n).sum (λi, μ (t ∩ s i)) : ennreal.tsum_eq_supr_nat
     ... = ⨆n, μ (t ∩ ⋃i<n, s i) : congr_arg _ $ funext $ assume n, C_sum h hd,
 have hn : ∀n, μ (t \ (⋃i<n, s i)) ≥ μ (t \ (⋃i, s i)),
   from assume n,
-    m.mono $ sdiff_subset_sdiff (subset.refl t) $ bUnion_subset $ assume i _, le_supr s i,
+    m.mono $ diff_subset_diff (subset.refl t) $ bUnion_subset $ assume i _, le_supr s i,
 calc μ (t ∩ (⋃i, s i)) + μ (t \ (⋃i, s i)) ≤ (⨆n, μ (t ∩ ⋃i<n, s i)) + μ (t \ (⋃i, s i)) :
     add_le_add' hp (le_refl _)
   ... = (⨆n, μ (t ∩ ⋃i<n, s i) + μ (t \ (⋃i, s i))) :
@@ -373,9 +373,9 @@ le_antisymm
       o.subadditive)
   (le_infi $ assume f, le_infi $ assume hf,
     have h₁ : t ∩ s ⊆ ⋃i, f i ∩ s,
-      by rw [←inter_distrib_Union_right]; from inter_subset_inter hf (subset.refl s),
+      by rw [← inter_Union_right]; from inter_subset_inter hf (subset.refl s),
     have h₂ : t \ s ⊆ ⋃i, f i \ s,
-      from subset.trans (sdiff_subset_sdiff hf (subset.refl s)) $
+      from subset.trans (diff_subset_diff hf (subset.refl s)) $
         by simp [set.subset_def] {contextual := tt},
     calc om (t ∩ s) + om (t \ s) ≤ (∑i, m (f i ∩ s)) + (∑i, m (f i \ s)) :
         add_le_add'
diff --git a/analysis/topology/topological_space.lean b/analysis/topology/topological_space.lean
index 23d73c9cfee36..c8b75303a1c2f 100644
--- a/analysis/topology/topological_space.lean
+++ b/analysis/topology/topological_space.lean
@@ -1121,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₂⟩
 
diff --git a/data/finset.lean b/data/finset.lean
index 4bab04b629bcc..ffd322cda3bdd 100644
--- a/data/finset.lean
+++ b/data/finset.lean
@@ -383,6 +383,9 @@ instance : lattice (finset α) :=
   inf_le_right := assume a b, inter_subset_right,
   ..finset.partial_order }
 
+@[simp] theorem sup_eq_union (s t : finset α) : s ⊔ t = s ∪ t := rfl
+@[simp] theorem inf_eq_inter (s t : finset α) : s ⊓ t = s ∩ t := rfl
+
 instance : semilattice_inf_bot (finset α) :=
 { bot := ∅, bot_le := empty_subset, ..finset.lattice.lattice }
 
@@ -1276,14 +1279,14 @@ end sort
 section disjoint
 variable [decidable_eq α]
 
-theorem disjoint_iff_inter_eq_empty {s t : finset α} : disjoint s t ↔ s ∩ t = ∅ :=
-iff.rfl
-
 theorem disjoint_left {s t : finset α} : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
-by simp [disjoint_iff_inter_eq_empty, ext, mem_inter]
+by simp [_root_.disjoint, subset_iff]; refl
+
+theorem disjoint_iff_inter_eq_empty {s t : finset α} : disjoint s t ↔ s ∩ t = ∅ :=
+disjoint_iff
 
 theorem disjoint_right {s t : finset α} : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s :=
-by rw [_root_.disjoint_comm, disjoint_left]
+by rw [disjoint.comm, disjoint_left]
 
 theorem disjoint_iff_ne {s t : finset α} : disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b :=
 by simp [disjoint_left, imp_not_comm]
@@ -1294,15 +1297,15 @@ disjoint_left.2 (λ x m₁, (disjoint_left.1 d) (h m₁))
 theorem disjoint_of_subset_right {s t u : finset α} (h : t ⊆ u) (d : disjoint s u) : disjoint s t :=
 disjoint_right.2 (λ x m₁, (disjoint_right.1 d) (h m₁))
 
-@[simp] theorem disjoint_empty_left (s : finset α) : disjoint ∅ s := bot_inf_eq
+@[simp] theorem disjoint_empty_left (s : finset α) : disjoint ∅ s := disjoint_bot_left
 
-@[simp] theorem disjoint_empty_right (s : finset α) : disjoint s ∅ := inf_bot_eq
+@[simp] theorem disjoint_empty_right (s : finset α) : disjoint s ∅ := disjoint_bot_right
 
 @[simp] theorem singleton_disjoint {s : finset α} {a : α} : disjoint (singleton a) s ↔ a ∉ s :=
 by simp [disjoint_left]; refl
 
 @[simp] theorem disjoint_singleton {s : finset α} {a : α} : disjoint s (singleton a) ↔ a ∉ s :=
-by rw _root_.disjoint_comm; simp
+by rw disjoint.comm; simp
 
 @[simp] theorem disjoint_insert_left {a : α} {s t : finset α} :
   disjoint (insert a s) t ↔ a ∉ t ∧ disjoint s t :=
@@ -1310,7 +1313,7 @@ by simp [disjoint_left, or_imp_distrib, forall_and_distrib]; refl
 
 @[simp] theorem disjoint_insert_right {a : α} {s t : finset α} :
   disjoint s (insert a t) ↔ a ∉ s ∧ disjoint s t :=
-_root_.disjoint_comm.trans $ by simp [disjoint_insert_left]
+disjoint.comm.trans $ by rw [disjoint_insert_left, disjoint.comm]
 
 @[simp] theorem disjoint_union_left {s t u : finset α} :
   disjoint (s ∪ t) u ↔ disjoint s u ∧ disjoint t u :=
diff --git a/data/set/disjointed.lean b/data/set/disjointed.lean
index 9ea226aabea4c..1f7a77c31eb20 100644
--- a/data/set/disjointed.lean
+++ b/data/set/disjointed.lean
@@ -41,15 +41,23 @@ subset.antisymm (Union_subset_Union $ assume i, inter_subset_left _ _) $
 lemma disjointed_induct {f : ℕ → set α} {n : ℕ} {p : set α → Prop}
   (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
-  rw disjointed,
-  generalize_hyp : f n = t at h₁ ⊢,
-  induction n,
-  case nat.zero { simp [nat.not_lt_zero, h₁] },
+  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] },
   case nat.succ : n ih {
-    rw [Inter_lt_succ, inter_comm (-f n), ← inter_assoc],
-    exact h₂ _ n ih }
-end
+    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₁
 
 lemma disjointed_of_mono {f : ℕ → set α} {n : ℕ} (hf : monotone f) :
   disjointed f (n + 1) = f (n + 1) \ f n :=