diff --git a/src/algebra/big_operators.lean b/src/algebra/big_operators.lean
index 8e30613f728f1..b2a66b2886cd2 100644
--- a/src/algebra/big_operators.lean
+++ b/src/algebra/big_operators.lean
@@ -850,12 +850,12 @@ theorem card_eq_sum_card_image [decidable_eq β] (f : α → β) (s : finset α)
   s.card = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :=
 by letI := classical.dec_eq α; exact
 calc s.card = ((s.image f).bind (λ a, s.filter (λ x, f x = a))).card :
-  congr_arg _ (finset.ext.2 $ λ x,
+  congr_arg _ (finset.ext $ λ x,
     ⟨λ hs, mem_bind.2 ⟨f x, mem_image_of_mem _ hs,
       mem_filter.2 ⟨hs, rfl⟩⟩,
     λ h, let ⟨a, ha₁, ha₂⟩ := mem_bind.1 h in by convert filter_subset s ha₂⟩)
 ... = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :
-  card_bind (by simp [disjoint_left, finset.ext] {contextual := tt})
+  card_bind (by simp [disjoint_left, finset.ext_iff] {contextual := tt})
 
 lemma gsmul_sum [add_comm_group β] {f : α → β} {s : finset α} (z : ℤ) :
   gsmul z (∑ a in s, f a) = ∑ a in s, gsmul z (f a) :=
@@ -972,7 +972,7 @@ calc ∏ a in s, (f a + g a)
         _ _ _
         (λ b hb, ⟨b, by cases b; finish⟩));
     intros; simp * at *; simp * at * },
