From 3cd81051c64b356c33c2a8fe63eef065d29cc4b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Jun 2015 13:52:52 -0700 Subject: [PATCH] refactor(library/data/real/division): remove unnecessary 'xrewrite' --- library/data/real/division.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 8e2fef0c0f..e12cba488b 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -228,7 +228,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ apply rat.le.trans, apply rat.mul_le_mul, apply Hs, - xrewrite [-(mul_one 1), -(div_mul_div Hsp Hspn), abs_mul], + rewrite [-(mul_one 1), -(div_mul_div Hsp Hspn), abs_mul], apply rat.mul_le_mul, rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt), apply le_ps Hs Hsep, @@ -252,7 +252,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ apply rat.le.trans, apply rat.mul_le_mul, apply Hs, - xrewrite [-(mul_one 1), -(div_mul_div Hspm Hsp), abs_mul], + rewrite [-(mul_one 1), -(div_mul_div Hspm Hsp), abs_mul], apply rat.mul_le_mul, rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)), apply le_ps Hs Hsep, @@ -274,7 +274,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ apply rat.le.trans, apply rat.mul_le_mul, apply Hs, - xrewrite [-(mul_one 1), -(div_mul_div Hspm Hspn), abs_mul], + rewrite [-(mul_one 1), -(div_mul_div Hspm Hspn), abs_mul], apply rat.mul_le_mul, rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)), apply le_ps Hs Hsep, @@ -315,7 +315,7 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H existsi max (ps Hs Hsep) j, intro n Hn, have Hnz : s_inv Hs ((K₂ s (s_inv Hs)) * 2 * n) ≠ 0, from s_inv_ne_zero Hs Hsep _, - xrewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz), + rewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz), -rat.mul_sub_left_distrib, abs_mul], apply rat.le.trans, apply rat.mul_le_mul_of_nonneg_right, @@ -334,13 +334,13 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H s_ne_zero_of_ge_p Hs Hsep (show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n), by rewrite *pnat.mul.assoc; apply pnat.mul_le_mul_right), - xrewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')], + rewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')], apply rat.le.trans, apply rat.mul_le_mul_of_nonneg_left, apply Hs, apply le_of_lt, apply rat_of_pnat_is_pos, - xrewrite [rat.mul.left_distrib, mul.comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat.mul.assoc, + rewrite [rat.mul.left_distrib, mul.comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat.mul.assoc, *(@inv_mul_eq_mul_inv (K₂ s (s_inv Hs))), -*rat.mul.assoc, *inv_cancel_left, *one_mul, -(add_halves j)], apply rat.add_le_add,