diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index 46ad727fd..c29b5c746 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -76,11 +76,11 @@ namespace binary
               ... = a*((b*c)*d) : H_assoc
   end
 
-  definition right_commutative_compose_right [reducible]
-    {A B : Type} (f : A → A → A) (g : B → A) (rcomm : right_commutative f) : right_commutative (compose_right f g) :=
+  definition right_commutative_comp_right [reducible]
+    {A B : Type} (f : A → A → A) (g : B → A) (rcomm : right_commutative f) : right_commutative (comp_right f g) :=
   λ a b₁ b₂, !rcomm
 
   definition left_commutative_compose_left [reducible]
-    {A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (compose_left f g) :=
+    {A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (comp_left f g) :=
   λ a b₁ b₂, !lcomm
 end binary
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index cdc51c09b..628ace0d8 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -30,7 +30,7 @@ namespace category
   --    (λ a b f, !id_right)
   --    (λ a b f, !id_left)
 
-  infixr `∘op`:60 := @compose _ (opposite _) _ _ _
+  infixr `∘op`:60 := @comp _ (opposite _) _ _ _
 
   variables {C : Category} {a b c : C}
 
@@ -47,11 +47,11 @@ namespace category
 
   definition type_category [reducible] : category Type :=
   mk (λa b, a → b)
-     (λ a b c, function.compose)
+     (λ a b c, function.comp)
      (λ a, _root_.id)
-     (λ a b c d h g f, symm (function.compose.assoc h g f))
-     (λ a b f, function.compose.left_id f)
-     (λ a b f, function.compose.right_id f)
+     (λ a b c d h g f, symm (function.comp.assoc h g f))
+     (λ a b f, function.comp.left_id f)
+     (λ a b f, function.comp.right_id f)
 
   definition Type_category [reducible] : Category := Mk type_category
 
diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean
index 9321e7a96..9d1f0f84d 100644
--- a/library/algebra/group_bigops.lean
+++ b/library/algebra/group_bigops.lean
@@ -203,7 +203,7 @@ namespace finset
   variable [comm_semigroup B]
 
   theorem mulf_rcomm (f : A → B) : right_commutative (mulf f) :=
-  right_commutative_compose_right (@has_mul.mul B _) f (@mul.right_comm B _)
+  right_commutative_comp_right (@has_mul.mul B _) f (@mul.right_comm B _)
 
   namespace Prod_semigroup
   open Prodl_semigroup
diff --git a/library/data/equiv.lean b/library/data/equiv.lean
index 977cc0a2e..62da1c9e5 100644
--- a/library/data/equiv.lean
+++ b/library/data/equiv.lean
@@ -63,7 +63,7 @@ open equiv.ops
 lemma id_apply {A : Type} (x : A) : id ∙ x = x :=
 rfl
 
-lemma compose_apply {A B C : Type} (g : B ≃ C) (f : A ≃ B) (x : A) : (g ∘ f) ∙ x = g ∙ f ∙ x :=
+lemma comp_apply {A B C : Type} (g : B ≃ C) (f : A ≃ B) (x : A) : (g ∘ f) ∙ x = g ∙ f ∙ x :=
 begin cases g, cases f, esimp end
 
 lemma inverse_apply_apply {A B : Type} : ∀ (e : A ≃ B) (x : A), e⁻¹ ∙ e ∙ x = x
@@ -379,7 +379,7 @@ assume h₁ h₂, by rewrite [swap_apply_def, if_neg h₁, if_neg h₂]
 lemma swap_swap (a b : A) : swap a b ∘ swap a b = id :=
 eq_of_to_fun_eq (funext (λ x, begin unfold [swap, fn, equiv.trans, equiv.refl], rewrite swap_core_swap_core end))
 
-lemma swap_compose_apply (a b : A) (π : perm A) (x : A) : (swap a b ∘ π) ∙ x = if π ∙ x = a then b else if π ∙ x = b then a else π ∙ x :=
+lemma swap_comp_apply (a b : A) (π : perm A) (x : A) : (swap a b ∘ π) ∙ x = if π ∙ x = a then b else if π ∙ x = b then a else π ∙ x :=
 begin cases π, reflexivity end
 
 end swap
diff --git a/library/data/hf.lean b/library/data/hf.lean
index 89937e0a1..ccdab5c17 100644
--- a/library/data/hf.lean
+++ b/library/data/hf.lean
@@ -455,7 +455,7 @@ theorem powerset_insert {a : hf} {s : hf} : a ∉ s → 𝒫 (insert a s) = 𝒫
 begin unfold [mem, powerset, insert, union, image], rewrite [*to_finset_of_finset], intro h,
       have (λ (x : finset hf), of_finset (finset.insert a x)) = (λ (x : finset hf), of_finset (finset.insert a (to_finset (of_finset x)))), from
         funext (λ x, by rewrite to_finset_of_finset),
-      rewrite [finset.powerset_insert h, finset.image_union, -*finset.image_comp, ↑compose, this]
+      rewrite [finset.powerset_insert h, finset.image_union, -*finset.image_comp, ↑comp, this]
 end
 
 theorem mem_powerset_iff_subset (s : hf) : ∀ x : hf, x ∈ 𝒫 s ↔ x ⊆ s :=
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index 78ddebc53..e8263659f 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -118,7 +118,7 @@ assume xa : x ∈ a,
 have H : f1 x ∈ b, from maps_to_f1 xa,
 show f2 x ∈ b, from eq_on_a xa ▸ H
 
-theorem maps_to_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
+theorem maps_to_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
    (H1 : maps_to g b c) (H2 : maps_to f a b) : maps_to (g ∘ f) a c :=
 take x, assume H : x ∈ a, H1 (H2 H)
 
@@ -157,7 +157,7 @@ assume H : f2 x1 = f2 x2,
 have H' : f1 x1 = f1 x2, from eq_f1_f2 ax1 ⬝ H ⬝ (eq_f1_f2 ax2)⁻¹,
 show x1 = x2, from inj_f1 ax1 ax2 H'
 
-theorem inj_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y}
+theorem inj_on_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y}
     (fab : maps_to f a b) (Hg : inj_on g b) (Hf: inj_on f a) :
   inj_on (g ∘ f) a :=
 take x1 x2 : X,