-  { finish [function.funext_iff, finset.ext, subset_iff] },
+  { finish [function.funext_iff, finset.ext_iff, subset_iff] },
   { assume f hf,
     exact ⟨s.filter (λ a : α, ∃ h : a ∈ s, f a h),
       by simp, by funext; intros; simp *⟩ }
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
index 2c2943886dcf8..7a7b746f1126e 100644
--- a/src/data/complex/exponential.lean
+++ b/src/data/complex/exponential.lean
@@ -218,7 +218,7 @@ begin
   rw [← sum_sdiff (@filter_subset _ (λ k, n ≤ k) _ (range m)),
     sub_eq_iff_eq_add, ← eq_sub_iff_add_eq, add_sub_cancel'],
   refine finset.sum_congr
-    (finset.ext.2 $ λ a, ⟨λ h, by simp at *; finish,
+    (finset.ext $ λ a, ⟨λ h, by simp at *; finish,
     λ h, have ham : a < m := lt_of_lt_of_le (mem_range.1 h) hnm,
       by simp * at *⟩)
     (λ _ _, rfl),
diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index 07fefbd33a80c..581f8767f47fc 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -498,7 +498,7 @@ lemma mem_support_iff (f : Π₀ i, β i) : ∀i:ι, i ∈ f.support ↔ f i ≠
 f.mem_support_to_fun
 
 @[simp] lemma support_eq_empty {f : Π₀ i, β i} : f.support = ∅ ↔ f = 0 :=
-⟨λ H, ext $ by simpa [finset.ext] using H, by simp {contextual:=tt}⟩
+⟨λ H, ext $ by simpa [finset.ext_iff] using H, by simp {contextual:=tt}⟩
 
 instance decidable_zero : decidable_pred (eq (0 : Π₀ i, β i)) :=
 λ f, decidable_of_iff _ $ support_eq_empty.trans eq_comm
diff --git a/src/data/equiv/denumerable.lean b/src/data/equiv/denumerable.lean
index a2ee8b8416160..cac3b0a0cfcdf 100644
--- a/src/data/equiv/denumerable.lean
+++ b/src/data/equiv/denumerable.lean
@@ -220,7 +220,7 @@ have h₁ : (of_nat s n : ℕ) ∉ (range (of_nat s n)).filter s, by simp,
 have h₂ : (range (succ (of_nat s n))).filter s =
     insert (of_nat s n) ((range (of_nat s n)).filter s),
   begin
-    simp only [finset.ext, mem_insert, mem_range, mem_filter],
+    simp only [finset.ext_iff, mem_insert, mem_range, mem_filter],
     assume m,
     exact ⟨λ h, by simp only [h.2, and_true]; exact or.symm
         (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
diff --git a/src/data/finmap.lean b/src/data/finmap.lean
index 405221b0939cb..06dea05e27a8c 100644
--- a/src/data/finmap.lean
+++ b/src/data/finmap.lean
@@ -333,7 +333,7 @@ induction_on₂ s₁ s₂ $ λ _ _, mem_union
 by simp [(∪), union]
 
 theorem keys_union {s₁ s₂ : finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys :=
-induction_on₂ s₁ s₂ $ λ s₁ s₂, finset.ext' $ by simp [keys]
+induction_on₂ s₁ s₂ $ λ s₁ s₂, finset.ext $ by simp [keys]
 
 @[simp] theorem lookup_union_left {a} {s₁ s₂ : finmap β} :
   a ∈ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₁ :=
diff --git a/src/data/finset.lean b/src/data/finset.lean
index 8f7d88a6bcfa8..d126919e4b401 100644
--- a/src/data/finset.lean
+++ b/src/data/finset.lean
@@ -1,14 +1,16 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
-
-Finite sets.
+Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import data.multiset
 import tactic.monotonicity
 import tactic.apply
 
+/-!
+# Finite sets
+-/
+
 open multiset subtype nat
 
 variables {α : Type*} {β : Type*} {γ : Type*}
@@ -49,7 +51,7 @@ multiset.decidable_mem _ _
 /-- Convert a finset to a set in the natural way. -/
 instance : has_lift (finset α) (set α) := ⟨λ s, {x | x ∈ s}⟩
 
-@[simp] lemma mem_coe {a : α} {s : finset α} : a ∈ (↑s : set α) ↔ a ∈ s := iff.rfl
+@[simp, norm_cast] lemma mem_coe {a : α} {s : finset α} : a ∈ (↑s : set α) ↔ a ∈ s := iff.rfl
 
 @[simp] lemma set_of_mem {α} {s : finset α} : {a | a ∈ s} = ↑s := rfl
 
@@ -63,15 +65,15 @@ instance decidable_mem' [decidable_eq α] (a : α) (s : finset α) :
   decidable (a ∈ (↑s : set α)) := s.decidable_mem _
 
 /-! ### extensionality -/
-theorem ext {s₁ s₂ : finset α} : s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂ :=
+theorem ext_iff {s₁ s₂ : finset α} : s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂ :=
 val_inj.symm.trans $ nodup_ext s₁.2 s₂.2
 
 @[ext]
-theorem ext' {s₁ s₂ : finset α} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ :=
-ext.2
+theorem ext {s₁ s₂ : finset α} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ :=
+ext_iff.2
 
-@[simp] theorem coe_inj {s₁ s₂ : finset α} : (↑s₁ : set α) = ↑s₂ ↔ s₁ = s₂ :=
-set.ext_iff.trans ext.symm
+@[simp, norm_cast] theorem coe_inj {s₁ s₂ : finset α} : (↑s₁ : set α) = ↑s₂ ↔ s₁ = s₂ :=
+set.ext_iff.trans ext_iff.symm
 
 lemma coe_injective {α} : function.injective (coe : finset α → set α) :=
 λ s t, coe_inj.1
@@ -95,7 +97,7 @@ local attribute [trans] subset.trans superset.trans
 theorem mem_of_subset {s₁ s₂ : finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := mem_of_subset
 
 theorem subset.antisymm {s₁ s₂ : finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
-ext.2 $ λ a, ⟨@H₁ a, @H₂ a⟩
+ext $ λ a, ⟨@H₁ a, @H₂ a⟩
 
 theorem subset_iff {s₁ s₂ : finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x⦄, x ∈ s₁ → x ∈ s₂ := iff.rfl
 
@@ -126,6 +128,9 @@ show (↑s₁ : set α) ⊂ ↑s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁,
 @[simp] theorem val_lt_iff {s₁ s₂ : finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
 and_congr val_le_iff $ not_congr val_le_iff
 
+theorem ssubset_iff_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁ :=
+set.ssubset_iff_of_subset h
+
 /-! ### Nonempty -/
 
 /-- The property `s.nonempty` expresses the fact that the finset `s` is not empty. It should be used
@@ -265,10 +270,10 @@ eq_of_veq $ ndinsert_of_mem h
 insert_eq_of_mem $ mem_singleton_self _
 
 theorem insert.comm (a b : α) (s : finset α) : insert a (insert b s) = insert b (insert a s) :=
-ext.2 $ λ x, by simp only [finset.mem_insert, or.left_comm]
+ext $ λ x, by simp only [finset.mem_insert, or.left_comm]
 
 @[simp] theorem insert_idem (a : α) (s : finset α) : insert a (insert a s) = insert a s :=
-ext.2 $ λ x, by simp only [finset.mem_insert, or.assoc.symm, or_self]
+ext $ λ x, by simp only [finset.mem_insert, or.assoc.symm, or_self]
 
 @[simp] theorem insert_ne_empty (a : α) (s : finset α) : insert a s ≠ ∅ :=
 ne_empty_of_mem (mem_insert_self a s)
@@ -288,9 +293,9 @@ insert_subset.2 ⟨mem_insert_self _ _, subset.trans h (subset_insert _ _)⟩
 
 lemma ssubset_iff {s t : finset α} : s ⊂ t ↔ (∃a, a ∉ s ∧ insert a s ⊆ t) :=
 iff.intro
-  (assume ⟨h₁, h₂⟩,
-    have ∃a ∈ t, a ∉ s, by simpa only [finset.subset_iff, classical.not_forall] using h₂,
-    let ⟨a, hat, has⟩ := this in ⟨a, has, insert_subset.mpr ⟨hat, h₁⟩⟩)
+  (assume H,
+    have ∃a ∈ t, a ∉ s := set.exists_of_ssubset H,
+    let ⟨a, hat, has⟩ := this in ⟨a, has, insert_subset.mpr ⟨hat, H.1⟩⟩)
   (assume ⟨a, hat, has⟩,
     let ⟨h₁, h₂⟩ := insert_subset.mp has in
     ⟨h₂, assume h, hat $ h h₁⟩)
@@ -350,33 +355,33 @@ theorem subset_union_left (s₁ s₂ : finset α) : s₁ ⊆ s₁ ∪ s₂ := λ
 theorem subset_union_right (s₁ s₂ : finset α) : s₂ ⊆ s₁ ∪ s₂ := λ x, mem_union_right _
 
 theorem union_comm (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
-ext.2 $ λ x, by simp only [mem_union, or_comm]
+ext $ λ x, by simp only [mem_union, or_comm]
 
 instance : is_commutative (finset α) (∪) := ⟨union_comm⟩
 
 @[simp] theorem union_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
-ext.2 $ λ x, by simp only [mem_union, or_assoc]
+ext $ λ x, by simp only [mem_union, or_assoc]
 
 instance : is_associative (finset α) (∪) := ⟨union_assoc⟩
 
 @[simp] theorem union_idempotent (s : finset α) : s ∪ s = s :=
-ext.2 $ λ _, mem_union.trans $ or_self _
+ext $ λ _, mem_union.trans $ or_self _
 
 instance : is_idempotent (finset α) (∪) := ⟨union_idempotent⟩
 
 theorem union_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
-ext.2 $ λ _, by simp only [mem_union, or.left_comm]
+ext $ λ _, by simp only [mem_union, or.left_comm]
 
 theorem union_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
-ext.2 $ λ x, by simp only [mem_union, or_assoc, or_comm (x ∈ s₂)]
+ext $ λ x, by simp only [mem_union, or_assoc, or_comm (x ∈ s₂)]
 
 theorem union_self (s : finset α) : s ∪ s = s := union_idempotent s
 
 @[simp] theorem union_empty (s : finset α) : s ∪ ∅ = s :=
-ext.2 $ λ x, mem_union.trans $ or_false _
+ext $ λ x, mem_union.trans $ or_false _
 
 @[simp] theorem empty_union (s : finset α) : ∅ ∪ s = s :=
-ext.2 $ λ x, mem_union.trans $ false_or _
+ext $ λ x, mem_union.trans $ false_or _
 
 theorem insert_eq (a : α) (s : finset α) : insert a s = {a} ∪ s := rfl
 
@@ -451,32 +456,32 @@ by rw [← coe_inj, coe_inter, coe_union, set.union_inter_cancel_left]
 by rw [← coe_inj, coe_inter, coe_union, set.union_inter_cancel_right]
 
 theorem inter_comm (s₁ s₂ : finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
-ext.2 $ λ _, by simp only [mem_inter, and_comm]
+ext $ λ _, by simp only [mem_inter, and_comm]
 
 @[simp] theorem inter_assoc (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
-ext.2 $ λ _, by simp only [mem_inter, and_assoc]
+ext $ λ _, by simp only [mem_inter, and_assoc]
 
 theorem inter_left_comm (s₁ s₂ s₃ : finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
-ext.2 $ λ _, by simp only [mem_inter, and.left_comm]
+ext $ λ _, by simp only [mem_inter, and.left_comm]
 
 theorem inter_right_comm (s₁ s₂ s₃ : finset α) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
-ext.2 $ λ _, by simp only [mem_inter, and.right_comm]
+ext $ λ _, by simp only [mem_inter, and.right_comm]
 
 @[simp] theorem inter_self (s : finset α) : s ∩ s = s :=
-ext.2 $ λ _, mem_inter.trans $ and_self _
+ext $ λ _, mem_inter.trans $ and_self _
 
 @[simp] theorem inter_empty (s : finset α) : s ∩ ∅ = ∅ :=
-ext.2 $ λ _, mem_inter.trans $ and_false _
+ext $ λ _, mem_inter.trans $ and_false _
 
 @[simp] theorem empty_inter (s : finset α) : ∅ ∩ s = ∅ :=
-ext.2 $ λ _, mem_inter.trans $ false_and _
+ext $ λ _, mem_inter.trans $ false_and _
 
 @[simp] lemma inter_union_self (s t : finset α) : s ∩ (t ∪ s) = s :=
 by rw [inter_comm, union_inter_cancel_right]
 
 @[simp] theorem insert_inter_of_mem {s₁ s₂ : finset α} {a : α} (h : a ∈ s₂) :
   insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
-ext.2 $ λ x, have x = a ∨ x ∈ s₂ ↔ x ∈ s₂, from or_iff_right_of_imp $ by rintro rfl; exact h,
+ext $ λ x, have x = a ∨ x ∈ s₂ ↔ x ∈ s₂, from or_iff_right_of_imp $ by rintro rfl; exact h,
 by simp only [mem_inter, mem_insert, or_and_distrib_left, this]
 
 @[simp] theorem inter_insert_of_mem {s₁ s₂ : finset α} {a : α} (h : a ∈ s₁) :
@@ -485,7 +490,7 @@ by rw [inter_comm, insert_inter_of_mem h, inter_comm]
 
 @[simp] theorem insert_inter_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₂) :
   insert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
-ext.2 $ λ x, have ¬ (x = a ∧ x ∈ s₂), by rintro ⟨rfl, H⟩; exact h H,
+ext $ λ x, have ¬ (x = a ∧ x ∈ s₂), by rintro ⟨rfl, H⟩; exact h H,
 by simp only [mem_inter, mem_insert, or_and_distrib_right, this, false_or]
 
 @[simp] theorem inter_insert_of_not_mem {s₁ s₂ : finset α} {a : α} (h : a ∉ s₁) :
@@ -580,11 +585,11 @@ theorem mem_erase_of_ne_of_mem {a b : α} {s : finset α} : a ≠ b → a ∈ s
 by simp only [mem_erase]; exact and.intro
 
 theorem erase_insert {a : α} {s : finset α} (h : a ∉ s) : erase (insert a s) a = s :=
-ext.2 $ assume x, by simp only [mem_erase, mem_insert, and_or_distrib_left, not_and_self, false_or];
+ext $ assume x, by simp only [mem_erase, mem_insert, and_or_distrib_left, not_and_self, false_or];
 apply and_iff_right_of_imp; rintro H rfl; exact h H
 
 theorem insert_erase {a : α} {s : finset α} (h : a ∈ s) : insert a (erase s a) = s :=
-ext.2 $ assume x, by simp only [mem_insert, mem_erase, or_and_distrib_left, dec_em, true_and];
+ext $ assume x, by simp only [mem_insert, mem_erase, or_and_distrib_left, dec_em, true_and];
 apply or_iff_right_of_imp; rintro rfl; exact h
 
 theorem erase_subset_erase (a : α) {s t : finset α} (h : s ⊆ t) : erase s a ⊆ erase t a :=
@@ -624,7 +629,7 @@ lemma not_mem_sdiff_of_mem_right {a : α} {s t : finset α} (h : a ∈ t) : a 
 by simp only [mem_sdiff, h, not_true, not_false_iff, and_false]
 
 theorem sdiff_union_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : (s₂ \ s₁) ∪ s₁ = s₂ :=
-ext.2 $ λ a, by simpa only [mem_sdiff, mem_union, or_comm,
+ext $ λ a, by simpa only [mem_sdiff, mem_union, or_comm,
   or_and_distrib_left, dec_em, and_true] using or_iff_right_of_imp (@h a)
 
 theorem union_sdiff_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁ ∪ (s₂ \ s₁) = s₂ :=
@@ -653,7 +658,7 @@ by simp only [sdiff_inter_distrib_right, sdiff_self, empty_union]
 by simp only [sdiff_inter_distrib_right, sdiff_self, union_empty]
 
 @[simp] theorem sdiff_empty {s₁ : finset α} : s₁ \ ∅ = s₁ :=
-ext.2 (by simp)
+ext (by simp)
 
 @[mono]
 theorem sdiff_subset_sdiff {s₁ s₂ t₁ t₂ : finset α} (h₁ : t₁ ⊆ t₂) (h₂ : s₂ ⊆ s₁) :
@@ -668,7 +673,7 @@ sdiff_subset_sdiff (subset.refl _) (empty_subset _)
 set.ext $ λ _, mem_sdiff
 
 @[simp] theorem union_sdiff_self_eq_union {s t : finset α} : s ∪ (t \ s) = s ∪ t :=
-ext.2 $ λ a, by simp only [mem_union, mem_sdiff, or_iff_not_imp_left,
+ext $ λ a, by simp only [mem_union, mem_sdiff, or_iff_not_imp_left,
   imp_and_distrib, and_iff_left id]
 
 @[simp] theorem sdiff_union_self_eq_union {s t : finset α} : (s \ t) ∪ t = s ∪ t :=
@@ -678,13 +683,13 @@ lemma union_sdiff_symm {s t : finset α} : s ∪ (t \ s) = t ∪ (s \ t) :=
 by rw [union_sdiff_self_eq_union, union_sdiff_self_eq_union, union_comm]
 
 lemma sdiff_union_inter (s t : finset α) : (s \ t) ∪ (s ∩ t) = s :=
-by { simp only [ext, mem_union, mem_sdiff, mem_inter], tauto }
+by { simp only [ext_iff, mem_union, mem_sdiff, mem_inter], tauto }
 
 @[simp] lemma sdiff_idem (s t : finset α) : s \ t \ t = s \ t :=
-by { simp only [ext, mem_sdiff], tauto }
+by { simp only [ext_iff, mem_sdiff], tauto }
 
 lemma sdiff_eq_empty_iff_subset {s t : finset α} : s \ t = ∅ ↔ s ⊆ t :=
-by { rw [subset_iff, ext], simp }
+by { rw [subset_iff, ext_iff], simp }
 
 @[simp] lemma empty_sdiff (s : finset α) : ∅ \ s = ∅ :=
 by { rw sdiff_eq_empty_iff_subset, exact empty_subset _ }
@@ -707,10 +712,10 @@ end
 by simp [subset_iff, mem_sdiff] {contextual := tt}
 
 lemma union_sdiff_distrib (s₁ s₂ t : finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t :=
-by { simp only [ext, mem_sdiff, mem_union], tauto }
+by { simp only [ext_iff, mem_sdiff, mem_union], tauto }
 
 lemma sdiff_union_distrib (s t₁ t₂ : finset α) : s \ (t₁ ∪ t₂) = (s \ t₁) ∩ (s \ t₂) :=
-by { simp only [ext, mem_union, mem_sdiff, mem_inter], tauto }
+by { simp only [ext_iff, mem_union, mem_sdiff, mem_inter], tauto }
 
 lemma union_sdiff_self (s t : finset α) : (s ∪ t) \ t = s \ t :=
 by rw [union_sdiff_distrib, sdiff_self, union_empty]
@@ -719,10 +724,10 @@ lemma sdiff_singleton_eq_erase (a : α) (s : finset α) : s \ singleton a = eras
 by { ext, rw [mem_erase, mem_sdiff, mem_singleton], tauto }
 
 lemma sdiff_sdiff_self_left (s t : finset α) : s \ (s \ t) = s ∩ t :=
-by { simp only [ext, mem_sdiff, mem_inter], tauto }
+by { simp only [ext_iff, mem_sdiff, mem_inter], tauto }
 
 lemma inter_eq_inter_of_sdiff_eq_sdiff {s t₁ t₂ : finset α} : s \ t₁ = s \ t₂ → s ∩ t₁ = s ∩ t₂ :=
-by { simp only [ext, mem_sdiff, mem_inter], intros b c, replace b := b c, split; tauto }
+by { simp only [ext_iff, mem_sdiff, mem_inter], intros b c, replace b := b c, split; tauto }
 
 end decidable_eq
 
@@ -832,14 +837,14 @@ theorem filter_ssubset {s : finset α} : s.filter p ⊂ s ↔ ∃ x ∈ s, ¬ p
 
 theorem filter_filter (s : finset α) :
   (s.filter p).filter q = s.filter (λa, p a ∧ q a) :=
-ext.2 $ assume a, by simp only [mem_filter, and_comm, and.left_comm]
+ext $ assume a, by simp only [mem_filter, and_comm, and.left_comm]
 
 @[simp] lemma filter_true {s : finset α} [h : decidable_pred (λ _, true)] :
   @finset.filter α (λ _, true) h s = s :=
 by ext; simp
 
 @[simp] theorem filter_false {h} (s : finset α) : @filter α (λa, false) h s = ∅ :=
-ext.2 $ assume a, by simp only [mem_filter, and_false]; refl
+ext $ assume a, by simp only [mem_filter, and_false]; refl
 
 lemma filter_congr {s : finset α} (H : ∀ x ∈ s, p x ↔ q x) : filter p s = filter q s :=
 eq_of_veq $ filter_congr H
@@ -860,14 +865,14 @@ variable [decidable_eq α]
 
 theorem filter_union (s₁ s₂ : finset α) :
   (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
-ext.2 $ λ _, by simp only [mem_filter, mem_union, or_and_distrib_right]
+ext $ λ _, by simp only [mem_filter, mem_union, or_and_distrib_right]
 
 theorem filter_union_right (p q : α → Prop) [decidable_pred p] [decidable_pred q] (s : finset α) :
   s.filter p ∪ s.filter q = s.filter (λx, p x ∨ q x) :=
-ext.2 $ λ x, by simp only [mem_filter, mem_union, and_or_distrib_left.symm]
+ext $ λ x, by simp only [mem_filter, mem_union, and_or_distrib_left.symm]
 
 lemma filter_mem_eq_inter {s t : finset α} : s.filter (λ i, i ∈ t) = s ∩ t :=
-ext' $ λ i, by rw [mem_filter, mem_inter]
+ext $ λ i, by rw [mem_filter, mem_inter]
 
 theorem filter_inter {s t : finset α} : filter p s ∩ t = filter p (s ∩ t) :=
 by { ext, simp only [mem_inter, mem_filter, and.right_comm] }
@@ -881,19 +886,19 @@ by { ext x, simp, split_ifs with h; by_cases h' : x = a; simp [h, h'] }
 
 theorem filter_or [decidable_pred (λ a, p a ∨ q a)] (s : finset α) :
   s.filter (λ a, p a ∨ q a) = s.filter p ∪ s.filter q :=
-ext.2 $ λ _, by simp only [mem_filter, mem_union, and_or_distrib_left]
+ext $ λ _, by simp only [mem_filter, mem_union, and_or_distrib_left]
 
 theorem filter_and [decidable_pred (λ a, p a ∧ q a)] (s : finset α) :
   s.filter (λ a, p a ∧ q a) = s.filter p ∩ s.filter q :=
-ext.2 $ λ _, by simp only [mem_filter, mem_inter, and_comm, and.left_comm, and_self]
+ext $ λ _, by simp only [mem_filter, mem_inter, and_comm, and.left_comm, and_self]
 
 theorem filter_not [decidable_pred (λ a, ¬ p a)] (s : finset α) :
   s.filter (λ a, ¬ p a) = s \ s.filter p :=
-ext.2 $ by simpa only [mem_filter, mem_sdiff, and_comm, not_and] using λ a, and_congr_right $
+ext $ by simpa only [mem_filter, mem_sdiff, and_comm, not_and] using λ a, and_congr_right $
   λ h : a ∈ s, (imp_iff_right h).symm.trans imp_not_comm
 
 theorem sdiff_eq_filter (s₁ s₂ : finset α) :
-  s₁ \ s₂ = filter (∉ s₂) s₁ := ext.2 $ λ _, by simp only [mem_sdiff, mem_filter]
+  s₁ \ s₂ = filter (∉ s₂) s₁ := ext $ λ _, by simp only [mem_sdiff, mem_filter]
 
 theorem sdiff_eq_self (s₁ s₂ : finset α) :
   s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅ :=
@@ -1095,7 +1100,7 @@ finset.eq_of_veq erase_dup_cons
 
 @[simp] lemma to_finset_add (s t : multiset α) :
   to_finset (s + t) = to_finset s ∪ to_finset t :=
-finset.ext' $ by simp
+finset.ext $ by simp
 
 @[simp] lemma to_finset_nsmul (s : multiset α) :
   ∀(n : ℕ) (hn : n ≠ 0), (n •ℕ s).to_finset = s.to_finset
@@ -1109,7 +1114,7 @@ finset.ext' $ by simp
 
 @[simp] lemma to_finset_inter (s t : multiset α) :
   to_finset (s ∩ t) = to_finset s ∩ to_finset t :=
-finset.ext' $ by simp
+finset.ext $ by simp
 
 theorem to_finset_eq_empty {m : multiset α} : m.to_finset = ∅ ↔ m = 0 :=
 finset.val_inj.symm.trans multiset.erase_dup_eq_zero
@@ -1173,10 +1178,10 @@ calc ↑(s.map f) = f '' ↑s     : coe_map f s
 
 theorem map_to_finset [decidable_eq α] [decidable_eq β] {s : multiset α} :
   s.to_finset.map f = (s.map f).to_finset :=
-ext.2 $ λ _, by simp only [mem_map, multiset.mem_map, exists_prop, multiset.mem_to_finset]
+ext $ λ _, by simp only [mem_map, multiset.mem_map, exists_prop, multiset.mem_to_finset]
 
 @[simp] theorem map_refl : s.map (embedding.refl _) = s :=
-ext.2 $ λ _, by simpa only [mem_map, exists_prop] using exists_eq_right
+ext $ λ _, by simpa only [mem_map, exists_prop] using exists_eq_right
 
 theorem map_map {g : β ↪ γ} : (s.map f).map g = s.map (f.trans g) :=
 eq_of_veq $ by simp only [map_val, multiset.map_map]; refl
@@ -1196,22 +1201,22 @@ def map_embedding (f : α ↪ β) : finset α ↪ finset β := ⟨map f, λ s₁
 
 theorem map_filter {p : β → Prop} [decidable_pred p] :
   (s.map f).filter p = (s.filter (p ∘ f)).map f :=
-ext.2 $ λ b, by simp only [mem_filter, mem_map, exists_prop, and_assoc]; exact
+ext $ λ b, by simp only [mem_filter, mem_map, exists_prop, and_assoc]; exact
 ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, h1, h2, rfl⟩,
 by rintro ⟨x, h1, h2, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩
 
 theorem map_union [decidable_eq α] [decidable_eq β]
   {f : α ↪ β} (s₁ s₂ : finset α) : (s₁ ∪ s₂).map f = s₁.map f ∪ s₂.map f :=
-ext.2 $ λ _, by simp only [mem_map, mem_union, exists_prop, or_and_distrib_right, exists_or_distrib]
+ext $ λ _, by simp only [mem_map, mem_union, exists_prop, or_and_distrib_right, exists_or_distrib]
 
 theorem map_inter [decidable_eq α] [decidable_eq β]
   {f : α ↪ β} (s₁ s₂ : finset α) : (s₁ ∩ s₂).map f = s₁.map f ∩ s₂.map f :=
-ext.2 $ λ b, by simp only [mem_map, mem_inter, exists_prop]; exact
+ext $ λ b, by simp only [mem_map, mem_inter, exists_prop]; exact
 ⟨by rintro ⟨a, ⟨m₁, m₂⟩, rfl⟩; exact ⟨⟨a, m₁, rfl⟩, ⟨a, m₂, rfl⟩⟩,
 by rintro ⟨⟨a, m₁, e⟩, ⟨a', m₂, rfl⟩⟩; cases f.2 e; exact ⟨_, ⟨m₁, m₂⟩, rfl⟩⟩
 
 @[simp] theorem map_singleton (f : α ↪ β) (a : α) : map f {a} = {f a} :=
-ext.2 $ λ _, by simp only [mem_map, mem_singleton, exists_prop, exists_eq_left]; exact eq_comm
+ext $ λ _, by simp only [mem_map, mem_singleton, exists_prop, exists_eq_left]; exact eq_comm
 
 @[simp] theorem map_insert [decidable_eq α] [decidable_eq β]
   (f : α ↪ β) (a : α) (s : finset α) :
@@ -1258,13 +1263,13 @@ let ⟨a, ha⟩ := h in ⟨f a, mem_image_of_mem f ha⟩
 
 theorem image_to_finset [decidable_eq α] {s : multiset α} :
   s.to_finset.image f = (s.map f).to_finset :=
-ext.2 $ λ _, by simp only [mem_image, multiset.mem_to_finset, exists_prop, multiset.mem_map]
+ext $ λ _, by simp only [mem_image, multiset.mem_to_finset, exists_prop, multiset.mem_map]
 
 theorem image_val_of_inj_on (H : ∀x∈s, ∀y∈s, f x = f y → x = y) : (image f s).1 = s.1.map f :=
 multiset.erase_dup_eq_self.2 (nodup_map_on H s.2)
 
 theorem image_id [decidable_eq α] : s.image id = s :=
-ext.2 $ λ _, by simp only [mem_image, exists_prop, id, exists_eq_right]
+ext $ λ _, by simp only [mem_image, exists_prop, id, exists_eq_right]
 
 theorem image_image [decidable_eq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f) :=
 eq_of_veq $ by simp only [image_val, erase_dup_map_erase_dup_eq, multiset.map_map]
@@ -1281,23 +1286,23 @@ calc ↑(s.image f) = f '' ↑s     : coe_image
 
 theorem image_filter {p : β → Prop} [decidable_pred p] :
   (s.image f).filter p = (s.filter (p ∘ f)).image f :=
-ext.2 $ λ b, by simp only [mem_filter, mem_image, exists_prop]; exact
+ext $ λ b, by simp only [mem_filter, mem_image, exists_prop]; exact
 ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩,
  by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩
 
 theorem image_union [decidable_eq α] {f : α → β} (s₁ s₂ : finset α) :
   (s₁ ∪ s₂).image f = s₁.image f ∪ s₂.image f :=
-ext.2 $ λ _, by simp only [mem_image, mem_union, exists_prop, or_and_distrib_right,
+ext $ λ _, by simp only [mem_image, mem_union, exists_prop, or_and_distrib_right,
   exists_or_distrib]
 
 theorem image_inter [decidable_eq α] (s₁ s₂ : finset α) (hf : ∀x y, f x = f y → x = y) :
   (s₁ ∩ s₂).image f = s₁.image f ∩ s₂.image f :=
-ext.2 $ by simp only [mem_image, exists_prop, mem_inter]; exact λ b,
+ext $ by simp only [mem_image, exists_prop, mem_inter]; exact λ b,
 ⟨λ ⟨a, ⟨m₁, m₂⟩, e⟩, ⟨⟨a, m₁, e⟩, ⟨a, m₂, e⟩⟩,
  λ ⟨⟨a, m₁, e₁⟩, ⟨a', m₂, e₂⟩⟩, ⟨a, ⟨m₁, hf _ _ (e₂.trans e₁.symm) ▸ m₂⟩, e₁⟩⟩.
 
 @[simp] theorem image_singleton (f : α → β) (a : α) : image f {a} = {f a} :=
-ext.2 $ λ x, by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm
+ext $ λ x, by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm
 
 @[simp] theorem image_insert [decidable_eq α] (f : α → β) (a : α) (s : finset α) :
   (insert a s).image f = insert (f a) (s.image f) :=
@@ -1313,7 +1318,7 @@ eq_of_veq $ by rw [image_val, attach_val, multiset.attach_map_val, erase_dup_eq_
 @[simp] lemma attach_insert [decidable_eq α] {a : α} {s : finset α} :
   attach (insert a s) = insert (⟨a, mem_insert_self a s⟩ : {x // x ∈ insert a s})
     ((attach s).image (λx, ⟨x.1, mem_insert_of_mem x.2⟩)) :=
-ext.2 $ λ ⟨x, hx⟩, ⟨or.cases_on (mem_insert.1 hx)
+ext $ λ ⟨x, hx⟩, ⟨or.cases_on (mem_insert.1 hx)
   (λ h : x = a, λ _, mem_insert.2 $ or.inl $ subtype.eq h)
   (λ h : x ∈ s, λ _, mem_insert_of_mem $ mem_image.2 $ ⟨⟨x, h⟩, mem_attach _ _, subtype.eq rfl⟩),
 λ _, finset.mem_attach _ _⟩
@@ -1322,7 +1327,7 @@ theorem map_eq_image (f : α ↪ β) (s : finset α) : s.map f = s.image f :=
 eq_of_veq $ (multiset.erase_dup_eq_self.2 (s.map f).2).symm
 
 lemma image_const {s : finset α} (h : s.nonempty) (b : β) : s.image (λa, b) = singleton b :=
-ext.2 $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right,
+ext $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right,
   h.bex, true_and, mem_singleton, eq_comm]
 
 /--
@@ -1450,7 +1455,7 @@ begin
     from assume a, ⟨assume ha, let ⟨i, hi, eq⟩ := hf a ha in ⟨i, mem_range.2 hi, eq⟩,
       assume ⟨i, hi, eq⟩, eq ▸ hf' i (mem_range.1 hi)⟩,
   have : s = ((range n).attach.image $ λi, f i.1 (mem_range.1 i.2)),
-    by simpa only [ext, mem_image, exists_prop, subtype.exists, mem_attach, true_and],
+    by simpa only [ext_iff, mem_image, exists_prop, subtype.exists, mem_attach, true_and],
   calc card s = card ((range n).attach.image $ λi, f i.1 (mem_range.1 i.2)) :
       by rw [this]
     ... = card ((range n).attach) :
@@ -1517,7 +1522,7 @@ by haveI := classical.prop_decidable; exact
 calc s.card = s.attach.card : card_attach.symm
 ... = (s.attach.image (λ (a : {a // a ∈ s}), f a.1 a.2)).card :
   eq.symm (card_image_of_injective _ (λ a b h, subtype.eq (h₂ _ _ _ _ h)))
-... = t.card : congr_arg card (finset.ext.2 $ λ b,
+... = t.card : congr_arg card (finset.ext $ λ b,
     ⟨λ h, let ⟨a, ha₁, ha₂⟩ := mem_image.1 h in ha₂ ▸ h₁ _ _,
       λ h, let ⟨a, ha₁, ha₂⟩ := h₃ b h in mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
 
@@ -1591,9 +1596,9 @@ protected def bind (s : finset α) (t : α → finset β) : finset β :=
 by simp only [mem_def, bind_val, mem_erase_dup, mem_bind, exists_prop]
 
 @[simp] theorem bind_insert [decidable_eq α] {a : α} : (insert a s).bind t = t a ∪ s.bind t :=
-ext.2 $ λ x, by simp only [mem_bind, exists_prop, mem_union, mem_insert,
+ext $ λ x, by simp only [mem_bind, exists_prop, mem_union, mem_insert,
   or_and_distrib_right, exists_or_distrib, exists_eq_left]
--- ext.2 $ λ x, by simp [or_and_distrib_right, exists_or_distrib]
+-- ext $ λ x, by simp [or_and_distrib_right, exists_or_distrib]
 
 @[simp] lemma singleton_bind {a : α} : finset.bind {a} t = t a :=
 begin
@@ -1627,7 +1632,7 @@ finset.induction_on s rfl (λ a s has ih,
 
 theorem bind_to_finset [decidable_eq α] (s : multiset α) (t : α → multiset β) :
   (s.bind t).to_finset = s.to_finset.bind (λa, (t a).to_finset) :=
-ext.2 $ λ x, by simp only [multiset.mem_to_finset, mem_bind, multiset.mem_bind, exists_prop]
+ext $ λ x, by simp only [multiset.mem_to_finset, mem_bind, multiset.mem_bind, exists_prop]
 
 lemma bind_mono {t₁ t₂ : α → finset β} (h : ∀a∈s, t₁ a ⊆ t₂ a) : s.bind t₁ ⊆ s.bind t₂ :=
 have ∀b a, a ∈ s → b ∈ t₁ a → (∃ (a : α), a ∈ s ∧ b ∈ t₂ a),
@@ -1643,7 +1648,7 @@ begin
 end
 
 lemma bind_singleton {f : α → β} : s.bind (λa, {f a}) = s.image f :=
-ext.2 $ λ x, by simp only [mem_bind, mem_image, mem_singleton, eq_comm]
+ext $ λ x, by simp only [mem_bind, mem_image, mem_singleton, eq_comm]
 
 lemma image_bind_filter_eq [decidable_eq α] (s : finset β) (g : β → α) :
   (s.image g).bind (λa, s.filter $ (λc, g c = a)) = s :=
@@ -1668,7 +1673,7 @@ protected def product (s : finset α) (t : finset β) : finset (α × β) := ⟨
 
 theorem product_eq_bind [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
  s.product t = s.bind (λa, t.image $ λb, (a, b)) :=
-ext.2 $ λ ⟨x, y⟩, by simp only [mem_product, mem_bind, mem_image, exists_prop, prod.mk.inj_iff,
+ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bind, mem_image, exists_prop, prod.mk.inj_iff,
   and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left]
 
 @[simp] theorem card_product (s : finset α) (t : finset β) : card (s.product t) = card s * card t :=
@@ -1693,7 +1698,7 @@ theorem sigma_mono {s₁ s₂ : finset α} {t₁ t₂ : Πa, finset (σ a)}
 theorem sigma_eq_bind [decidable_eq α] [∀a, decidable_eq (σ a)] (s : finset α)
   (t : Πa, finset (σ a)) :
   s.sigma t = s.bind (λa, (t a).image $ λb, ⟨a, b⟩) :=
-ext.2 $ λ ⟨x, y⟩, by simp only [mem_sigma, mem_bind, mem_image, exists_prop,
+ext $ λ ⟨x, y⟩, by simp only [mem_sigma, mem_bind, mem_image, exists_prop,
   and.left_comm, exists_and_distrib_left, exists_eq_left, heq_iff_eq, exists_eq_right]
 
 end sigma
diff --git a/src/data/finsupp.lean b/src/data/finsupp.lean
index 2b214da3f14e8..c5a671cf0302e 100644
--- a/src/data/finsupp.lean
+++ b/src/data/finsupp.lean
@@ -94,7 +94,7 @@ lemma ext_iff {f g : α →₀ β} : f = g ↔ (∀a:α, f a = g a) :=
 ⟨by rintros rfl a; refl, ext⟩
 
 @[simp] lemma support_eq_empty {f : α →₀ β} : f.support = ∅ ↔ f = 0 :=
-⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext.1 h a).1 $
+⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext_iff.1 h a).1 $
   mem_support_iff.2 H, by rintro rfl; refl⟩
 
 instance finsupp.decidable_eq [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
@@ -945,7 +945,7 @@ lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid
    comap_domain f l hf.inj_on = 0 → l = 0 :=
 begin
   rw [← support_eq_empty, ← support_eq_empty, comap_domain],
-  simp only [finset.ext, finset.not_mem_empty, iff_false, mem_preimage],
+  simp only [finset.ext_iff, finset.not_mem_empty, iff_false, mem_preimage],
   assume h a ha,
   cases hf.2.2 ha with b hb,
   exact h b (hb.2.symm ▸ ha)
@@ -985,7 +985,7 @@ if_pos h
 if_neg h
 
 @[simp] lemma support_filter : (f.filter p).support = f.support.filter p :=
-finset.ext.mpr $ assume a, if H : p a
+finset.ext $ assume a, if H : p a
 then by simp only [mem_support_iff, filter_apply_pos _ _ H, mem_filter, H, and_true]
 else by simp only [mem_support_iff, filter_apply_neg _ _ H, mem_filter, H, and_false, ne.def,
   ne_self_iff_false]
@@ -1580,7 +1580,7 @@ def split_comp [has_zero γ] (g : Π i, (αs i →₀ β) → γ)
   end }
 
 lemma sigma_support : l.support = l.split_support.sigma (λ i, (l.split i).support) :=
-by simp only [finset.ext, split_support, split, comap_domain, mem_image,
+by simp only [finset.ext_iff, split_support, split, comap_domain, mem_image,
   mem_preimage, sigma.forall, mem_sigma]; tauto
 
 lemma sigma_sum [add_comm_monoid γ] (f : (Σ (i : ι), αs i) → β → γ) :
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index fa2f8369b11ff..4fc44af04bd0f 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -37,10 +37,10 @@ by ext; simp
 theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 
 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
-by simp [ext]
+by simp [ext_iff]
 
 @[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
-  univ ∩ s = s := ext' $ λ a, by simp
+  univ ∩ s = s := ext $ λ a, by simp
 
 @[simp] lemma inter_univ [decidable_eq α] (s : finset α) :
   s ∩ univ = s :=
@@ -154,7 +154,7 @@ equiv.of_bijective (mono_of_fin univ h) begin
 end
 
 instance (α : Type*) : subsingleton (fintype α) :=
-⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext, h₁, h₂]⟩
+⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext_iff, h₁, h₂]⟩
 
 protected def subtype {p : α → Prop} (s : finset α)
   (H : ∀ x : α, x ∈ s ↔ p x) : fintype {x // p x} :=
@@ -840,7 +840,7 @@ by rw [perms_of_list, list.nodup_append, list.nodup_bind, pairwise_iff_nth_le];
 def perms_of_finset (s : finset α) : finset (perm α) :=
 quotient.hrec_on s.1 (λ l hl, ⟨perms_of_list l, nodup_perms_of_list hl⟩)
   (λ a b hab, hfunext (congr_arg _ (quotient.sound hab))
-    (λ ha hb _, heq_of_eq $ finset.ext.2 $
+    (λ ha hb _, heq_of_eq $ finset.ext $
       by simp [mem_perms_of_list_iff, hab.mem_iff]))
   s.2
 
diff --git a/src/data/fintype/card.lean b/src/data/fintype/card.lean
index 1fd111c2a02e1..318726f90aea7 100644
--- a/src/data/fintype/card.lean
+++ b/src/data/fintype/card.lean
@@ -215,7 +215,7 @@ begin
   resetI,
   subst p,
   congr,
-  simp [finset.ext]
+  simp [finset.ext_iff]
 end
 
 @[to_additive] lemma finset.prod_fiberwise [fintype β] [decidable_eq β] [comm_monoid γ]
@@ -258,7 +258,7 @@ begin
   rw [← prod_sdiff (subset_univ s),
       ← @prod_image (α₁ ⊕ α₂) _ _ _ _ _ _ sum.inl,
       ← @prod_image (α₁ ⊕ α₂) _ _ _ _ _ _ sum.inr],
-  { congr, rw finset.ext, rintro (a|a);
+  { congr, rw finset.ext_iff, rintro (a|a);
     { simp only [mem_image, exists_eq, mem_sdiff, mem_univ, exists_false,
         exists_prop_of_true, not_false_iff, and_self, not_true, and_false], } },
   all_goals { intros, solve_by_elim [sum.inl.inj, sum.inr.inj], }
diff --git a/src/data/nat/multiplicity.lean b/src/data/nat/multiplicity.lean
index 13454f1c9d030..505685ec92e97 100644
--- a/src/data/nat/multiplicity.lean
+++ b/src/data/nat/multiplicity.lean
@@ -33,7 +33,7 @@ lemma multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm1 : m ≠ 1) (hn0 : 0 < n) (
 calc multiplicity m n = ↑(Ico 1 $ ((multiplicity m n).get (finite_nat_iff.2 ⟨hm1, hn0⟩) + 1)).card :
   by simp
 ... = ↑((finset.Ico 1 b).filter (λ i, m ^ i ∣ n)).card : congr_arg coe $ congr_arg card $
-  finset.ext.2 $ λ i,
+  finset.ext $ λ i,
   have hmn : ¬ m ^ n ∣ n,
     from if hm0 : m = 0
     then λ _, by cases n; simp [*, lt_irrefl, nat.pow_succ] at *
diff --git a/src/data/nat/totient.lean b/src/data/nat/totient.lean
index b3a83480e838a..ce069c0f1d9b6 100644
--- a/src/data/nat/totient.lean
+++ b/src/data/nat/totient.lean
@@ -65,7 +65,7 @@ calc ∑ m in (range n.succ).filter (∣ n), φ m
 ... = ((filter (∣ n) (range n.succ)).bind (λ d, (range n).filter (λ m, gcd n m = d))).card :
   (card_bind (by intros; apply disjoint_filter.2; cc)).symm
 ... = (range n).card :
-  congr_arg card (finset.ext.2 (λ m, ⟨by finish,
+  congr_arg card (finset.ext (λ m, ⟨by finish,
     λ hm, have h : m < n, from mem_range.1 hm,
       mem_bind.2 ⟨gcd n m, mem_filter.2 ⟨mem_range.2 (lt_succ_of_le (le_of_dvd (lt_of_le_of_lt (nat.zero_le _) h)
         (gcd_dvd_left _ _))), gcd_dvd_left _ _⟩, mem_filter.2 ⟨hm, rfl⟩⟩⟩))
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 8134bb5288d5e..8361a18fd2904 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -205,6 +205,9 @@ not_subset.1 h.2
 lemma ssubset_iff_subset_ne {s t : set α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t :=
 by split; simp [set.ssubset_def, ne.def, set.subset.antisymm_iff] {contextual := tt}
 
+lemma ssubset_iff_of_subset {s t : set α} (h : s ⊆ t) : s ⊂ t ↔ ∃ x ∈ t, x ∉ s :=
+⟨exists_of_ssubset, λ ⟨x, hxt, hxs⟩, ⟨h, λ h, hxs $ h hxt⟩⟩
+
 theorem not_mem_empty (x : α) : ¬ (x ∈ (∅ : set α)) :=
 assume h : x ∈ ∅, h
 
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index ba6201c358007..16f7cf1418408 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -126,7 +126,7 @@ end
 
 lemma to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : finite s) :
   (finite_insert a hs).to_finset = insert a hs.to_finset :=
-finset.ext.mpr $ by simp
+finset.ext $ by simp
 
 @[elab_as_eliminator]
 theorem finite.induction_on {C : set α → Prop} {s : set α} (h : finite s)
diff --git a/src/field_theory/finite.lean b/src/field_theory/finite.lean
index 4b7f44bb60b8d..ebe93ac8507c9 100644
--- a/src/field_theory/finite.lean
+++ b/src/field_theory/finite.lean
@@ -53,7 +53,7 @@ lemma card_image_polynomial_eval [fintype R] [decidable_eq R] {p : polynomial R}
   fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
 finset.card_le_mul_card_image _ _
   (λ a _, calc _ = (p - C a).roots.card : congr_arg card
-    (by simp [finset.ext, mem_roots_sub_C hp, -sub_eq_add_neg])
+    (by simp [finset.ext_iff, mem_roots_sub_C hp, -sub_eq_add_neg])
     ... ≤ _ : card_roots_sub_C' hp)
 
 /-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution. -/
diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean
index de4a39e6953b1..cab0c91ce158d 100644
--- a/src/group_theory/order_of_element.lean
+++ b/src/group_theory/order_of_element.lean
@@ -161,7 +161,7 @@ lemma sum_card_order_of_eq_card_pow_eq_one {n : ℕ} (hn : 0 < n) :
   = (finset.univ.filter (λ a : α, a ^ n = 1)).card :=
 calc ∑ m in (finset.range n.succ).filter (∣ n), (finset.univ.filter (λ a : α, order_of a = m)).card
     = _ : (finset.card_bind (by { intros, apply finset.disjoint_filter.2, cc })).symm
-... = _ : congr_arg finset.card (finset.ext.2 (begin
+... = _ : congr_arg finset.card (finset.ext (begin
   assume a,
   suffices : order_of a ≤ n ∧ order_of a ∣ n ↔ a ^ n = 1,
   { simpa [nat.lt_succ_iff], },
@@ -443,7 +443,7 @@ have h : ∑ m in (range d.succ).filter (∣ d.succ),
             nat.div_div_self hm (succ_pos _)]⟩⟩)),
 have hinsert : insert d.succ ((range d.succ).filter (∣ d.succ))
     = (range d.succ.succ).filter (∣ d.succ),
-  from (finset.ext.2 $ λ x, ⟨λ h, (mem_insert.1 h).elim (λ h, by simp [h, range_succ])
+  from (finset.ext $ λ x, ⟨λ h, (mem_insert.1 h).elim (λ h, by simp [h, range_succ])
     (by clear _let_match; simp [range_succ]; tauto), by clear _let_match; simp [range_succ] {contextual := tt}; tauto⟩),
 have hinsert₁ : d.succ ∉ (range d.succ).filter (∣ d.succ),
   by simp [mem_range, zero_le_one, le_succ],
@@ -471,7 +471,7 @@ let c := fintype.card α in
 have hc0 : 0 < c, from fintype.card_pos_iff.2 ⟨1⟩,
 lt_irrefl c $
   calc c = (univ.filter (λ a : α, a ^ c = 1)).card :
-    congr_arg card $ by simp [finset.ext, c]
+    congr_arg card $ by simp [finset.ext_iff, c]
   ... = ∑ m in (range c.succ).filter (∣ c),
       (univ.filter (λ a : α, order_of a = m)).card :
     (sum_card_order_of_eq_card_pow_eq_one hc0).symm
@@ -479,7 +479,7 @@ lt_irrefl c $
       (univ.filter (λ a : α, order_of a = m)).card :
     eq.symm (sum_subset (erase_subset _ _) (λ m hm₁ hm₂,
       have m = d, by simp at *; cc,
-      by simp [*, finset.ext] at *; exact h0))
+      by simp [*, finset.ext_iff] at *; exact h0))
   ... ≤ ∑ m in ((range c.succ).filter (∣ c)).erase d, φ m :
     sum_le_sum (λ m hm,
       have hmc : m ∣ c, by simp at hm; tauto,
diff --git a/src/group_theory/perm/sign.lean b/src/group_theory/perm/sign.lean
index 6c6885c4baa67..a0c33de13be79 100644
--- a/src/group_theory/perm/sign.lean
+++ b/src/group_theory/perm/sign.lean
@@ -191,7 +191,7 @@ end
 lemma support_swap_mul_eq [fintype α] {f : perm α} {x : α}
   (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
 have hfx : f x ≠ x, from λ hfx, by simpa [hfx] using hffx,
-finset.ext.2 $ λ y,
+finset.ext $ λ y,
 ⟨λ hy, have hy' : (swap x (f x) * f) y ≠ y, from mem_support.1 hy,
     mem_erase.2 ⟨λ hyx, by simp [hyx, mul_apply, *] at *,
     mem_support.2 $ λ hfy,
@@ -666,11 +666,11 @@ lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
   is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
 
 @[simp] lemma support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
-finset.ext.2 $ λ a, by simp [swap_apply_def]; split_ifs; cc
+finset.ext $ λ a, by simp [swap_apply_def]; split_ifs; cc
 
 lemma card_support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
 show (swap x y).support.card = finset.card ⟨x::y::0, by simp [hxy]⟩,
-from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext]; cc
+from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext_iff]; cc
 
 lemma sign_cycle [fintype α] : ∀ {f : perm α} (hf : is_cycle f),
   sign f = -(-1) ^ f.support.card
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
index 0df86458d915f..72edcc5f9be17 100644
--- a/src/linear_algebra/basis.lean
+++ b/src/linear_algebra/basis.lean
@@ -1138,8 +1138,7 @@ assume t, finset.induction_on t
           hsu, by simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
 begin
   have eq : t.filter (λx, x ∈ s) ∪ t.filter (λx, x ∉ s) = t,
-  { apply finset.ext.mpr,
-    intro x,
+  { ext1 x,
     by_cases x ∈ s; simp * },
   apply exists.elim (this (t.filter (λx, x ∉ s)) (t.filter (λx, x ∈ s))
     (by simp [set.subset_def]) (by simp [set.ext_iff] {contextual := tt}) (by rwa [eq])),
diff --git a/src/measure_theory/outer_measure.lean b/src/measure_theory/outer_measure.lean
index 8077f20215bf9..1e6c66945f97f 100644
--- a/src/measure_theory/outer_measure.lean
+++ b/src/measure_theory/outer_measure.lean
@@ -48,12 +48,12 @@ begin
     rwa [← e, mem_decode2.1 (option.get_mem (H m hm))] at this },
   { intros b h,
     refine ⟨encode b, _, _⟩,
-    { convert h, simp [ext_iff, encodek2] },
+    { convert h, simp [set.ext_iff, encodek2] },
     { exact option.get_of_mem _ (encodek2 _) } },
   { intros n h,
     transitivity, swap,
     rw [show decode2 β n = _, from option.get_mem (H n h)],
-    congr, simp [ext_iff, -option.some_get] }
+    congr, simp [set.ext_iff, -option.some_get] }
 end
 
 protected theorem Union (m : outer_measure α)
diff --git a/src/number_theory/quadratic_reciprocity.lean b/src/number_theory/quadratic_reciprocity.lean
index 8e376c96316a2..b5bb1b28820af 100644
--- a/src/number_theory/quadratic_reciprocity.lean
+++ b/src/number_theory/quadratic_reciprocity.lean
@@ -281,7 +281,7 @@ lemma div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) : a / b
   ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :=
 calc a / b = (Ico 1 (a / b).succ).card : by simp
 ... = ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card :
-  congr_arg _$ finset.ext.2 $ λ x,
+  congr_arg _ $ finset.ext $ λ x,
     have x * b ≤ a → x ≤ c,
       from λ h, le_trans (by rwa [le_div_iff_mul_le _ _ hb0]) hc,
     by simp [lt_succ_iff, le_div_iff_mul_le _ _ hb0]; tauto
@@ -292,7 +292,7 @@ private lemma sum_Ico_eq_card_lt {p q : ℕ} :
   ∑ a in Ico 1 (p / 2).succ, (a * q) / p =
   (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
   (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q)).card :=
-if hp0 : p = 0 then by simp [hp0, finset.ext]
+if hp0 : p = 0 then by simp [hp0, finset.ext_iff]
 else
   calc ∑ a in Ico 1 (p / 2).succ, (a * q) / p =
     ∑ a in Ico 1 (p / 2).succ,
@@ -348,7 +348,7 @@ have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
     ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
       (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p) =
     ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)),
-  from finset.ext.2 $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
+  from finset.ext $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
 by rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
     card_product];
   simp
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
index e811479d0c869..25f08f72b01a9 100644
--- a/src/topology/metric_space/emetric_space.lean
+++ b/src/topology/metric_space/emetric_space.lean
@@ -494,12 +494,12 @@ instance emetric_space_pi [∀b, emetric_space (π b)] : emetric_space (Πb, π
     end,
   to_uniform_space := Pi.uniform_space _,
   uniformity_edist := begin
-    simp only [Pi.uniformity, emetric_space.uniformity_edist, comap_infi, gt_iff_lt, preimage_set_of_eq,
-          comap_principal],
+    simp only [Pi.uniformity, emetric_space.uniformity_edist, comap_infi, gt_iff_lt,
+      preimage_set_of_eq, comap_principal],
     rw infi_comm, congr, funext ε,
     rw infi_comm, congr, funext εpos,
     change 0 < ε at εpos,
-    simp [ext_iff, εpos]
+    simp [set.ext_iff, εpos]
   end }
 
 end pi