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