@@ -195,7 +195,7 @@ have H2 : x ∈ a, from and.left H1,
 have H3 : f2 x = y, from (eq_f1_f2 H2)⁻¹ ⬝ and.right H1,
 exists.intro x (and.intro H2 H3)
 
-theorem surj_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
+theorem surj_on_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
   (Hg : surj_on g b c) (Hf: surj_on f a b) :
   surj_on (g ∘ f) a c :=
 take z,
@@ -260,16 +260,16 @@ lemma image_eq_of_bij_on {f : X → Y} {a : set X} {b : set Y} (bfab : bij_on f
   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}
+theorem bij_on_comp {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
   (Hg : bij_on g b c) (Hf: bij_on f a b) :
   bij_on (g ∘ f) a c :=
 match Hg with and.intro Hgmap (and.intro Hginj Hgsurj) :=
   match Hf with and.intro Hfmap (and.intro Hfinj Hfsurj) :=
     and.intro
-      (maps_to_compose Hgmap Hfmap)
+      (maps_to_comp Hgmap Hfmap)
       (and.intro
-        (inj_on_compose Hfmap Hginj Hfinj)
-        (surj_on_compose Hgsurj Hfsurj))
+        (inj_on_comp Hfmap Hginj Hfinj)
+        (surj_on_comp Hgsurj Hfsurj))
   end
 end
 
@@ -320,7 +320,7 @@ calc
      ... = g (f x2) : H1
      ... = x2       : H x2a
 
