From 607e5343b1c242f3079d8f35c7d230cbf82514b5 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 7 Jun 2017 09:39:33 -0600
Subject: [PATCH] Remove useless esimp to speed up Lean.

---
 algebra/direct_sum.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index acc32c3..8596dc3 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -114,7 +114,7 @@ namespace group
     dirsum_functor (λi, homomorphism_mul (f i) (f' i)) :=
   begin
     apply dirsum_homotopy,
-    intro i y, esimp, exact sorry
+    intro i y, exact sorry
   end
 
   definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :