diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean
index fa298939d3..d10398d9ba 100644
--- a/library/algebra/group_bigops.lean
+++ b/library/algebra/group_bigops.lean
@@ -225,8 +225,8 @@ namespace finset
         {rewrite [*Prod_empty]},
       have injg : set.inj_on g (to_set s),
         from set.inj_on_of_inj_on_of_subset H (λ x, mem_insert_of_mem a),
-      have g a ∉ g '[s], from
-        suppose g a ∈ g '[s],
+      have g a ∉ g ' s, from
+        suppose g a ∈ g ' s,
         obtain b [(bs : b ∈ s) (gbeq : g b = g a)], from exists_of_mem_image this,
         have aias : set.mem a (to_set (insert a s)),
           by rewrite to_set_insert; apply set.mem_insert a s,
@@ -240,7 +240,7 @@ namespace finset
     theorem Prod_eq_of_bij_on {C : Type} [deceqC : decidable_eq C] {s : finset A} {t : finset C}
                               (f : C → B) {g : A → C} (H : set.bij_on g (to_set s) (to_set t)) :
             (∏ j ∈ t, f j) = (∏ i ∈ s, f (g i)) :=
-    have g '[s] = t,
+    have g ' s = t,
       by apply eq_of_to_set_eq_to_set; rewrite to_set_image; exact set.image_eq_of_bij_on H,
     using this, by rewrite [-this, Prod_image f (and.left (and.right H))]
   end deceqA
@@ -362,7 +362,7 @@ section Prod
           (∏ j ∈ t, f j) = (∏ i ∈ s, f (g i)) :=
   by_cases
     (suppose finite s,
-      have g '[s] = t, from image_eq_of_bij_on H,
+      have g ' s = t, from image_eq_of_bij_on H,
       using this, by rewrite [-this, Prod_image f (and.left (and.right H))])
     (assume nfins : ¬ finite s,
       have nfint : ¬ finite t, from
diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index 74c24a7df0..595f6899eb 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -20,7 +20,8 @@ definition image (f : A → B) (s : finset A) : finset B :=
 quot.lift_on s
   (λ l, to_finset (list.map f (elt_of l)))
   (λ l₁ l₂ p, quot.sound (perm_erase_dup_of_perm (perm_map _ p)))
-notation [priority finset.prio] f `'[`:max a `]` := image f a
+
+infix [priority finset.prio] `'` := image
 
 theorem image_empty (f : A → B) : image f ∅ = ∅ :=
 rfl
@@ -87,9 +88,9 @@ ext (take z, iff.intro
     obtain x (Hx : x ∈ s) (Hgx : g x = y), from exists_of_mem_image Hy,
     mem_image Hx (by esimp; rewrite [Hgx, Hfy])))
 
-lemma image_subset {a b : finset A} (f : A → B) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
+lemma image_subset {a b : finset A} (f : A → B) (H : a ⊆ b) : f ' a ⊆ f ' b :=
 subset_of_forall
