From de83a68667094453a13cc13bae03ba032222b66d Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 12 Sep 2015 10:00:34 -0400
Subject: [PATCH] refactor(library/data/{int,rat}/*): clean up casts between
 nat, int, and rat

---
 library/data/int/basic.lean                   |  7 ++-
 library/data/int/div.lean                     | 10 +--
 library/data/int/gcd.lean                     | 12 ++--
 library/data/int/order.lean                   | 17 +++--
 library/data/pnat.lean                        | 10 +--
 library/data/rat/basic.lean                   | 22 +++++--
 library/data/rat/order.lean                   | 63 ++++++++++++-------
 library/data/real/basic.lean                  | 10 +--
 library/data/real/complete.lean               |  8 +--
 .../number_theory/irrational_roots.lean       |  4 +-
 10 files changed, 97 insertions(+), 66 deletions(-)

diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 1c10c3bce..437c9f6cc 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -87,7 +87,10 @@ infix  [priority int.prio] *  := int.mul
 theorem of_nat.inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n :=
 int.no_confusion H imp.id
 
-theorem of_nat_eq_of_nat (m n : ℕ) : of_nat m = of_nat n ↔ m = n :=
+theorem eq_of_of_nat_eq_of_nat {m n : ℕ} (H : of_nat m = of_nat n) : m = n :=
+of_nat.inj H
+
+theorem of_nat_eq_of_nat_iff (m n : ℕ) : of_nat m = of_nat n ↔ m = n :=
 iff.intro of_nat.inj !congr_arg
 
 theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n :=
@@ -97,7 +100,7 @@ theorem neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl
 
 private definition has_decidable_eq₂ : Π (a b : ℤ), decidable (a = b)
 | (of_nat m) (of_nat n) := decidable_of_decidable_of_iff
-    (nat.has_decidable_eq m n) (iff.symm (of_nat_eq_of_nat m n))
+    (nat.has_decidable_eq m n) (iff.symm (of_nat_eq_of_nat_iff m n))
 | (of_nat m) -[1+ n]    := inr (by contradiction)
 | -[1+ m]    (of_nat n) := inr (by contradiction)
 | -[1+ m]    -[1+ n]    := if H : m = n then
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index add7a9679..3de303d69 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -288,7 +288,7 @@ obtain m (Hm : a = of_nat m), from exists_eq_of_nat H1,
 obtain n (Hn : b = of_nat n), from exists_eq_of_nat (le_of_lt (lt_of_le_of_lt H1 H2)),
 begin
   revert H2,
-  rewrite [Hm, Hn, of_nat_mod, of_nat_lt_of_nat, of_nat_eq_of_nat],
+  rewrite [Hm, Hn, of_nat_mod, of_nat_lt_of_nat_iff, of_nat_eq_of_nat_iff],
   apply nat.mod_eq_of_lt
 end
 
@@ -481,21 +481,21 @@ nat.by_cases_zero_pos n
         assume H4 : of_nat n' = of_nat m * c,
         have H5 : c > 0, from pos_of_mul_pos_left (H4 ▸ H2) !of_nat_nonneg,
         obtain k (H6 : c = of_nat k), from exists_eq_of_nat (le_of_lt H5),
-        have H7 : n' = (#nat m * k), from (!iff.mp !of_nat_eq_of_nat (H6 ▸ H4)),
+        have H7 : n' = (#nat m * k), from (of_nat.inj (H6 ▸ H4)),
         nat.dvd.intro H7⁻¹))
 
 theorem of_nat_dvd_of_nat_of_dvd {m n : ℕ} (H : #nat m ∣ n) : of_nat m ∣ of_nat n :=
 nat.dvd.elim H
   (take k, assume H1 : #nat n = m * k,
-    dvd.intro (!iff.mpr !of_nat_eq_of_nat H1⁻¹))
+    dvd.intro (H1⁻¹ ▸ rfl))
 
-theorem of_nat_dvd_of_nat (m n : ℕ) : of_nat m ∣ of_nat n ↔ (#nat m ∣ n) :=
+theorem of_nat_dvd_of_nat_iff (m n : ℕ) : of_nat m ∣ of_nat n ↔ (#nat m ∣ n) :=
 iff.intro dvd_of_of_nat_dvd_of_nat of_nat_dvd_of_nat_of_dvd
 
 theorem dvd.antisymm {a b : ℤ} (H1 : a ≥ 0) (H2 : b ≥ 0) : a ∣ b → b ∣ a → a = b :=
 begin
   rewrite [-abs_of_nonneg H1, -abs_of_nonneg H2, -*of_nat_nat_abs],
-  rewrite [*of_nat_dvd_of_nat, *of_nat_eq_of_nat],
+  rewrite [*of_nat_dvd_of_nat_iff, *of_nat_eq_of_nat_iff],
   apply nat.dvd.antisymm
 end
 
diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean
index 502c00bb0..48715c573 100644
--- a/library/data/int/gcd.lean
+++ b/library/data/int/gcd.lean
@@ -63,7 +63,7 @@ by rewrite [↑gcd, nat.gcd_self, of_nat_nat_abs]
 
 theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a :=
 have gcd a b ∣ abs a,
-  by rewrite [↑gcd, -of_nat_nat_abs, of_nat_dvd_of_nat]; apply nat.gcd_dvd_left,
+  by rewrite [↑gcd, -of_nat_nat_abs, of_nat_dvd_of_nat_iff]; apply nat.gcd_dvd_left,
 iff.mp !dvd_abs_iff this
 
 theorem gcd_dvd_right (a b : ℤ) : gcd a b ∣ b :=
@@ -72,7 +72,7 @@ by rewrite gcd.comm; apply gcd_dvd_left
 theorem dvd_gcd {a b c : ℤ} : a ∣ b → a ∣ c → a ∣ gcd b c :=
 begin
   rewrite [↑gcd, -*(abs_dvd_iff a), -(dvd_abs_iff _ b), -(dvd_abs_iff _ c), -*of_nat_nat_abs],
-  rewrite [*of_nat_dvd_of_nat] ,
+  rewrite [*of_nat_dvd_of_nat_iff] ,
   apply nat.dvd_gcd
 end
 
@@ -212,21 +212,21 @@ theorem lcm_self (a : ℤ) : lcm a a = abs a :=
 by krewrite [↑lcm, nat.lcm_self, of_nat_nat_abs]
 
 theorem dvd_lcm_left (a b : ℤ) : a ∣ lcm a b :=
-by rewrite [↑lcm, -abs_dvd_iff, -of_nat_nat_abs, of_nat_dvd_of_nat]; apply nat.dvd_lcm_left
+by rewrite [↑lcm, -abs_dvd_iff, -of_nat_nat_abs, of_nat_dvd_of_nat_iff]; apply nat.dvd_lcm_left
 
 theorem dvd_lcm_right (a b : ℤ) : b ∣ lcm a b :=
 !lcm.comm ▸ !dvd_lcm_left
 
 theorem gcd_mul_lcm (a b : ℤ) : gcd a b * lcm a b = abs (a * b) :=
 begin
-  rewrite [↑gcd, ↑lcm, -of_nat_nat_abs, -of_nat_mul, of_nat_eq_of_nat, nat_abs_mul],
+  rewrite [↑gcd, ↑lcm, -of_nat_nat_abs, -of_nat_mul, of_nat_eq_of_nat_iff, nat_abs_mul],
   apply nat.gcd_mul_lcm
 end
 
 theorem lcm_dvd {a b c : ℤ} : a ∣ c → b ∣ c → lcm a b ∣ c :=
 begin
   rewrite [↑lcm, -(abs_dvd_iff a), -(abs_dvd_iff b), -*(dvd_abs_iff _ c), -*of_nat_nat_abs],
-  rewrite [*of_nat_dvd_of_nat] ,
+  rewrite [*of_nat_dvd_of_nat_iff] ,
   apply nat.lcm_dvd
 end
 
@@ -261,7 +261,7 @@ dvd_of_coprime_of_dvd_mul_right H1 (!mul.comm ▸ H2)
 theorem gcd_mul_left_cancel_of_coprime {c : ℤ} (a : ℤ) {b : ℤ} (H : coprime c b) :
    gcd (c * a) b = gcd a b :=
 begin
-  revert H, rewrite [↑coprime, ↑gcd, *of_nat_eq_of_nat, nat_abs_mul],
+  revert H, rewrite [↑coprime, ↑gcd, *of_nat_eq_of_nat_iff, nat_abs_mul],
   apply nat.gcd_mul_left_cancel_of_coprime
 end
 
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 3ed514fcc..2b4f35201 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -45,7 +45,7 @@ theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
 or.imp_right
   (assume H : nonneg (-(b - a)),
    have -(b - a) = a - b, from !neg_sub,
-   show nonneg (a - b), from this ▸ H)   -- too bad: can't do it in one step
+   show nonneg (a - b), from this ▸ H)
   (nonneg_or_nonneg_neg (b - a))
 
 theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : #nat m ≤ n) : of_nat m ≤ of_nat n :=
@@ -57,7 +57,7 @@ obtain (k : ℕ) (Hk : of_nat m + of_nat k = of_nat n), from le.elim H,
 have m + k = n, from of_nat.inj (of_nat_add m k ⬝ Hk),
 nat.le.intro this
 
-theorem of_nat_le_of_nat (m n : ℕ) : of_nat m ≤ of_nat n ↔ m ≤ n :=
+theorem of_nat_le_of_nat_iff (m n : ℕ) : of_nat m ≤ of_nat n ↔ m ≤ n :=
 iff.intro le_of_of_nat_le_of_nat of_nat_le_of_nat_of_le
 
 theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
@@ -78,18 +78,18 @@ have a + succ n = b, from
            ... = b         : Hn,
 exists.intro n this
 
-theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m :=
+theorem of_nat_lt_of_nat_iff (n m : ℕ) : of_nat n < of_nat m ↔ n < m :=
 calc
   of_nat n < of_nat m ↔ of_nat n + 1 ≤ of_nat m : iff.refl
     ... ↔ of_nat (nat.succ n) ≤ of_nat m        : of_nat_succ n ▸ !iff.refl
-    ... ↔ nat.succ n ≤ m                        : of_nat_le_of_nat
+    ... ↔ nat.succ n ≤ m                        : of_nat_le_of_nat_iff
     ... ↔ n < m                                 : iff.symm (lt_iff_succ_le _ _)
 
 theorem lt_of_of_nat_lt_of_nat {m n : ℕ} (H : of_nat m < of_nat n) : #nat m < n :=
-iff.mp !of_nat_lt_of_nat H
+iff.mp !of_nat_lt_of_nat_iff H
 
 theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : #nat m < n) : of_nat m < of_nat n :=
-iff.mpr !of_nat_lt_of_nat H
+iff.mpr !of_nat_lt_of_nat_iff H
 
 /- show that the integers form an ordered additive group -/
 
@@ -388,7 +388,6 @@ dvd.elim H'
   (take b,
     suppose 1 = a * b,
     eq_one_of_mul_eq_one_right H this⁻¹)
---
 
 theorem ex_smallest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≤ b → ¬ P z)
         (Hinh : ∃ z : ℤ, P z) : ∃ lb : ℤ, P lb ∧ (∀ z : ℤ, z < lb → ¬ P z) :=
@@ -418,7 +417,7 @@ theorem ex_smallest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : 
     have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin
      let Hz' := iff.mp !int.lt_add_iff_sub_lt_left Hz,
      rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
-     apply iff.mp !int.of_nat_lt_of_nat Hz'
+     apply lt_of_of_nat_lt_of_nat Hz'
     end,
     let Hk' := nat.not_le_of_gt Hk,
     rewrite Hzbk,
@@ -455,7 +454,7 @@ theorem ex_largest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : ∃
     have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin
       let Hz' := iff.mp !int.lt_add_iff_sub_lt_left (iff.mpr !int.lt_add_iff_sub_lt_right Hz),
       rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
-      apply iff.mp !int.of_nat_lt_of_nat Hz'
+      apply lt_of_of_nat_lt_of_nat Hz'
     end,
     let Hk' := nat.not_le_of_gt Hk,
     rewrite Hzbk,
diff --git a/library/data/pnat.lean b/library/data/pnat.lean
index 4910d59e8..c1a277f8b 100644
--- a/library/data/pnat.lean
+++ b/library/data/pnat.lean
@@ -88,16 +88,16 @@ theorem pnat.to_rat_of_nat (n : ℕ+) : rat_of_pnat n = of_nat n~ := rfl
 theorem rat_of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial
 
 theorem rat_of_pnat_ge_one (n : ℕ+) : rat_of_pnat n ≥ 1 :=
-  (iff.mpr !of_nat_le_of_nat) (pnat_pos n)
+  of_nat_le_of_nat_of_le (pnat_pos n)
 
 theorem rat_of_pnat_is_pos (n : ℕ+) : rat_of_pnat n > 0 :=
-  (iff.mpr !of_nat_pos) (pnat_pos n)
+  of_nat_lt_of_nat_of_lt (pnat_pos n)
 
 theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : m ≤ n) : of_nat m ≤ of_nat n :=
-  (iff.mpr !of_nat_le_of_nat) H
+  of_nat_le_of_nat_of_le H
 
 theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : m < n) : of_nat m < of_nat n :=
-  (iff.mpr !of_nat_lt_of_nat) H
+  of_nat_lt_of_nat_of_lt H
 
 theorem rat_of_pnat_le_of_pnat_le {m n : ℕ+} (H : m ≤ n) : rat_of_pnat m ≤ rat_of_pnat n :=
   of_nat_le_of_nat_of_le H
@@ -106,7 +106,7 @@ theorem rat_of_pnat_lt_of_pnat_lt {m n : ℕ+} (H : m < n) : rat_of_pnat m < rat
   of_nat_lt_of_nat_of_lt H
 
 theorem pnat_le_of_rat_of_pnat_le {m n : ℕ+} (H : rat_of_pnat m ≤ rat_of_pnat n) : m ≤ n :=
-  (iff.mp !of_nat_le_of_nat) H
+  le_of_of_nat_le_of_nat H
 
 definition inv (n : ℕ+) : ℚ := (1 : ℚ) / rat_of_pnat n
 postfix `⁻¹` := inv
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 2f7f5b6eb..c3754d372 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -349,8 +349,8 @@ namespace rat
 /- operations -/
 
 definition of_int [coercion] (i : ℤ) : ℚ := ⟦prerat.of_int i⟧
-definition of_nat [coercion] (n : ℕ) : ℚ := ⟦prerat.of_int n⟧
-definition of_num [coercion] [reducible] (n : num) : ℚ := of_int (int.of_num n)
+definition of_nat [coercion] (n : ℕ) : ℚ := nat.to.rat n
+definition of_num [coercion] [reducible] (n : num) : ℚ := num.to.rat n
 
 definition add : ℚ → ℚ → ℚ :=
 quot.lift₂
@@ -413,16 +413,28 @@ calc
 theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b :=
 prerat.of_int.inj (quot.exact H)
 
+theorem eq_of_of_int_eq_of_int {a b : ℤ} (H : of_int a = of_int b) : a = b :=
+of_int.inj H
+
 theorem of_nat_eq (a : ℕ) : of_nat a = of_int (int.of_nat a) := rfl
 
 theorem of_nat_add (a b : ℕ) : of_nat (#nat a + b) = of_nat a + of_nat b :=
-by rewrite [*of_nat_eq, int.of_nat_add, rat.of_int_add]
+by rewrite [of_nat_eq, int.of_nat_add, rat.of_int_add]
 
 theorem of_nat_mul (a b : ℕ) : of_nat (#nat a * b) = of_nat a * of_nat b :=
-by rewrite [*of_nat_eq, int.of_nat_mul, rat.of_int_mul]
+by rewrite [of_nat_eq, int.of_nat_mul, rat.of_int_mul]
 
 theorem of_nat_sub {a b : ℕ} (H : #nat a ≥ b) : of_nat (#nat a - b) = of_nat a - of_nat b :=
-by rewrite [*of_nat_eq, int.of_nat_sub H, rat.of_int_sub]
+by rewrite [of_nat_eq, int.of_nat_sub H, rat.of_int_sub]
+
+theorem of_nat.inj {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
+int.of_nat.inj (of_int.inj H)
+
+theorem eq_of_of_nat_eq_of_nat {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
+of_nat.inj H
+
+theorem of_nat_eq_of_nat_iff (a b : ℕ) : of_nat a = of_nat b ↔ a = b :=
+iff.intro of_nat.inj !congr_arg
 
 theorem add.comm (a b : ℚ) : a + b = b + a :=
 quot.induction_on₂ a b (take u v, quot.sound !prerat.add.comm)
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 5dedf223a..14605aa4f 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -152,35 +152,52 @@ infix [priority rat.prio] >= := rat.ge
 infix [priority rat.prio] ≥  := rat.ge
 infix [priority rat.prio] >  := rat.gt
 
-theorem of_int_lt_of_int (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) :=
+theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) :=
 iff.symm (calc
   (#int a < b) ↔ (#int b - a > 0)          : iff.symm !int.sub_pos_iff_lt
            ... ↔ pos (of_int (#int b - a)) : iff.symm !pos_of_int
            ... ↔ pos (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
            ... ↔ of_int a < of_int b       : iff.rfl)
 
-theorem of_int_le_of_int (a b : ℤ) : of_int a ≤ of_int b ↔ (#int a ≤ b) :=
+theorem of_int_lt_of_int_of_lt {a b : ℤ} (H : (#int a < b)) : of_int a < of_int b :=
+iff.mpr !of_int_lt_of_int_iff H
+
+theorem lt_of_of_int_lt_of_int {a b : ℤ} (H : of_int a < of_int b) : (#int a < b) :=
+iff.mp !of_int_lt_of_int_iff H
+
+theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (#int a ≤ b) :=
 iff.symm (calc
   (#int a ≤ b) ↔ (#int b - a ≥ 0)             : iff.symm !int.sub_nonneg_iff_le
            ... ↔ nonneg (of_int (#int b - a)) : iff.symm !nonneg_of_int
            ... ↔ nonneg (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
            ... ↔ of_int a ≤ of_int b          : iff.rfl)
 
-theorem of_int_pos (a : ℤ) : (of_int a > 0) ↔ (#int a > 0) := !of_int_lt_of_int
+theorem of_int_le_of_int_of_le {a b : ℤ} (H : (#int a ≤ b)) : of_int a ≤ of_int b :=
+iff.mpr !of_int_le_of_int_iff H
 
-theorem of_int_nonneg (a : ℤ) : (of_int a ≥ 0) ↔ (#int a ≥ 0) := !of_int_le_of_int
+theorem le_of_of_int_le_of_int {a b : ℤ} (H : of_int a ≤ of_int b) : (#int a ≤ b) :=
+iff.mp !of_int_le_of_int_iff H
 
-theorem of_nat_lt_of_nat (a b : ℕ) : of_nat a < of_nat b ↔ (#nat a < b) :=
-by rewrite [*of_nat_eq, propext !of_int_lt_of_int]; apply int.of_nat_lt_of_nat
+theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ (#nat a < b) :=
+by rewrite [*of_nat_eq, of_int_lt_of_int_iff, int.of_nat_lt_of_nat_iff]
 
-theorem of_nat_le_of_nat (a b : ℕ) : of_nat a ≤ of_nat b ↔ (#nat a ≤ b) :=
-by rewrite [*of_nat_eq, propext !of_int_le_of_int]; apply int.of_nat_le_of_nat
+theorem of_nat_lt_of_nat_of_lt {a b : ℕ} (H : (#nat a < b)) : of_nat a < of_nat b :=
+iff.mpr !of_nat_lt_of_nat_iff H
 
-theorem of_nat_pos (a : ℕ) : (of_nat a > 0) ↔ (#nat a > nat.zero) :=
-!of_nat_lt_of_nat
+theorem lt_of_of_nat_lt_of_nat {a b : ℕ} (H : of_nat a < of_nat b) : (#nat a < b) :=
+iff.mp !of_nat_lt_of_nat_iff H
+
+theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ (#nat a ≤ b) :=
+by rewrite [*of_nat_eq, of_int_le_of_int_iff, int.of_nat_le_of_nat_iff]
+
+theorem of_nat_le_of_nat_of_le {a b : ℕ} (H : (#nat a ≤ b)) : of_nat a ≤ of_nat b :=
+iff.mpr !of_nat_le_of_nat_iff H
+
+theorem le_of_of_nat_le_of_nat {a b : ℕ} (H : of_nat a ≤ of_nat b) : (#nat a ≤ b) :=
+iff.mp !of_nat_le_of_nat_iff H
 
 theorem of_nat_nonneg (a : ℕ) : (of_nat a ≥ 0) :=
-iff.mpr !of_nat_le_of_nat !nat.zero_le
+of_nat_le_of_nat_of_le !nat.zero_le
 
 theorem le.refl (a : ℚ) : a ≤ a :=
 by rewrite [↑rat.le, sub_self]; apply nonneg_zero
@@ -328,8 +345,8 @@ end migrate_algebra
 theorem rat_of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
 assert ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
 int.induction_on a
-  (take b, abs_of_nonneg (!of_nat_nonneg))
-  (take b, by rewrite [this, abs_neg, abs_of_nonneg (!of_nat_nonneg)])
+  (take b, abs_of_nonneg !of_nat_nonneg)
+  (take b, by rewrite [this, abs_neg, abs_of_nonneg !of_nat_nonneg])
 
 section
   open int
@@ -341,40 +358,40 @@ section
     begin
       rewrite [-mul_denom],
       apply mul_nonneg H,
-      rewrite [of_int_le_of_int],
+      rewrite [of_int_le_of_int_iff],
       exact int.le_of_lt !denom_pos
     end,
-  show num q ≥ 0, from iff.mp !of_int_le_of_int this
+  show num q ≥ 0, from le_of_of_int_le_of_int this
 
   theorem num_pos_of_pos {q : ℚ} (H : q > 0) : num q > 0 :=
   have of_int (num q) > of_int 0,
     begin
       rewrite [-mul_denom],
       apply mul_pos H,
-      rewrite [of_int_lt_of_int],
+      rewrite [of_int_lt_of_int_iff],
       exact !denom_pos
     end,
-  show num q > 0, from iff.mp !of_int_lt_of_int this
+  show num q > 0, from lt_of_of_int_lt_of_int this
 
   theorem num_neg_of_neg {q : ℚ} (H : q < 0) : num q < 0 :=
   have of_int (num q) < of_int 0,
     begin
       rewrite [-mul_denom],
       apply mul_neg_of_neg_of_pos H,
-      rewrite [of_int_lt_of_int],
+      rewrite [of_int_lt_of_int_iff],
       exact !denom_pos
     end,
-  show num q < 0, from iff.mp !of_int_lt_of_int this
+  show num q < 0, from lt_of_of_int_lt_of_int this
 
   theorem num_nonpos_of_nonpos {q : ℚ} (H : q ≤ 0) : num q ≤ 0 :=
   have of_int (num q) ≤ of_int 0,
     begin
       rewrite [-mul_denom],
       apply mul_nonpos_of_nonpos_of_nonneg H,
-      rewrite [of_int_le_of_int],
+      rewrite [of_int_le_of_int_iff],
       exact int.le_of_lt !denom_pos
     end,
-  show num q ≤ 0, from iff.mp !of_int_le_of_int this
+  show num q ≤ 0, from le_of_of_int_le_of_int this
 end
 
 definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a))
@@ -382,10 +399,10 @@ definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a))
 theorem ubound_ge (a : ℚ) : of_nat (ubound a) ≥ a :=
 have h : abs a * abs (of_int (denom a)) = abs (of_int (num a)), from
   !abs_mul ▸ !mul_denom ▸ rfl,
-assert of_int (denom a) > 0, from (iff.mpr !of_int_pos) !denom_pos,
+assert of_int (denom a) > 0, from of_int_lt_of_int_of_lt !denom_pos,
 have 1 ≤ abs (of_int (denom a)), begin
     rewrite (abs_of_pos this),
-    apply iff.mpr !of_int_le_of_int,
+    apply of_int_le_of_int_of_le,
     apply denom_pos
   end,
 have abs a ≤ abs (of_int (num a)), from
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 9bb6fb547..67e023000 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -1061,11 +1061,11 @@ theorem one_mul (x : ℝ) : 1 * x = x :=
 theorem mul_one (x : ℝ) : x * 1 = x :=
   quot.induction_on x (λ s, quot.sound (r_mul_one s))
 
-theorem distrib (x y z : ℝ) : x * (y + z) = x * y + x * z :=
+theorem left_distrib (x y z : ℝ) : x * (y + z) = x * y + x * z :=
   quot.induction_on₃ x y z (λ s t u, quot.sound (r_distrib s t u))
 
-theorem distrib_l (x y z : ℝ) : (x + y) * z = x * z + y * z :=
-  by rewrite [mul_comm, distrib, {x * _}mul_comm, {y * _}mul_comm] -- this shouldn't be necessary
+theorem right_distrib (x y z : ℝ) : (x + y) * z = x * z + y * z :=
+  by rewrite [mul_comm, left_distrib, {x * _}mul_comm, {y * _}mul_comm] -- this shouldn't be necessary
 
 theorem zero_ne_one : ¬ (0 : ℝ) = 1 :=
   take H : 0 = 1,
@@ -1087,8 +1087,8 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
     apply of_num 1,
     apply one_mul,
     apply mul_one,
-    apply distrib,
-    apply distrib_l,
+    apply left_distrib,
+    apply right_distrib,
     apply mul_comm
   end
 
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index 768370134..6b93a5db1 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -399,7 +399,7 @@ theorem archimedean_upper_strict (x : ℝ) : ∃ z : ℤ, x < of_rat (of_int z)
     apply lt_of_le_of_lt,
     apply Hz,
     apply of_rat_lt_of_rat_of_lt,
-    apply iff.mpr !of_int_lt_of_int,
+    apply of_int_lt_of_int_of_lt,
     apply int.lt_add_of_pos_right,
     apply dec_trivial
   end
@@ -431,7 +431,7 @@ definition ex_floor (x : ℝ) :=
       apply Har,
       have H : of_rat (of_int (some (archimedean_upper_strict x))) ≤ of_rat (of_int z), begin
         apply of_rat_le_of_rat_of_le,
-        apply iff.mpr !of_int_le_of_int,
+        apply of_int_le_of_int_of_le,
         apply Hz
       end,
       exact H
@@ -553,7 +553,7 @@ noncomputable definition under : ℚ := of_int (floor (elt - 1))
 theorem under_spec1 : of_rat under < elt :=
   have H : of_rat under < of_rat (of_int (floor elt)), begin
     apply of_rat_lt_of_rat_of_lt,
-    apply iff.mpr !of_int_lt_of_int,
+    apply of_int_lt_of_int_of_lt,
     apply floor_succ_lt
   end,
   lt_of_lt_of_le H !floor_spec
@@ -574,7 +574,7 @@ noncomputable definition over : ℚ := of_int (ceil (bound + 1)) -- b
 theorem over_spec1 : bound < of_rat over :=
   have H : of_rat (of_int (ceil bound)) < of_rat over, begin
     apply of_rat_lt_of_rat_of_lt,
-    apply iff.mpr !of_int_lt_of_int,
+    apply of_int_lt_of_int_of_lt,
     apply ceil_succ
   end,
   lt_of_le_of_lt !ceil_spec H
diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean
index 919e593e1..4368cf19a 100644
--- a/library/theories/number_theory/irrational_roots.lean
+++ b/library/theories/number_theory/irrational_roots.lean
@@ -24,7 +24,7 @@ section
   have even b, from even_of_even_pow this,
   have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
   have 2 ∣ 1, from co ▸ this,
-  absurd `2 ∣ 1` dec_trivial
+  show false, from absurd `2 ∣ 1` dec_trivial
 end
 
 /-
@@ -81,7 +81,7 @@ section
     using this, by rewrite [-int.abs_pow, this, int.abs_mul, int.abs_pow],
   have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n,
     using this,
-      by apply of_nat.inj; rewrite [int.of_nat_mul, +of_nat_pow, +of_nat_nat_abs]; assumption,
+      by apply int.of_nat.inj; rewrite [int.of_nat_mul, +of_nat_pow, +of_nat_nat_abs]; assumption,
   have H₂ : nat.coprime (nat_abs a) (nat_abs b), from of_nat.inj !coprime_num_denom,
   have nat_abs b = 1, from
     by_cases