From 1b80dc0df612b61a035b7b2df7438bed9a0f16d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Dec 2015 10:57:16 -0800
Subject: [PATCH] feat(library/data/real/basic): improve performance

---
 library/data/real/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 039a79de77..2d6464b591 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -947,7 +947,7 @@ section
   eq_of_forall_abs_sub_le
     (take ε,
       suppose ε > 0,
-      have ε / 2 > 0, from div_pos_of_pos_of_pos this two_pos,
+      have ε / 2 > 0, begin exact div_pos_of_pos_of_pos this two_pos end,
       obtain n (Hn : n⁻¹ ≤ ε / 2), from pnat_bound this,
       show abs (a - b) ≤ ε, from calc
         abs (a - b) ≤ n⁻¹ + n⁻¹     : H₁ n