diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean
index abda72dc4..58cd7873a 100644
--- a/library/data/set/finite.lean
+++ b/library/data/set/finite.lean
@@ -134,7 +134,7 @@ by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto)
 
 theorem finite_powerset (s : set A) [fins : finite s] : finite (𝒫 s) :=
 assert H : (𝒫 s) = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))],
-  from setext (take t, iff.intro
+  from ext (take t, iff.intro
     (suppose t ∈ 𝒫 s,
       assert t ⊆ s, from this,
       assert finite t, from finite_subset this,
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index b0ad975ea..8d4bf969b 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -22,7 +22,7 @@ notation f `'[`:max a `]` := image f a
 
 theorem image_eq_image_of_eq_on {f1 f2 : X → Y} {a : set X} (H1 : eq_on f1 f2 a) :
   f1 '[a] = f2 '[a] :=
-setext (take y, iff.intro
+ext (take y, iff.intro
   (assume H2,
     obtain x (H3 : x ∈ a ∧ f1 x = y), from H2,
     have H4 : x ∈ a, from and.left H3,
@@ -42,7 +42,7 @@ theorem mem_image_of_mem (f : X → Y) {x : X} {a : set X} (H : x ∈ a) : f x 
 mem_image H rfl
 
 lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
-setext (take z,
+ext (take z,
   iff.intro
     (assume Hz : z ∈ (f ∘ g) '[a],
       obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
@@ -60,7 +60,7 @@ mem_image (H Hx₁) Hx₂
 
 theorem image_union (f : X → Y) (s t : set X) :
   image f (s ∪ t) = image f s ∪ image f t :=
-setext (take y, iff.intro
+ext (take y, iff.intro
   (assume H : y ∈ image f (s ∪ t),
     obtain x [(xst : x ∈ s ∪ t) (fxy : f x = y)], from H,
     or.elim xst
diff --git a/library/theories/group_theory/subgroup.lean b/library/theories/group_theory/subgroup.lean
index f0edb7aed..288392140 100644
--- a/library/theories/group_theory/subgroup.lean
+++ b/library/theories/group_theory/subgroup.lean
@@ -84,7 +84,7 @@ lemma lmul_inj_on (a : A) (H : set A) : inj_on (lmul_by a) H :=
       inj_on_of_left_inv_on (lmul_inv_on a H)
 
 lemma glcoset_eq_lcoset a (H : set A) : a ∘> H = coset.l a H :=
-      setext
+      ext
       begin
       intro x,
       rewrite [↑glcoset, ↑coset.l, ↑image, ↑set_of, ↑mem, ↑coset.lmul],
@@ -103,7 +103,7 @@ lemma glcoset_eq_lcoset a (H : set A) : a ∘> H = coset.l a H :=
 lemma grcoset_eq_rcoset a (H : set A) : H <∘ a = coset.r a H :=
       begin
         rewrite [↑grcoset, ↑coset.r, ↑image, ↑coset.rmul, ↑set_of],
-        apply setext, rewrite ↑mem,
+        apply ext, rewrite ↑mem,
         intro x,
         apply iff.intro,
           show H (x * a⁻¹) → (∃ (x_1 : A), H x_1 ∧ x_1 * a = x), from
@@ -215,14 +215,14 @@ lemma subgroup_coset_id : ∀ a, a ∈ H → (a ∘> H = H ∧ H <∘ a = H) :=
       assert Pr : H <∘ a ⊆ H, from closed_rcontract a H subg_mul_closed PHa,
       assert PHainv : H a⁻¹, from subg_has_inv a PHa,
       and.intro
-      (setext (assume x,
+      (ext (assume x,
         begin
           esimp [glcoset, mem],
           apply iff.intro,
             apply Pl,
             intro PHx, exact (subg_mul_closed a⁻¹ x PHainv PHx)
         end))
-      (setext (assume x,
+      (ext (assume x,
         begin
           esimp [grcoset, mem],
           apply iff.intro,