-  (take y, assume Hy : y ∈ f '[a],
+  (take y, assume Hy : y ∈ f ' a,
     obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from exists_of_mem_image Hy,
     mem_image (mem_of_subset_of_mem H Hx₁) Hx₂)
 
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index a8237cc330..45ee59ff39 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -437,10 +437,10 @@ abbreviation eq_on (f1 f2 : X → Y) (a : set X) : Prop :=
 ∀₀ x ∈ a, f1 x = f2 x
 
 definition image (f : X → Y) (a : set X) : set Y := {y : Y | ∃x, x ∈ a ∧ f x = y}
-notation f `'[`:max a `]` := image f a
+infix `'` := image
 
 theorem image_eq_image_of_eq_on {f1 f2 : X → Y} {a : set X} (H1 : eq_on f1 f2 a) :
-  f1 '[a] = f2 '[a] :=
+  f1 ' a = f2 ' a :=
 ext (take y, iff.intro
   (assume H2,
     obtain x (H3 : x ∈ a ∧ f1 x = y), from H2,
@@ -454,26 +454,26 @@ ext (take y, iff.intro
     exists.intro x (and.intro H4 H5)))
 
 theorem mem_image {f : X → Y} {a : set X} {x : X} {y : Y}
-  (H1 : x ∈ a) (H2 : f x = y) : y ∈ f '[a] :=
+  (H1 : x ∈ a) (H2 : f x = y) : y ∈ f ' a :=
 exists.intro x (and.intro H1 H2)
 
 theorem mem_image_of_mem (f : X → Y) {x : X} {a : set X} (H : x ∈ a) : f x ∈ image f a :=
 mem_image H rfl
 
-lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
+lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
 ext (take z,
   iff.intro
-    (assume Hz : z ∈ (f ∘ g) '[a],
+    (assume Hz : z ∈ (f ∘ g) ' a,
       obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
-      have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl,
-      show z ∈ f '[g '[a]], from mem_image Hgx Hx₂)
-    (assume Hz : z ∈ f '[g '[a]],
-      obtain y (Hy₁ : y ∈ g '[a]) (Hy₂ : f y = z), from Hz,
+      have Hgx : g x ∈ g ' a, from mem_image Hx₁ rfl,
+      show z ∈ f ' (g ' a), from mem_image Hgx Hx₂)
+    (assume Hz : z ∈ f ' (g 'a),
+      obtain y (Hy₁ : y ∈ g ' a) (Hy₂ : f y = z), from Hz,
       obtain x (Hz₁ : x ∈ a) (Hz₂ : g x = y),      from Hy₁,
-      show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
+      show z ∈ (f ∘ g) ' a, from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
 
-lemma image_subset {a b : set X} (f : X → Y) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
-take y, assume Hy : y ∈ f '[a],
+lemma image_subset {a b : set X} (f : X → Y) (H : a ⊆ b) : f ' a ⊆ f ' b :=
+take y, assume Hy : y ∈ f ' a,
 obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from Hy,
 mem_image (H Hx₁) Hx₂
 
@@ -501,24 +501,24 @@ eq_empty_of_forall_not_mem
     H)
 
 theorem mem_image_complement (t : set X) (S : set (set X)) :
-  t ∈ complement '[S] ↔ -t ∈ S :=
+  t ∈ complement ' S ↔ -t ∈ S :=
 iff.intro
-  (suppose t ∈ complement '[S],
+  (suppose t ∈ complement ' S,
     obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this,
     show -t ∈ S, by rewrite [-Ht, comp_comp]; exact Ht')
   (suppose -t ∈ S,
-    have -(-t) ∈ complement '[S], from mem_image_of_mem complement this,
-    show t ∈ complement '[S], from comp_comp t ▸ this)
+    have -(-t) ∈ complement 'S, from mem_image_of_mem complement this,
+    show t ∈ complement 'S, from comp_comp t ▸ this)
 
-theorem image_id (s : set X) : id '[s] = s :=
+theorem image_id (s : set X) : id ' s = s :=
 ext (take x, iff.intro
-  (suppose x ∈ id '[s],
+  (suppose x ∈ id ' s,
     obtain x' [(Hx' : x' ∈ s) (x'eq : x' = x)], from this,
     show x ∈ s, by rewrite [-x'eq]; apply Hx')
   (suppose x ∈ s, mem_image_of_mem id this))
 
 theorem complement_complement_image (S : set (set X)) :
-  complement '[complement '[S]] = S :=
+  complement ' (complement ' S) = S :=
 by rewrite [-image_compose, complement_compose_complement, image_id]
 
 end image
@@ -648,30 +648,30 @@ theorem sInter_insert (s : set X) (T : set (set X)) :
 by rewrite [insert_eq, sInter_union, sInter_singleton]
 
 theorem comp_sUnion (S : set (set X)) :
-  - ⋃₀ S = ⋂₀ (complement '[S]) :=
+  - ⋃₀ S = ⋂₀ (complement ' S) :=
 ext (take x, iff.intro
   (assume H : x ∈ -(⋃₀ S),
-    take t, suppose t ∈ complement '[S],
+    take t, suppose t ∈ complement ' S,
     obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this,
     have x ∈ -t', from suppose x ∈ t', H (mem_sUnion this Ht'),
     show x ∈ t, using this, by rewrite -Ht; apply this)
-  (assume H : x ∈ ⋂₀ (complement '[S]),
+  (assume H : x ∈ ⋂₀ (complement ' S),
     suppose x ∈ ⋃₀ S,
     obtain t [(tS : t ∈ S) (xt : x ∈ t)], from this,
-    have -t ∈ complement '[S], from mem_image_of_mem complement tS,
+    have -t ∈ complement ' S, from mem_image_of_mem complement tS,
     have x ∈ -t, from H this,
     show false, proof this xt qed))
 
 theorem sUnion_eq_comp_sInter_comp (S : set (set X)) :
-  ⋃₀ S = - ⋂₀ (complement '[S]) :=
+  ⋃₀ S = - ⋂₀ (complement ' S) :=
 by rewrite [-comp_comp, comp_sUnion]
 
 theorem comp_sInter (S : set (set X)) :
-  - ⋂₀ S = ⋃₀ (complement '[S]) :=
+  - ⋂₀ S = ⋃₀ (complement ' S) :=
 by rewrite [sUnion_eq_comp_sInter_comp, complement_complement_image]
 
 theorem sInter_eq_comp_sUnion_comp (S : set (set X)) :
-   ⋂₀ S = -(⋃₀ (complement '[S])) :=
+   ⋂₀ S = -(⋃₀ (complement ' S)) :=
 by rewrite [-comp_comp, comp_sInter]
 
 -- Union and Inter: a family of sets indexed by a type
@@ -685,26 +685,26 @@ show x ∈ c, from H i Hi
 theorem subset_Inter {I : Type} {b : I → set X} {c : set X} (H : ∀ i, c ⊆ b i) : c ⊆ ⋂ i, b i :=
 λ x cx i, H i cx
 
-theorem Union_eq_sUnion_image {X I : Type} (s : I → set X) : (⋃ i, s i) = ⋃₀ (s '[univ]) :=
+theorem Union_eq_sUnion_image {X I : Type} (s : I → set X) : (⋃ i, s i) = ⋃₀ (s ' univ) :=
 ext (take x, iff.intro
   (suppose x ∈ Union s,
     obtain i (Hi : x ∈ s i), from this,
     mem_sUnion Hi (mem_image_of_mem s trivial))
-  (suppose x ∈ sUnion (s '[univ]),
-    obtain t [(Ht : t ∈ s '[univ]) (Hx : x ∈ t)], from this,
+  (suppose x ∈ sUnion (s ' univ),
+    obtain t [(Ht : t ∈ s ' univ) (Hx : x ∈ t)], from this,
     obtain i [univi (Hi : s i = t)], from Ht,
     exists.intro i (show x ∈ s i, by rewrite Hi; apply Hx)))
 
-theorem Inter_eq_sInter_image {X I : Type} (s : I → set X) : (⋂ i, s i) = ⋂₀ (s '[univ]) :=
+theorem Inter_eq_sInter_image {X I : Type} (s : I → set X) : (⋂ i, s i) = ⋂₀ (s ' univ) :=
 ext (take x, iff.intro
   (assume H : x ∈ Inter s,
     take t,
-    suppose t ∈ s '[univ],
+    suppose t ∈ s 'univ,
     obtain i [univi (Hi : s i = t)], from this,
     show x ∈ t, by rewrite -Hi; exact H i)
-  (assume H : x ∈ ⋂₀ (s '[univ]),
+  (assume H : x ∈ ⋂₀ (s ' univ),
     take i,
-    have s i ∈ s '[univ], from mem_image_of_mem s trivial,
+    have s i ∈ s ' univ, from mem_image_of_mem s trivial,
     show x ∈ s i, from H this))
 
 theorem comp_Union {X I : Type} (s : I → set X) : - (⋃ i, s i) = (⋂ i, - s i) :=
diff --git a/library/data/set/equinumerosity.lean b/library/data/set/equinumerosity.lean
index 43f2f57d13..4d6b13f9fa 100644
--- a/library/data/set/equinumerosity.lean
+++ b/library/data/set/equinumerosity.lean
@@ -30,7 +30,7 @@ have x ∈ f x, from Hx⁻¹ ▸ this,
 show false, from `x ∉ f x` this
 
 theorem not_inj_on_pow {f : set X → X} (H : maps_to f (𝒫 A) A) : ¬ inj_on f (𝒫 A) :=
-let diag := f '[{x ∈ 𝒫 A | f x ∉ x}] in
+let diag := f ' {x ∈ 𝒫 A | f x ∉ x} in
 have diag ⊆ A, from image_subset_of_maps_to_of_subset H (sep_subset _ _),
 assume H₁ : inj_on f (𝒫 A),
 have f diag ∈ diag, from by_contradiction
@@ -83,20 +83,20 @@ open set
   /- define a sequence of sets U -/
 
   definition U : ℕ → set X
-  | U 0       := A \ g '[B]
-  | U (n + 1) := g '[f '[U n]]
+  | U 0       := A \ (g ' B)
+  | U (n + 1) := g ' (f ' (U n))
 
   lemma U_subset_A : ∀ n, U n ⊆ A
   | 0       := show U 0 ⊆ A,
                  from diff_subset _ _
-  | (n + 1) := have f '[U n] ⊆ B,
+  | (n + 1) := have f ' (U n) ⊆ B,
                  from image_subset_of_maps_to_of_subset f_maps_to (U_subset_A n),
                show U (n + 1) ⊆ A,
                  from image_subset_of_maps_to_of_subset g_maps_to this
 
   lemma g_ginv_eq {a : X} (aA : a ∈ A) (anU  : a ∉ Union U) : g (ginv a) = a :=
-  have a ∈ g '[B], from by_contradiction
-    (suppose a ∉ g '[B],
+  have a ∈ g ' B, from by_contradiction
+    (suppose a ∉ g ' B,
       have a ∈ U 0, from and.intro aA this,
       have a ∈ Union U, from exists.intro 0 this,
       show false, from anU this),
@@ -135,7 +135,7 @@ open set
              ... = g (h a₂)       : heq
              ... = g (ginv a₂)    : ha₂eq
              ... = a₂             : g_ginv_eq a₂A `a₂ ∉ Union U`,
-      have g (f a₁) ∈ g '[f '[U n]],
+      have g (f a₁) ∈ g ' (f ' (U n)),
         from mem_image_of_mem g (mem_image_of_mem f a₁Un),
       have a₂ ∈ U (n + 1),
         from `g (f a₁) = a₂` ▸ this,
@@ -186,12 +186,12 @@ open set
       begin
         cases n with n,
           {have g b ∈ U 0, from gbUn,
-            have g b ∉ g '[B], from and.right this,
-            have g b ∈ g '[B], from mem_image_of_mem g `b ∈ B`,
-            show b ∈ h '[A], from absurd `g b ∈ g '[B]` `g b ∉ g '[B]`},
+            have g b ∉ g ' B, from and.right this,
+            have g b ∈ g ' B, from mem_image_of_mem g `b ∈ B`,
+            show b ∈ h ' A, from absurd `g b ∈ g ' B` `g b ∉ g ' B`},
         {have g b ∈ U (succ n), from gbUn,
-           have g b ∈ g '[f '[U n]], from this,
-           obtain b' [(b'fUn : b' ∈ f '[U n]) (geq : g b' = g b)], from this,
+           have g b ∈ g ' (f ' (U n)), from this,
+           obtain b' [(b'fUn : b' ∈ f ' (U n)) (geq : g b' = g b)], from this,
            obtain a [(aUn : a ∈ U n) (faeq : f a = b')], from b'fUn,
            have g (f a) = g b, by rewrite [faeq, geq],
            have a ∈ A, from U_subset_A n aUn,
@@ -199,12 +199,12 @@ open set
            have f a = b, from ginj `f a ∈ B` `b ∈ B` `g (f a) = g b`,
            have a ∈ Union U, from exists.intro n aUn,
            have h a = f a, from dif_pos this,
-           show b ∈ h '[A], from mem_image `a ∈ A` (`h a = f a` ⬝ `f a = b`)}
+           show b ∈ h ' A, from mem_image `a ∈ A` (`h a = f a` ⬝ `f a = b`)}
       end)
     (suppose g b ∉ Union U,
       have eq₁ : h (g b) = ginv (g b), from dif_neg this,
       have eq₂ : ginv (g b) = b, from ginv_g_eq `b ∈ B`,
-      show b ∈ h '[A], from mem_image `g b ∈ A` (eq₁ ⬝ eq₂))
+      show b ∈ h ' A, from mem_image `g b ∈ A` (eq₁ ⬝ eq₂))
 end
 end schroeder_bernstein
 
diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean
index b47cd1fe05..b4984ac76d 100644
--- a/library/data/set/finite.lean
+++ b/library/data/set/finite.lean
@@ -93,13 +93,13 @@ theorem to_finset_sep (s : set A) (p : A → Prop) [finite s] :
 by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_sep, to_set_to_finset]
 
 theorem finite_image [instance] {B : Type} (f : A → B) (s : set A) [finite s] :
-  finite (f '[s]) :=
+  finite (f ' s) :=
 exists.intro (finset.image f (to_finset s))
   (by rewrite [finset.to_set_image, *to_set_to_finset])
 
 theorem to_finset_image {B : Type}  (f : A → B) (s : set A)
     [fins : finite s] :
-  to_finset (f '[s]) = (#finset f '[to_finset s]) :=
+  to_finset (f ' s) = (#finset f ' (to_finset s)) :=
 by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_image, to_set_to_finset]
 
 theorem finite_diff [instance] (s t : set A) [finite s] : finite (s \ t) :=
@@ -157,7 +157,7 @@ theorem finite_iff_finite_of_bij_on {B : Type} {f : A → B} {s : set A} {t : se
 iff.intro (assume fs, finite_of_bij_on bijf) (assume ft, finite_of_bij_on' bijf)
 
 theorem finite_powerset (s : set A) [finite s] : finite 𝒫 s :=
-assert H : 𝒫 s = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))],
+assert H : 𝒫 s = finset.to_set ' (finset.to_set (#finset 𝒫 (to_finset s))),
   from ext (take t, iff.intro
     (suppose t ∈ 𝒫 s,
       assert t ⊆ s, from this,
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index 7a88199676..a8f93d36f8 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -33,16 +33,16 @@ take x, assume H, trivial
 
 theorem image_subset_of_maps_to_of_subset {f : X → Y} {a : set X} {b : set Y} (mfab : maps_to f a b)
     {c : set X} (csuba : c ⊆ a) :
-  f '[c] ⊆ b :=
+  f ' c ⊆ b :=
 take y,
-suppose y ∈ f '[c],
+suppose y ∈ f ' c,
 obtain x [(xc : x ∈ c) (yeq : f x = y)], from this,
 have x ∈ a, from csuba `x ∈ c`,
 have f x ∈ b, from mfab this,
 show y ∈ b, from yeq ▸ this
 
 theorem image_subset_of_maps_to {f : X → Y} {a : set X} {b : set Y} (mfab : maps_to f a b) :
-  f '[a] ⊆ b :=
+  f ' a ⊆ b :=
 image_subset_of_maps_to_of_subset mfab (subset.refl a)
 
 /- injectivity -/
@@ -90,7 +90,7 @@ iff.intro
 
 /- surjectivity -/
 
-definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]
+definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f ' a
 
 theorem surj_on_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (eq_f1_f2 : eq_on f1 f2 a)
     (surj_f1 : surj_on f1 a b) :
@@ -127,7 +127,7 @@ iff.intro
 
 lemma image_eq_of_maps_to_of_surj_on {f : X → Y} {a : set X} {b : set Y}
     (H1 : maps_to f a b) (H2 : surj_on f a b) :
-  f '[a] = b :=
+  f ' a = b :=
 eq_of_subset_of_subset (image_subset_of_maps_to H1) H2
 
 /- bijectivity -/
@@ -163,7 +163,7 @@ match H with and.intro Hmap (and.intro Hinj Hsurj) :=
 end
 
 lemma image_eq_of_bij_on {f : X → Y} {a : set X} {b : set Y} (bfab : bij_on f a b) :
-  f '[a] = b :=
+  f ' a = b :=
 image_eq_of_maps_to_of_surj_on (and.left bfab) (and.right (and.right bfab))
 
 theorem bij_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
diff --git a/library/data/set/map.lean b/library/data/set/map.lean
index b21629b8c1..0bd1434904 100644
--- a/library/data/set/map.lean
+++ b/library/data/set/map.lean
@@ -81,7 +81,7 @@ theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g)
   map.surjective (g ∘ f) :=
 surj_on_compose Hg Hf
 
-theorem image_eq_of_surjective {f : map a b} (H : map.surjective f) : f '[a] = b :=
+theorem image_eq_of_surjective {f : map a b} (H : map.surjective f) : f ' a = b :=
 image_eq_of_maps_to_of_surj_on (map.mapsto f) H
 
 /- bijective -/
@@ -98,7 +98,7 @@ obtain Hg₁ Hg₂, from Hg,
 obtain Hf₁ Hf₂, from Hf,
 and.intro (injective_compose Hg₁ Hf₁) (surjective_compose Hg₂ Hf₂)
 
-theorem image_eq_of_bijective {f : map a b} (H : map.bijective f) : f '[a] = b :=
+theorem image_eq_of_bijective {f : map a b} (H : map.bijective f) : f ' a = b :=
 image_eq_of_surjective (proof and.right H qed)
 
 /- left inverse -/
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 7741e12edc..8a744c2dd4 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -188,6 +188,7 @@ reserve infixl ` ∩ `:70
 reserve infixl ` ∪ `:65
 reserve infix ` ⊆ `:50
 reserve infix ` ⊇ `:50
+reserve infix ` ' `:75  -- for the image of a set under a function
 
 /- other symbols -/
 
diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean
index 43ddbfba9c..d4c605a87f 100644
--- a/library/theories/analysis/real_limit.lean
+++ b/library/theories/analysis/real_limit.lean
@@ -250,7 +250,7 @@ exists.intro x
 section
 local attribute mem [quasireducible]
 -- TODO: is there a better place to put this?
-proposition image_neg_eq (X : set ℝ) : (λ x, -x) '[X] = {x | -x ∈ X} :=
+proposition image_neg_eq (X : set ℝ) : (λ x, -x) ' X = {x | -x ∈ X} :=
 set.ext (take x, iff.intro
   (assume H, obtain y [(Hy₁ : y ∈ X) (Hy₂ : -y = x)], from H,
     show -x ∈ X, by rewrite [-Hy₂, neg_neg]; exact Hy₁)
@@ -425,20 +425,20 @@ have X i ≤ X (i + (j - i)), from !this,
 by+ rewrite [add_sub_of_le `i ≤ j` at this]; exact this
 
 proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ}
-    (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X '[univ]) in ℕ :=
-let sX := sup (X '[univ]) in
+    (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) in ℕ :=
+let sX := sup (X ' univ) in
 have Xle : ∀ i, X i ≤ sX, from
   take i,
-  have ∀ x, x ∈ X '[univ] → x ≤ b, from
+  have ∀ x, x ∈ X ' univ → x ≤ b, from
     (take x, assume H,
       obtain i [H' (Hi : X i = x)], from H,
       by rewrite -Hi; exact Hb i),
   show X i ≤ sX, from le_sup (mem_image_of_mem X !mem_univ) this,
-have exX : ∃ x, x ∈ X '[univ],
+have exX : ∃ x, x ∈ X ' univ,
   from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
 take ε, assume epos : ε > 0,
 have sX - ε < sX, from !sub_lt_of_pos epos,
-obtain x' [(H₁x' : x' ∈ X '[univ]) (H₂x' : sX - ε < x')],
+obtain x' [(H₁x' : x' ∈ X ' univ) (H₂x' : sX - ε < x')],
   from exists_mem_and_lt_of_lt_sup exX this,
 obtain i [H' (Hi : X i = x')], from H₁x',
 have Hi' : ∀ j, j ≥ i → sX - ε < X j, from
@@ -488,15 +488,15 @@ begin
 end
 
 proposition converges_to_seq_inf_of_nonincreasing (nonincX : nonincreasing X) {b : ℝ}
-    (Hb : ∀ i, b ≤ X i) : X ⟶ inf (X '[univ]) in ℕ :=
-have H₁ : ∃ x, x ∈ X '[univ], from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
-have H₂ : ∀ x, x ∈ X '[univ] → b ≤ x, from
+    (Hb : ∀ i, b ≤ X i) : X ⟶ inf (X ' univ) in ℕ :=
+have H₁ : ∃ x, x ∈ X ' univ, from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
+have H₂ : ∀ x, x ∈ X ' univ → b ≤ x, from
   (take x, assume H,
     obtain i [Hi₁ (Hi₂ : X i = x)], from H,
     show b ≤ x, by rewrite -Hi₂; apply Hb i),
-have H₃ : {x : ℝ | -x ∈ X '[univ]} = {x : ℝ | x ∈ (λ n, -X n) '[univ]}, from calc
-  {x : ℝ | -x ∈ X '[univ]} = (λ y, -y) '[X '[univ]] : by rewrite image_neg_eq
-                       ... = {x : ℝ | x ∈ (λ n, -X n) '[univ]} : image_compose,
+have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, from calc
+  {x : ℝ | -x ∈ X ' univ} = (λ y, -y) ' (X ' univ) : by rewrite image_neg_eq
+                       ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_compose,
 have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i),
 begin+
   rewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX],
@@ -515,7 +515,7 @@ suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from
   using this,
     by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H',
 let  aX := (λ n, (abs x)^n),
-    iaX := inf (aX '[univ]),
+    iaX := inf (aX ' univ),
     asX := (λ n, (abs x)^(succ n)) in
 have noninc_aX : nonincreasing aX, from
   nonincreasing_of_forall_succ_le
diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean
index 0f91614a9e..464de0efc8 100644
--- a/library/theories/combinatorics/choose.lean
+++ b/library/theories/combinatorics/choose.lean
@@ -148,8 +148,8 @@ have a ∈ s, from mem_of_subset_of_mem (subset_of_mem_powerset tpows) this,
 anins this
 
 private theorem aux₃ {a : A} {s t : finset A} (anins : a ∉ s) (k : ℕ) :
-  t ∈ (insert a) '[powerset s] ∧ card t = succ k ↔
-    t ∈ (insert a) '[{t' ∈ powerset s | card t' = k}] :=
+  t ∈ (insert a) ' (powerset s) ∧ card t = succ k ↔
+    t ∈ (insert a) ' {t' ∈ powerset s | card t' = k} :=
 iff.intro
   (assume H,
     obtain H' cardt, from H,
@@ -167,13 +167,13 @@ iff.intro
     assert t'pows : t' ∈ powerset s, from mem_of_mem_sep Ht',
     assert cardt' : card t' = k, from of_mem_sep Ht',
     and.intro
-      (show t ∈ (insert a) '[powerset s], from mem_image t'pows teq)
+      (show t ∈ (insert a) ' (powerset s), from mem_image t'pows teq)
       (show card t = succ k,
         by rewrite [-teq, card_insert_of_not_mem (aux₂ anins t'pows), cardt']))
 
 private theorem aux₄ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
   {t ∈ powerset (insert a s)| card t = succ k} =
-    {t ∈ powerset s | card t = succ k} ∪ (insert a) '[{t ∈ powerset s | card t = k}] :=
+    {t ∈ powerset s | card t = succ k} ∪ (insert a) ' {t ∈ powerset s | card t = k} :=
 begin
   apply ext, intro t,
   rewrite [powerset_insert anins, mem_union_iff, *mem_sep_iff, mem_union_iff, and.right_distrib,
@@ -181,7 +181,7 @@ begin
 end
 
 private theorem aux₅ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
-  {t ∈ powerset s | card t = succ k} ∩ (insert a) '[{t ∈ powerset s | card t = k}] = ∅ :=
+  {t ∈ powerset s | card t = succ k} ∩ (insert a) ' {t ∈ powerset s | card t = k} = ∅ :=
 inter_eq_empty
   (take t, assume Ht₁ Ht₂,
     have tpows : t ∈ powerset s, from mem_of_mem_sep Ht₁,
@@ -191,7 +191,7 @@ inter_eq_empty
     show false, from anint aint)
 
 private theorem aux₆ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
-  card ((insert a) '[{t ∈ powerset s | card t = k}]) = card {t ∈ powerset s | card t = k} :=
+  card ((insert a) ' {t ∈ powerset s | card t = k}) = card {t ∈ powerset s | card t = k} :=
 have set.inj_on (insert a) (ts {t ∈ powerset s| card t = k}), from
   take t₁ t₂, assume Ht₁ Ht₂,
   assume Heq : insert a t₁ = insert a t₂,
diff --git a/library/theories/group_theory/hom.lean b/library/theories/group_theory/hom.lean
index 4c5a919471..a6ff0c9de7 100644
--- a/library/theories/group_theory/hom.lean
+++ b/library/theories/group_theory/hom.lean
@@ -75,9 +75,9 @@ theorem hom_map_inv (a : A) : f a⁻¹ = (f a)⁻¹ :=
         assert P3 : (f a⁻¹) * (f a) = (f a)⁻¹ * (f a), from eq.symm (mul.left_inv (f a)) ▸ P2,
         mul_right_cancel P3
 
-theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f '[H]) :=
+theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f ' H) :=
         assume Pclosed, assume b1, assume b2,
-        assume Pb1 : b1 ∈ f '[ H], assume Pb2 : b2 ∈ f '[ H],
+        assume Pb1 : b1 ∈ f ' H, assume Pb2 : b2 ∈ f ' H,
         obtain a1 (Pa1 : a1 ∈ H ∧ f a1 = b1), from Pb1,
         obtain a2 (Pa2 : a2 ∈ H ∧ f a2 = b2), from Pb2,
         assert Pa1a2 : a1 * a2 ∈ H, from Pclosed a1 a2 (and.left Pa1) (and.left Pa2),
@@ -115,14 +115,14 @@ variable {H : set A}
 variable [is_subgH : is_subgroup H]
 include is_subgH
 
-theorem hom_map_subgroup : is_subgroup (f '[H]) :=
-  have Pone : 1 ∈ f '[H], from mem_image (@subg_has_one _ _ H _) (hom_map_one f),
-  have Pclosed : mul_closed_on (f '[H]), from hom_map_mul_closed f H subg_mul_closed,
-  assert Pinv : ∀ b, b ∈ f '[H] → b⁻¹ ∈ f '[H], from
+theorem hom_map_subgroup : is_subgroup (f ' H) :=
+  have Pone : 1 ∈ f ' H, from mem_image (@subg_has_one _ _ H _) (hom_map_one f),
+  have Pclosed : mul_closed_on (f ' H), from hom_map_mul_closed f H subg_mul_closed,
+  assert Pinv : ∀ b, b ∈ f ' H → b⁻¹ ∈ f ' H, from
   assume b, assume Pimg,
   obtain a (Pa : a ∈ H ∧ f a = b), from Pimg,
   assert Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa),
-  assert Pfainv : (f a)⁻¹ ∈ f '[H], from mem_image Painv (hom_map_inv f a),
+  assert Pfainv : (f a)⁻¹ ∈ f ' H, from mem_image Painv (hom_map_inv f a),
     and.right Pa ▸ Pfainv,
   is_subgroup.mk Pone Pclosed Pinv
 end
diff --git a/library/theories/group_theory/subgroup.lean b/library/theories/group_theory/subgroup.lean
index 553a8a4182..c4cc018a48 100644
--- a/library/theories/group_theory/subgroup.lean
+++ b/library/theories/group_theory/subgroup.lean
@@ -17,8 +17,8 @@ variable [s : semigroup A]
 include s
 definition lmul (a : A) := λ x, a * x
 definition rmul (a : A) := λ x, x * a
-definition l a (S : set A) := (lmul a) '[S]
-definition r a (S : set A) := (rmul a) '[S]
+definition l a (S : set A) := (lmul a) ' S
+definition r a (S : set A) := (rmul a) ' S
 lemma lmul_compose : ∀ (a b : A), (lmul a) ∘ (lmul b) = lmul (a*b) :=
       take a, take b,
       funext (assume x, by
@@ -28,11 +28,11 @@ lemma rmul_compose : ∀ (a b : A), (rmul a) ∘ (rmul b) = rmul (b*a) :=
       funext (assume x, by
         rewrite [↑function.compose, ↑rmul, mul.assoc])
 lemma lcompose a b (S : set A) : l a (l b S) = l (a*b) S :=
-      calc (lmul a) '[(lmul b) '[S]] = ((lmul a) ∘ (lmul b)) '[S] : image_compose
-      ... = lmul (a*b) '[S] : lmul_compose
+      calc (lmul a) ' ((lmul b) ' S) = ((lmul a) ∘ (lmul b)) ' S : image_compose
+      ... = lmul (a*b) ' S : lmul_compose
 lemma rcompose a b (S : set A) : r a (r b S) = r (b*a) S :=
-      calc (rmul a) '[(rmul b) '[S]] = ((rmul a) ∘ (rmul b)) '[S] : image_compose
-      ... = rmul (b*a) '[S] : rmul_compose
+      calc (rmul a) ' ((rmul b) ' S) = ((rmul a) ∘ (rmul b)) ' S : image_compose
+      ... = rmul (b*a) ' S : rmul_compose
 lemma l_sub a (S H : set A) : S ⊆ H → (l a S) ⊆ (l a H) := image_subset (lmul a)
 definition l_same S (a b : A) := l a S = l b S
 definition r_same S (a b : A) := r a S = r b S
diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean
index 2175406726..2509106780 100644
--- a/library/theories/topology/basic.lean
+++ b/library/theories/topology/basic.lean
@@ -34,8 +34,8 @@ theorem Open_sUnion {S : set (set X)} (H : ∀₀ t ∈ S, Open t) : Open (⋃
 sUnion_mem_opens H
 
 theorem Open_Union {I : Type} {s : I → set X} (H : ∀ i, Open (s i)) : Open (⋃ i, s i) :=
-have ∀₀ t ∈ s '[univ], Open t,
-  from take t, suppose t ∈ s '[univ],
+have ∀₀ t ∈ s ' univ, Open t,
+  from take t, suppose t ∈ s ' univ,
     obtain i [univi (Hi : s i = t)], from this,
     show Open t, by rewrite -Hi; exact H i,
 using this, by rewrite Union_eq_sUnion_image; apply Open_sUnion this