diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index b7639f4cc..aa8f806dc 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -97,23 +97,14 @@ namespace morphism
   theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
       : is_section (g ∘ f) :=
   is_section.mk
-    (calc
-      (retraction_of f ∘ retraction_of g) ∘ g ∘ f
-            = retraction_of f ∘ retraction_of g ∘ g ∘ f   : by rewrite -assoc
-        ... = retraction_of f ∘ (retraction_of g ∘ g) ∘ f : by rewrite (assoc _ g f)
-        ... = retraction_of f ∘ id ∘ f                    : by rewrite retraction_compose
-        ... = retraction_of f ∘ f                         : by rewrite id_left
-        ... = id                                          : by rewrite retraction_compose)
+    (show (retraction_of f ∘ retraction_of g) ∘ g ∘ f = id,
+     by rewrite [-assoc, assoc _ g f, retraction_compose, id_left, retraction_compose])
 
   theorem composition_is_retraction [instance] [Hf : is_retraction f] [Hg : is_retraction g]
       : is_retraction (g ∘ f) :=
   is_retraction.mk
-    (calc
-      (g ∘ f) ∘ section_of f ∘ section_of g = g ∘ f ∘ section_of f ∘ section_of g : symm !assoc
-        ... = g ∘ (f ∘ section_of f) ∘ section_of g : by rewrite -assoc
-        ... = g ∘ id ∘ section_of g                 : by rewrite compose_section
-        ... = g ∘ section_of g                      : by rewrite id_left
-        ... = id                                    : by rewrite compose_section)
+    (show (g ∘ f) ∘ section_of f ∘ section_of g = id,
+     by rewrite [-assoc, {f ∘ _}assoc, compose_section, id_left, compose_section])
 
   theorem composition_is_inverse [instance] [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) :=
   !section_retraction_imp_iso
@@ -140,20 +131,23 @@ namespace morphism
   inductive is_epi  [class] (f : a ⟶ b) : Prop :=
   mk : (∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) → is_epi f
 
-  theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h
-  := is_mono.rec (λH3, H3 c g h H2) H
-  theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h
-  := is_epi.rec  (λH3, H3 c g h H2) H
+  theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h :=
+  match H with
+    is_mono.mk H3 := H3 c g h H2
+  end
+
+  theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h :=
+  match H with
+    is_epi.mk H3 := H3 c g h H2
+  end
 
   theorem section_is_mono [instance] (f : a ⟶ b) [H : is_section f] : is_mono f :=
   is_mono.mk
     (λ c g h H,
       calc
-        g = id ∘ g                    : symm (id_left g)
+        g = id ∘ g                    : by rewrite id_left
       ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_compose
-      ... = retraction_of f ∘ f ∘ g   : by rewrite assoc
-      ... = retraction_of f ∘ f ∘ h   : by rewrite H
-      ... = (retraction_of f ∘ f) ∘ h : by rewrite -assoc
+      ... = (retraction_of f ∘ f) ∘ h : by rewrite [-assoc, H, -assoc]
       ... = id ∘ h                    : by rewrite retraction_compose
       ... = h                         : by rewrite id_left)
 
@@ -161,11 +155,9 @@ namespace morphism
   is_epi.mk
     (λ c g h H,
       calc
-        g = g ∘ id                 : symm (id_right g)
-      ... = g ∘ f ∘ section_of f   : by rewrite -(compose_section f)
-      ... = (g ∘ f) ∘ section_of f : by rewrite assoc
-      ... = (h ∘ f) ∘ section_of f : by rewrite H
-      ... = h ∘ f ∘ section_of f   : by rewrite -assoc
+        g = g ∘ id                 : by rewrite id_right
+      ... = g ∘ f ∘ section_of f   : by rewrite -compose_section
+      ... = h ∘ f ∘ section_of f   : by rewrite [assoc, H, -assoc]
       ... = h ∘ id                 : by rewrite compose_section
       ... = h                      : by rewrite id_right)
 
@@ -177,13 +169,19 @@ namespace morphism
   theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) :=
   is_mono.mk
     (λ d h₁ h₂ H,
-    have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂), from symm (assoc g f h₁)  ▸ symm (assoc g f h₂) ▸ H,
+    have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂),
+    begin
+      rewrite *assoc, exact H
+    end,
     mono_elim (mono_elim H2))
 
   theorem composition_is_epi  [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi  (g ∘ f) :=
   is_epi.mk
     (λ d h₁ h₂ H,
-    have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f, from assoc h₁ g f  ▸ assoc h₂ g f ▸ H,
+    have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f,
+    begin
+      rewrite -*assoc, exact H
+    end,
     epi_elim (epi_elim H2))
 end morphism
 namespace morphism