feat(data/set/basic): more set theorems, normalize naming

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],

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

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,

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 α) :=

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

data/set/disjointed.lean

@@ -24,51 +24,39 @@ 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 :=
 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

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} :=