-theorem left_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
+theorem left_inv_on_comp {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
    {a : set X} {b : set Y} (fab : maps_to f a b)
     (Hf : left_inv_on f' f a) (Hg : left_inv_on g' g b) : left_inv_on (f' ∘ g') (g ∘ f) a :=
 take x : X,
@@ -353,10 +353,10 @@ have gya : g y ∈ a, from gba yb,
 have H1 : f (g y) = y, from H yb,
 exists.intro (g y) (and.intro gya H1)
 
-theorem right_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
+theorem right_inv_on_comp {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
    {c : set Z} {b : set Y} (g'cb : maps_to g' c b)
     (Hf : right_inv_on f' f b) (Hg : right_inv_on g' g c) : right_inv_on (f' ∘ g') (g ∘ f) c :=
-left_inv_on_compose g'cb Hg Hf
+left_inv_on_comp g'cb Hg Hf
 
 theorem right_inv_on_of_inj_on_of_left_inv_on {f : X → Y} {g : Y → X} {a : set X} {b : set Y}
     (fab : maps_to f a b) (gba : maps_to g b a) (injf : inj_on f a) (lfg : left_inv_on f g b) :
diff --git a/library/data/set/map.lean b/library/data/set/map.lean
index 0bd143490..69bead8a2 100644
--- a/library/data/set/map.lean
+++ b/library/data/set/map.lean
@@ -44,10 +44,10 @@ mk_equivalence (@map.equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b)
 
 /- compose -/
 
-protected definition compose (g : map b c) (f : map a b) : map a c :=
-map.mk (#function g ∘ f) (maps_to_compose (mapsto g) (mapsto f))
+protected definition comp (g : map b c) (f : map a b) : map a c :=
+map.mk (#function g ∘ f) (maps_to_comp (mapsto g) (mapsto f))
 
-notation g ∘ f := map.compose g f
+notation g ∘ f := map.comp g f
 
 /- range -/
 
@@ -64,9 +64,9 @@ theorem injective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.injective
   map.injective f2 :=
 inj_on_of_eq_on H1 H2
 
-theorem injective_compose {g : map b c} {f : map a b} (Hg : map.injective g) (Hf: map.injective f) :
+theorem injective_comp {g : map b c} {f : map a b} (Hg : map.injective g) (Hf: map.injective f) :
   map.injective (g ∘ f) :=
-inj_on_compose (mapsto f) Hg Hf
+inj_on_comp (mapsto f) Hg Hf
 
 /- surjective -/
 
@@ -76,10 +76,10 @@ theorem surjective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.surjectiv
   map.surjective f2 :=
 surj_on_of_eq_on H1 H2
 
-theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g)
+theorem surjective_comp {g : map b c} {f : map a b} (Hg : map.surjective g)
     (Hf: map.surjective f) :
   map.surjective (g ∘ f) :=
-surj_on_compose Hg Hf
+surj_on_comp Hg Hf
 
 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
@@ -92,11 +92,11 @@ theorem bijective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.bijective
   map.bijective f2 :=
 and.intro (injective_of_equiv H1 (and.left H2)) (surjective_of_equiv H1 (and.right H2))
 
-theorem bijective_compose {g : map b c} {f : map a b} (Hg : map.bijective g) (Hf: map.bijective f) :
+theorem bijective_comp {g : map b c} {f : map a b} (Hg : map.bijective g) (Hf: map.bijective f) :
   map.bijective (g ∘ f) :=
 obtain Hg₁ Hg₂, from Hg,
 obtain Hf₁ Hf₂, from Hf,
-and.intro (injective_compose Hg₁ Hf₁) (surjective_compose Hg₂ Hf₂)
+and.intro (injective_comp Hg₁ Hf₁) (surjective_comp Hg₂ Hf₂)
 
 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)
@@ -118,10 +118,10 @@ theorem injective_of_left_inverse {g : map b a} {f : map a b} (H : map.left_inve
   map.injective f :=
 inj_on_of_left_inv_on H
 
-theorem left_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
+theorem left_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
     (Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) :
   map.left_inverse (f' ∘ g') (g ∘ f) :=
-left_inv_on_compose (mapsto f) Hf Hg
+left_inv_on_comp (mapsto f) Hf Hg
 
 /- right inverse -/
 
@@ -150,10 +150,10 @@ theorem left_inverse_of_surjective_of_right_inverse {f : map a b} {g : map b a}
   map.left_inverse f g :=
 left_inv_on_of_surj_on_right_inv_on surjf rfg
 
-theorem right_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
+theorem right_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
     (Hf : map.right_inverse f' f) (Hg : map.right_inverse g' g) :
   map.right_inverse (f' ∘ g') (g ∘ f) :=
-map.left_inverse_compose Hg Hf
+map.left_inverse_comp Hg Hf
 
 theorem equiv_of_map.left_inverse_of_right_inverse {g1 g2 : map b a} {f : map a b}
   (H1 : map.left_inverse g1 f) (H2 : map.right_inverse g2 f) : g1 ~ g2 :=
diff --git a/library/data/stream.lean b/library/data/stream.lean
index ae936ca9b..f65b65887 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -595,7 +595,7 @@ infix `⊛`:75 := apply  -- input as \o*
 
 theorem identity (s : stream A) : pure id ⊛ s = s :=
 rfl
-theorem composition (g : stream (B → C)) (f : stream (A → B)) (s : stream A) : pure compose ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s) :=
+theorem composition (g : stream (B → C)) (f : stream (A → B)) (s : stream A) : pure comp ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s) :=
 rfl
 theorem homomorphism (f : A → B) (a : A) : pure f ⊛ pure a = pure (f a) :=
 rfl
diff --git a/library/init/function.lean b/library/init/function.lean
index 1110039d0..245413453 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -12,13 +12,13 @@ namespace function
 
 variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
 
-definition compose [reducible] [unfold_full] (f : B → C) (g : A → B) : A → C :=
+definition comp [reducible] [unfold_full] (f : B → C) (g : A → B) : A → C :=
 λx, f (g x)
 
-definition compose_right [reducible] [unfold_full] (f : B → B → B) (g : A → B) : B → A → B :=
+definition comp_right [reducible] [unfold_full] (f : B → B → B) (g : A → B) : B → A → B :=
 λ b a, f b (g a)
 
-definition compose_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B :=
+definition comp_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B :=
 λ a b, f (g a) b
 
 definition on_fun [reducible] [unfold_full] (f : B → B → C) (g : A → B) : A → A → C :=
@@ -31,7 +31,7 @@ definition combine [reducible] [unfold_full] (f : A → B → C) (op : C → D 
 definition const [reducible] [unfold_full] (B : Type) (a : A) : B → A :=
 λx, a
 
-definition dcompose [reducible] [unfold_full] {B : A → Type} {C : Π {x : A}, B x → Type}
+definition dcomp [reducible] [unfold_full] {B : A → Type} {C : Π {x : A}, B x → Type}
   (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
 λx, f (g x)
 
@@ -53,8 +53,8 @@ rfl
 theorem uncurry_curry (f : A × B → C) : uncurry (curry f) = f :=
 funext (λ p, match p with (a, b) := rfl end)
 
-infixr  ` ∘ `            := compose
-infixr  ` ∘' `:60        := dcompose
+infixr  ` ∘ `            := comp
+infixr  ` ∘' `:60        := dcomp
 infixl  ` on `:1         := on_fun
 infixr  ` $ `:1          := app
 notation f ` -[` op `]- ` g  := combine f op g
@@ -63,23 +63,23 @@ lemma left_id (f : A → B) : id ∘ f = f := rfl
 
 lemma right_id (f : A → B) : f ∘ id = f := rfl
 
-theorem compose.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
+theorem comp.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
 
-theorem compose.left_id (f : A → B) : id ∘ f = f := rfl
+theorem comp.left_id (f : A → B) : id ∘ f = f := rfl
 
-theorem compose.right_id (f : A → B) : f ∘ id = f := rfl
+theorem comp.right_id (f : A → B) : f ∘ id = f := rfl
 
-theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
+theorem comp_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
 
 definition injective [reducible] (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
 
-theorem injective_compose {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
+theorem injective_comp {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
   injective (g ∘ f) :=
 take a₁ a₂, assume Heq, Hf (Hg Heq)
 
 definition surjective [reducible] (f : A → B) : Prop := ∀ b, ∃ a, f a = b
 
-theorem surjective_compose {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
+theorem surjective_comp {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
   surjective (g ∘ f) :=
 take c,
   obtain b (Hb : g b = c), from Hg c,
@@ -88,11 +88,11 @@ take c,
 
 definition bijective (f : A → B) := injective f ∧ surjective f
 
-theorem bijective_compose {g : B → C} {f : A → B} (Hg : bijective g) (Hf : bijective f) :
+theorem bijective_comp {g : B → C} {f : A → B} (Hg : bijective g) (Hf : bijective f) :
   bijective (g ∘ f) :=
 obtain Hginj Hgsurj, from Hg,
 obtain Hfinj Hfsurj, from Hf,
-and.intro (injective_compose Hginj Hfinj) (surjective_compose Hgsurj Hfsurj)
+and.intro (injective_comp Hginj Hfinj) (surjective_comp Hgsurj Hfsurj)
 
 -- g is a left inverse to f
 definition left_inverse (g : B → A) (f : A → B) : Prop := ∀x, g (f x) = x
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index ecf7a72b5..43ff778e9 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -67,7 +67,7 @@ section
   theorem hproof_irrel {a b : Prop} (H : a = b) (H₁ : a) (H₂ : b) : H₁ == H₂ :=
   eq_rec_to_heq (proof_irrel (cast H H₁) H₂)
 
-  --TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
+  --TODO: generalize to eq.rec. This is a special case of rec_on_comp in eq.lean
   theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
     cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
   by subst Hab
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 4a9b5f350..52d0a292f 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -34,7 +34,7 @@ namespace eq
       eq.drec_on H b = eq.drec_on H' b :=
   proof_irrel H H' ▸ rfl
 
-  theorem rec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
+  theorem rec_on_comp {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
           (u : P a) : eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u :=
     (show ∀ H₂ : b = c, eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u,
       from eq.drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
diff --git a/library/logic/examples/leftinv_of_inj.lean b/library/logic/examples/leftinv_of_inj.lean
index a079a9874..df816efcd 100644
--- a/library/logic/examples/leftinv_of_inj.lean
+++ b/library/logic/examples/leftinv_of_inj.lean
@@ -23,7 +23,7 @@ have linv : left_inverse finv f, from
     have ex : ∃ a₁ : A, f a₁ = f a, from exists.intro a rfl,
     have h₁ : f (some ex) = f a,    from !some_spec,
     begin
-      esimp [mk_left_inv, compose, id],
+      esimp [mk_left_inv, comp, id],
       rewrite [dif_pos ex],
       exact (!inj h₁)
     end,
diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean
index 6a0810b89..fe044a84a 100644
--- a/library/theories/group_theory/action.lean
+++ b/library/theories/group_theory/action.lean
@@ -114,7 +114,7 @@ assume Pgstab,
 have hom g a = a, from of_mem_sep Pgstab, calc
   hom (f*g) a = perm.f ((hom f) * (hom g)) a : is_hom hom
           ... = ((hom f) ∘ (hom g)) a        : by rewrite perm_f_mul
-          ... = (hom f) a                    : by unfold compose; rewrite this
+          ... = (hom f) a                    : by unfold comp; rewrite this
 
 lemma stab_subset : stab hom H a ⊆ H :=
       begin
@@ -126,7 +126,7 @@ assume Pg,
 have hom g a = hom h a, from of_mem_sep Pg, calc
   hom (h⁻¹*g) a = perm.f ((hom h⁻¹) * (hom g)) a : by rewrite (is_hom hom)
   ... = ((hom h⁻¹) ∘ hom g) a                    : by rewrite perm_f_mul
-  ... = perm.f ((hom h)⁻¹ * hom h) a             : by unfold compose; rewrite [this, perm_f_mul, hom_map_inv hom h]
+  ... = perm.f ((hom h)⁻¹ * hom h) a             : by unfold comp; rewrite [this, perm_f_mul, hom_map_inv hom h]
   ... = perm.f (1 : perm S) a                    : by rewrite (mul.left_inv (hom h))
   ... = a                                        : by esimp
 
@@ -486,7 +486,7 @@ definition lower_perm (p : perm (fin (succ n))) (P : p maxi = maxi) : perm (fin
 perm.mk (lower_inj p (perm.inj p) P)
   (take i j, begin
   rewrite [-eq_iff_veq, *lower_inj_apply, eq_iff_veq],
-  apply injective_compose (perm.inj p) lift_succ_inj
+  apply injective_comp (perm.inj p) lift_succ_inj
   end)
 
 lemma lift_lower_eq : ∀ {p : perm (fin (succ n))} (P : p maxi = maxi),
diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean
index 08aecb5f8..8b326798a 100644
--- a/library/theories/group_theory/cyclic.lean
+++ b/library/theories/group_theory/cyclic.lean
@@ -292,7 +292,7 @@ lemma rotl_rotr : ∀ {n : nat} (m : nat), (@rotl n m) ∘ (rotr m) = id
 | (nat.succ n) := take m, funext take i, calc (mk_mod n (n*m)) + (-(mk_mod n (n*m)) + i) = i : add_neg_cancel_left
 
 lemma rotl_succ {n : nat} : (rotl 1) ∘ (@succ n) = lift_succ :=
-funext (take i, eq_of_veq (begin rewrite [↑compose, ↑rotl, ↑madd, mul_one n, ↑mk_mod, mod_add_mod, ↑lift_succ, val_succ, -succ_add_eq_succ_add, add_mod_self_left, mod_eq_of_lt (lt.trans (is_lt i) !lt_succ_self), -val_lift] end))
+funext (take i, eq_of_veq (begin rewrite [↑comp, ↑rotl, ↑madd, mul_one n, ↑mk_mod, mod_add_mod, ↑lift_succ, val_succ, -succ_add_eq_succ_add, add_mod_self_left, mod_eq_of_lt (lt.trans (is_lt i) !lt_succ_self), -val_lift] end))
 
 definition list.rotl {A : Type} : ∀ l : list A, list A
 | []     := []
@@ -336,7 +336,7 @@ lemma rotl_seq_ne_id : ∀ {n : nat}, (∃ a b : A, a ≠ b) → ∀ i, i < n 
   assume Peq, absurd (congr_fun Peq f) P
 
 lemma rotr_rotl_fun {n : nat} (m : nat) (f : seq A n) : rotr_fun m (rotl_fun m f) = f :=
-calc f ∘ (rotl m) ∘ (rotr m) = f ∘ ((rotl m) ∘ (rotr m)) : by rewrite -compose.assoc
+calc f ∘ (rotl m) ∘ (rotr m) = f ∘ ((rotl m) ∘ (rotr m)) : by rewrite -comp.assoc
                          ... = f ∘ id                    : by rewrite (rotl_rotr m)
 
 lemma rotl_fun_inj {n : nat} {m : nat} : @injective (seq A n) (seq A n) (rotl_fun m) :=
@@ -365,7 +365,7 @@ include finA deceqA
 
 lemma rotl_perm_mul {i j : nat} : (rotl_perm A n i) * (rotl_perm A n j) = rotl_perm A n (j+i) :=
 eq_of_feq (funext take f, calc
-  f ∘ (rotl j) ∘ (rotl i) = f ∘ ((rotl j) ∘ (rotl i)) : by rewrite -compose.assoc
+  f ∘ (rotl j) ∘ (rotl i) = f ∘ ((rotl j) ∘ (rotl i)) : by rewrite -comp.assoc
                       ... = f ∘ (rotl (j+i))          : by rewrite rotl_compose)
 
 lemma rotl_perm_pow_eq : ∀ {i : nat}, (rotl_perm A n 1) ^ i = rotl_perm A n i
diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean
index e0ad7c70c..86f4d045e 100644
--- a/library/theories/group_theory/finsubg.lean
+++ b/library/theories/group_theory/finsubg.lean
@@ -137,7 +137,7 @@ begin
   esimp [fin_inv, fin_lcoset, fin_rcoset],
   rewrite [-image_comp],
   apply ext, intro b,
-  rewrite [*mem_image_iff, ↑compose, ↑lmul_by, ↑rmul_by],
+  rewrite [*mem_image_iff, ↑comp, ↑lmul_by, ↑rmul_by],
   apply iff.intro,
     intro Pl, cases Pl with h Ph, cases Ph with Pin Peq,
     existsi h⁻¹, apply and.intro,
diff --git a/library/theories/group_theory/perm.lean b/library/theories/group_theory/perm.lean
index 48449bdc5..6e2583f8f 100644
--- a/library/theories/group_theory/perm.lean
+++ b/library/theories/group_theory/perm.lean
@@ -83,7 +83,7 @@ definition perm_is_fintype [instance] : fintype (perm A) :=
            fintype.mk all_perms nodup_all_perms all_perms_complete
 
 definition perm.mul (f g : perm A) :=
-           perm.mk (f∘g) (injective_compose (perm.inj f) (perm.inj g))
+           perm.mk (f∘g) (injective_comp (perm.inj f) (perm.inj g))
 definition perm.one [reducible] : perm A := perm.mk id injective_id
 definition perm.inv (f : perm A) := let inj := perm.inj f in
            perm.mk (perm_inv inj) (perm_inv_inj inj)
diff --git a/library/theories/group_theory/pgroup.lean b/library/theories/group_theory/pgroup.lean
index 6570bac9a..9c502d568 100644
--- a/library/theories/group_theory/pgroup.lean
+++ b/library/theories/group_theory/pgroup.lean
@@ -200,7 +200,7 @@ lemma rotl_perm_peo_of_peo {n : nat} : ∀ {m} {s : seq A n}, peo s → peo (rot
 | (succ m) := take s,
   have Pmul : rotl_perm A n (m + 1) s = rotl_fun 1 (rotl_perm A n m s), from
     calc s ∘ (rotl (m + 1)) = s ∘ ((rotl m) ∘ (rotl 1)) : rotl_compose
-                        ... = s ∘ (rotl m) ∘ (rotl 1) : compose.assoc,
+                        ... = s ∘ (rotl m) ∘ (rotl 1) : comp.assoc,
   begin
   rewrite [-add_one, Pmul], intro P,
   exact rotl1_peo_of_peo (rotl_perm_peo_of_peo P)
@@ -257,7 +257,7 @@ funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, -rotl_perm_pow_eq, rot
 
 lemma rotl_peo_seq_compose {n i j : nat} :
   (rotl_peo_seq A n i) ∘ (rotl_peo_seq A n j) = rotl_peo_seq A n (j + i) :=
-funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, ↑rotl_fun, compose.assoc, rotl_compose] end
+funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, ↑rotl_fun, comp.assoc, rotl_compose] end
 
 lemma rotl_peo_seq_mod {n i : nat} : rotl_peo_seq A n i = rotl_peo_seq A n (i % succ n) :=
 funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, rotl_perm_mod] end
diff --git a/library/theories/group_theory/subgroup.lean b/library/theories/group_theory/subgroup.lean
index 7b7d986c5..c2a0be65f 100644
--- a/library/theories/group_theory/subgroup.lean
+++ b/library/theories/group_theory/subgroup.lean
@@ -22,11 +22,11 @@ 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
-        rewrite [↑function.compose, ↑lmul, mul.assoc])
+        rewrite [↑function.comp, ↑lmul, mul.assoc])
 lemma rmul_compose : ∀ (a b : A), (rmul a) ∘ (rmul b) = rmul (b*a) :=
       take a, take b,
       funext (assume x, by
-        rewrite [↑function.compose, ↑rmul, mul.assoc])
+        rewrite [↑function.comp, ↑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_comp
       ... = lmul (a*b) ' S : lmul_compose
diff --git a/tests/lean/550.lean b/tests/lean/550.lean
index e94417d69..bb286c9ba 100644
--- a/tests/lean/550.lean
+++ b/tests/lean/550.lean
@@ -12,19 +12,19 @@ attribute bijection.func [coercion]
 namespace bijection
   variable {A : Type}
 
-  definition compose (f g : bijection A) : bijection A :=
+  definition comp (f g : bijection A) : bijection A :=
   bijection.mk
     (f ∘ g)
     (finv g ∘ finv f)
-    (by rewrite [compose.assoc, -{finv f ∘ _}compose.assoc, linv f, compose.left_id, linv g])
-    (by rewrite [-compose.assoc, {_ ∘ finv g}compose.assoc, rinv g, compose.right_id, rinv f])
+    (by rewrite [comp.assoc, -{finv f ∘ _}comp.assoc, linv f, comp.left_id, linv g])
+    (by rewrite [-comp.assoc, {_ ∘ finv g}comp.assoc, rinv g, comp.right_id, rinv f])
 
-  infixr ` ∘b `:100 := compose
+  infixr ` ∘b `:100 := comp
 
   lemma compose.assoc (f g h : bijection A) : (f ∘b g) ∘b h = f ∘b (g ∘b h) := rfl
 
   definition id : bijection A :=
-  bijection.mk id id (compose.left_id id) (compose.left_id id)
+  bijection.mk id id (comp.left_id id) (comp.left_id id)
 
   lemma id.left_id (f : bijection A) : id ∘b f = f :=
   bijection.rec_on f (λx x x x, rfl)
@@ -40,5 +40,5 @@ namespace bijection
     (linv f)
 
   lemma inv.linv (f : bijection A) : inv f ∘b f = id :=
-  bijection.rec_on f (λfunc finv linv rinv, by rewrite [↑inv, ↑compose, linv])
+  bijection.rec_on f (λfunc finv linv rinv, by rewrite [↑inv, ↑comp, linv])
 end bijection
diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out
index 8331dcc31..49cfc7644 100644
--- a/tests/lean/550.lean.expected.out
+++ b/tests/lean/550.lean.expected.out
@@ -1,4 +1,4 @@
-550.lean:43:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
+550.lean:43:69: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
   eq.symm linv
 term
   linv
@@ -16,13 +16,13 @@ linv : finv ∘ func = id,
 rinv : func ∘ finv = id
 ⊢ mk (finv ∘ func) (finv ∘ func)
     (eq.rec
-       (eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (compose.left_id func))) (eq.symm rinv))
-          (function.compose.assoc func finv func))
-       (eq.symm (function.compose.assoc finv func (finv ∘ func))))
+       (eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (comp.left_id func))) (eq.symm rinv))
+          (comp.assoc func finv func))
+       (eq.symm (comp.assoc finv func (finv ∘ func))))
     (eq.rec
-       (eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (compose.right_id finv))) (eq.symm rinv))
-          (eq.symm (function.compose.assoc finv func finv)))
-       (function.compose.assoc (finv ∘ func) finv func)) = id
+       (eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (comp.right_id finv))) (eq.symm rinv))
+          (eq.symm (comp.assoc finv func finv)))
+       (comp.assoc (finv ∘ func) finv func)) = id
 550.lean:43:44: error: don't know how to synthesize placeholder
 A : Type,
 f : bijection A,
