From bd41b6ea13a845f61a5976de86718d7a1b32fb7b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2015 15:10:50 -0700
Subject: [PATCH] refactor(library/data/rat/basic): cleanup proof

---
 library/data/rat/basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 4c8239506..8416abe7e 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -242,7 +242,8 @@ have H : smul (denom a) (mul a (add b c)) (denom_pos a) =
   have T : ∀ {x y z w : ℤ}, x*y*z*w=y*z*x*w, from
     λx y z w, (!int.mul.assoc ⬝ !int.mul.comm) ▸ rfl,
   exact !congr_arg2 T T,
-  exact !mul.left_comm ▸ !int.mul.assoc⁻¹
+  rewrite [mul.left_comm (denom a) (denom b) (denom c)],
+  rewrite int.mul.assoc
 end,
 equiv.symm (H ▸ smul_equiv (denom_pos a))