From e7f641ffc4a423149fdd07d815f1655751107390 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Mar 2016 17:37:24 -0800
Subject: [PATCH] chore(library): cleanup proofs

---
 library/algebra/ordered_ring.lean |  7 ++++++-
 library/algebra/ring.lean         | 13 ++++++++-----
 library/data/nat/div.lean         |  2 +-
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index c061418621..87f89ac42f 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -394,7 +394,12 @@ section
     (assume H : a ≥ 0, mul_nonneg H H)
     (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
 
-  theorem zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg 1
+  theorem zero_le_one : 0 ≤ (1:A) :=
+  have H : 1 * 1 ≥ 0, from mul_self_nonneg (1:A),
+  begin
+    rewrite one_mul at H,
+    assumption
+  end
 
   theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) :
     (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 8b254bed85..d5215f7dcc 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -132,7 +132,7 @@ section comm_semiring
         (show a * (d * c) = b * c, by simp))
 
   theorem dvd_mul_of_dvd_right {a b : A} (H : a ∣ b) (c : A) : a ∣ c * b :=
-  !mul.comm ▸ (dvd_mul_of_dvd_left H _)
+  begin rewrite mul.comm, exact dvd_mul_of_dvd_left H _ end
 
   theorem mul_dvd_mul {a b c d : A} (dvd_ab : a ∣ b) (dvd_cd : c ∣ d) : a * c ∣ b * d :=
   dvd.elim dvd_ab
@@ -147,7 +147,7 @@ section comm_semiring
   dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))
 
   theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b ∣ c) : b ∣ c :=
-  dvd_of_mul_right_dvd (mul.comm a b ▸ H)
+  dvd_of_mul_right_dvd begin rewrite mul.comm at H, apply H end
 
   theorem dvd_add {a b c : A} (Hab : a ∣ b) (Hac : a ∣ c) : a ∣ b + c :=
   dvd.elim Hab
@@ -361,13 +361,16 @@ section
 
   theorem eq_zero_of_mul_eq_self_right {a b : A} (H₁ : b ≠ 1) (H₂ : a * b = a) : a = 0 :=
   have b - 1 ≠ 0, from
-    suppose b - 1 = 0, H₁ (!zero_add ▸ eq_add_of_sub_eq this),
+    suppose b - 1 = 0,
+    have b = 0 + 1, from eq_add_of_sub_eq this,
+    have b = 1, by rewrite zero_add at this; exact this,
+    H₁ this,
   have a * b - a = 0,   by simp,
   have a * (b - 1) = 0, by rewrite [mul_sub_left_distrib, mul_one]; apply this,
     show a = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero this) `b - 1 ≠ 0`
 
   theorem eq_zero_of_mul_eq_self_left {a b : A} (H₁ : b ≠ 1) (H₂ : b * a = a) : a = 0 :=
-    eq_zero_of_mul_eq_self_right H₁ (!mul.comm ▸ H₂)
+    eq_zero_of_mul_eq_self_right H₁ (begin rewrite mul.comm at H₂, exact H₂ end)
 
   theorem mul_self_eq_mul_self_iff (a b : A) : a * a = b * b ↔ a = b ∨ a = -b :=
   iff.intro
@@ -392,7 +395,7 @@ section
   dvd.elim Hdvd
     (take d,
       suppose a * c = a * b * d,
-      have b * d = c, from eq_of_mul_eq_mul_left Ha (mul.assoc a b d ▸ this⁻¹),
+      have b * d = c, from eq_of_mul_eq_mul_left Ha begin rewrite -mul.assoc, symmetry, exact this end,
       dvd.intro this)
 
   theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a ∣ c * a)) : (b ∣ c) :=
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index f905d29572..cfd073b550 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -46,7 +46,7 @@ calc
             ... = succ (x / z)        : by rewrite nat.add_sub_cancel
 
 theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) / x = succ (z / x) :=
-!add.comm ▸ !add_div_self H
+add.comm z x ▸ !add_div_self H
 
 local attribute succ_mul [simp]