diff --git a/tests/lean/run/blast_tuple2.lean b/tests/lean/run/blast_tuple2.lean
index eca1cd669..cbcba8d9a 100644
--- a/tests/lean/run/blast_tuple2.lean
+++ b/tests/lean/run/blast_tuple2.lean
@@ -44,15 +44,15 @@ example : m = n → xs == ys → nil ++ xs == ys := by inst_simp
 example : (xs ++ ys) ++ zs == xs ++ (ys ++ zs) := by inst_simp
 example : p = m + n → zs == xs ++ ys → zs ++ ws == (xs ++ ys) ++ ws := by inst_simp
 example : m + n = p → xs ++ ys == zs → zs ++ ws == xs ++ (ys ++ ws) := by inst_simp
-        
+
 example : m = n → p = q → m + n = p → xs == ys → zs == ws → xs ++ ys == zs → ws ++ ws == (ys ++ xs) ++ (xs ++ ys) := by inst_simp
 
 example : m = n → n = p → xs == reverse ys → ys == reverse zs → xs == zs := by inst_simp
 
-example : m = n → xs == ys → f = g → a = b → map f (cons a xs) == cons (g b) (map g ys) := by 
+example : m = n → xs == ys → f = g → a = b → map f (cons a xs) == cons (g b) (map g ys) := by
 inst_simp
 
-attribute function.compose [semireducible]
+attribute function.comp [semireducible]
 example : m = n → xs == ys → h1 = h2 → k1 = k2 → map k1 (map h1 xs) == map (k2 ∘ h2) ys := by inst_simp
 
 example : ∀ (xs : tuple A (nat.succ m)) (ys : tuple A (nat.succ n))
diff --git a/tests/lean/run/new_obtain4.lean b/tests/lean/run/new_obtain4.lean
index 0af8bac43..66a6aedd1 100644
--- a/tests/lean/run/new_obtain4.lean
+++ b/tests/lean/run/new_obtain4.lean
@@ -3,7 +3,7 @@ open set function eq.ops
 
 variables {X Y Z : Type}
 
-lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
+lemma image_comp (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
 ext (take z,
   iff.intro
     (assume Hz,
@@ -11,4 +11,4 @@ ext (take z,
       by repeat (apply mem_image | assumption | reflexivity))
     (assume Hz,
       obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
-      by repeat (apply mem_image | assumption | esimp [compose] | rewrite Hz₂)))
+      by repeat (apply mem_image | assumption | esimp [comp] | rewrite Hz₂)))