From a9001166fd4a5c1a8b290c7506cc25daefb01152 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Fri, 28 Nov 2014 10:43:43 -0500
Subject: [PATCH] fix(library/algebra/category/morphism): remove sorry that was
 introduced by accident

---
 library/algebra/category/morphism.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index 5ffe46e13..85c14bc3f 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -54,7 +54,7 @@ namespace morphism
   calc
     g = g ∘ id : symm !id_right
      ... = g ∘ f ∘ g' : {symm Hr}
-     ... = (g ∘ f) ∘ g' : sorry -- !assoc
+     ... = (g ∘ f) ∘ g' : !assoc
      ... = id ∘ g' : {Hl}
      ... = g' : !id_left