diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index d72b9d993..ab20557b0 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -16,15 +16,12 @@ are independent of each other.
 -/
 
 import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat
-open -[coercions] rat
+open rat algebra -- nat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
-open -[coercions] nat
+local postfix ⁻¹ := pnat.inv
 open eq.ops pnat classical
 
-local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
-local notation 3 := subtype.tag (nat.of_num 3) dec_trivial
-
 namespace rat_seq
 
 theorem rat_approx {s : seq} (H : regular s) :
@@ -37,7 +34,7 @@ theorem rat_approx {s : seq} (H : regular s) :
     apply rat.le.trans,
     apply H,
     rewrite -(add_halves n),
-    apply rat.add_le_add_right,
+    apply algebra.add_le_add_right,
     apply inv_ge_of_le Hm
   end
 
@@ -58,13 +55,14 @@ theorem rat_approx_seq {s : seq} (H : regular s) :
     rewrite ↑[sadd, sneg, s_abs, const],
     apply rat.le.trans,
     rotate 1,
-    apply rat.sub_le_sub_left,
+    rewrite -sub_eq_add_neg,
+    apply algebra.sub_le_sub_left,
     apply HN,
     apply pnat.le.trans,
     apply Hp,
     rewrite -*pnat.mul.assoc,
     apply pnat.mul_le_mul_left,
-    rewrite [sub_self, -neg_zero],
+    rewrite [algebra.sub_self, -neg_zero],
     apply neg_le_neg,
     apply rat.le_of_lt,
     apply inv_pos
@@ -79,10 +77,11 @@ theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) :
   begin
     rewrite ↑[s_le, nonneg, s_abs, sadd, sneg, const],
     intro m,
-    apply iff.mp !rat.le_add_iff_neg_le_sub_left,
+    rewrite -sub_eq_add_neg,
+    apply iff.mp !le_add_iff_neg_le_sub_left,
     apply rat.le.trans,
     apply Hs,
-    apply rat.add_le_add_right,
+    apply algebra.add_le_add_right,
     rewrite -*pnat.mul.assoc,
     apply inv_ge_of_le,
     apply pnat.mul_le_mul_left
@@ -104,18 +103,18 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a
     existsi 2 * j,
     intro n Hn,
     cases em (s n ≥ 0) with [Hpos, Hneg],
-    rewrite [rat.abs_of_nonneg Hpos, sub_self, abs_zero],
+    rewrite [abs_of_nonneg Hpos, algebra.sub_self, abs_zero],
     apply rat.le_of_lt,
     apply inv_pos,
     let Hneg' := lt_of_not_ge Hneg,
     have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'),
-    rewrite [rat.abs_of_neg Hneg', rat.abs_of_pos Hsn],
+    rewrite [abs_of_neg Hneg', abs_of_pos Hsn],
     apply rat.le.trans,
-    apply rat.add_le_add,
-    repeat (apply rat.neg_le_neg; apply Hz'),
-    rewrite *rat.neg_neg,
+    apply add_le_add,
+    repeat (apply neg_le_neg; apply Hz'),
+    rewrite algebra.neg_neg,
     apply rat.le.trans,
-    apply rat.add_le_add,
+    apply add_le_add,
     repeat (apply inv_ge_of_le; apply Hn),
     rewrite pnat.add_halves,
     apply rat.le.refl
@@ -140,18 +139,18 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
     intro n Hn,
     cases em (s n ≥ 0) with [Hpos, Hneg],
     have Hsn : s n + s n ≥ 0, from add_nonneg Hpos Hpos,
-    rewrite [rat.abs_of_nonneg Hpos, ↑sneg, rat.sub_neg_eq_add, rat.abs_of_nonneg Hsn],
+    rewrite [abs_of_nonneg Hpos, ↑sneg, sub_neg_eq_add, abs_of_nonneg Hsn],
     rewrite [↑nonneg at Hz', ↑sneg at Hz'],
     apply rat.le.trans,
-    apply rat.add_le_add,
-    repeat apply (rat.le_of_neg_le_neg !Hz'),
+    apply add_le_add,
+    repeat apply (le_of_neg_le_neg !Hz'),
     apply rat.le.trans,
-    apply rat.add_le_add,
+    apply add_le_add,
     repeat (apply inv_ge_of_le; apply Hn),
     rewrite pnat.add_halves,
     apply rat.le.refl,
     let Hneg' := lt_of_not_ge Hneg,
-    rewrite [rat.abs_of_neg Hneg', ↑sneg, rat.sub_neg_eq_add, rat.neg_add_eq_sub, rat.sub_self,
+    rewrite [abs_of_neg Hneg', ↑sneg, sub_neg_eq_add, neg_add_eq_sub, algebra.sub_self,
                 abs_zero],
     apply rat.le_of_lt,
     apply inv_pos
@@ -169,10 +168,10 @@ namespace real
 open [classes] rat_seq
 
 private theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) :=
-  by rewrite[-sub_add_eq_sub_sub_swap,sub_add_cancel]
+  by rewrite [-sub_add_eq_sub_sub_swap, algebra.sub_add_cancel]
 
 private theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :=
-  by rewrite[*add_sub,*sub_add_cancel]
+  by rewrite [*add_sub, *algebra.sub_add_cancel]
 
 noncomputable definition rep (x : ℝ) : rat_seq.reg_seq := some (quot.exists_rep x)
 
@@ -185,20 +184,20 @@ theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=
 theorem r_abs_nonpos {x : ℝ} : x ≤ zero → re_abs x = -x :=
   quot.induction_on x (λ a Ha, quot.sound (rat_seq.r_equiv_neg_abs_of_le_zero Ha))
 
-private theorem abs_const' (a : ℚ) : of_rat (rat.abs a) = re_abs (of_rat a) := quot.sound (rat_seq.r_abs_const a)
+private theorem abs_const' (a : ℚ) : of_rat (abs a) = re_abs (of_rat a) := quot.sound (rat_seq.r_abs_const a)
 
-private theorem re_abs_is_abs : re_abs = real.abs := funext
+private theorem re_abs_is_abs : re_abs = abs := funext
   (begin
     intro x,
     apply eq.symm,
     cases em (zero ≤ x) with [Hor1, Hor2],
     rewrite [abs_of_nonneg Hor1, r_abs_nonneg Hor1],
-    have Hor2' : x ≤ zero, from le_of_lt (lt_of_not_ge Hor2),
+    have Hor2' : x ≤ zero, from algebra.le_of_lt (lt_of_not_ge Hor2),
     rewrite [abs_of_neg (lt_of_not_ge Hor2), r_abs_nonpos Hor2']
   end)
 
-theorem abs_const (a : ℚ) : of_rat (rat.abs a) = abs (of_rat a) :=
-  by rewrite -re_abs_is_abs
+theorem abs_const (a : ℚ) : of_rat (abs a) = abs (of_rat a) :=
+  by  rewrite -re_abs_is_abs
 
 private theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - of_rat q) ≤ of_rat n⁻¹ :=
   quot.induction_on x (λ s n, rat_seq.r_rat_approx s n)
@@ -228,9 +227,9 @@ theorem cauchy_with_rate_of_converges_to_with_rate {X : r_seq} {a : ℝ} {N : 
   begin
     intro k m n Hm Hn,
     rewrite (rewrite_helper9 a),
-    apply le.trans,
+    apply algebra.le.trans,
     apply abs_add_le_abs_add_abs,
-    apply le.trans,
+    apply algebra.le.trans,
     apply add_le_add,
     apply Hc,
     apply Hm,
@@ -262,7 +261,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
            abs (of_rat (lim_seq m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
             (X (Nb M n) - of_rat (lim_seq n)) ≤ of_rat (m⁻¹ + n⁻¹) :=
   begin
-    apply le.trans,
+    apply algebra.le.trans,
     apply add_le_add_three,
     apply approx_spec',
     rotate 1,
@@ -277,7 +276,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
     apply Nb_spec_right,
     rewrite [-*of_rat_add, rat.add.assoc, pnat.add_halves],
     apply of_rat_le_of_rat_of_le,
-    apply rat.add_le_add_right,
+    apply add_le_add_right,
     apply inv_ge_of_le,
     apply pnat.mul_le_mul_left
   end
@@ -288,12 +287,12 @@ theorem lim_seq_reg : rat_seq.regular lim_seq :=
     intro m n,
     apply le_of_of_rat_le_of_rat,
     rewrite [abs_const, of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
-    apply real.le.trans,
+    apply algebra.le.trans,
     apply abs_add_three,
     cases em (M (2 * m) ≥ M (2 * n)) with [Hor1, Hor2],
     apply lim_seq_reg_helper Hor1,
     let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2),
-    rewrite [real.abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub,
+    rewrite [abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub,
              rat.add.comm, add_comm_three],
     apply lim_seq_reg_helper Hor2'
   end
@@ -329,9 +328,9 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li
   begin
     intro k n Hn,
     rewrite (rewrite_helper10 (X (Nb M n)) (of_rat (lim_seq n))),
-    apply le.trans,
+    apply algebra.le.trans,
     apply abs_add_three,
-    apply le.trans,
+    apply algebra.le.trans,
     apply add_le_add_three,
     apply Hc,
     apply pnat.le.trans,
@@ -355,7 +354,7 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li
     rewrite [-*of_rat_add],
     apply of_rat_le_of_rat_of_le,
     apply rat.le.trans,
-    apply rat.add_le_add_three,
+    apply add_le_add_three,
     apply rat.le.refl,
     apply inv_ge_of_le,
     apply pnat_mul_le_mul_left',
@@ -403,10 +402,10 @@ theorem archimedean_upper_strict (x : ℝ) : ∃ z : ℤ, x < of_int z :=
   begin
     cases archimedean_upper x with [z, Hz],
     existsi z + 1,
-    apply lt_of_le_of_lt,
+    apply algebra.lt_of_le_of_lt,
     apply Hz,
     apply of_int_lt_of_int_of_lt,
-    apply int.lt_add_of_pos_right,
+    apply lt_add_of_pos_right,
     apply dec_trivial
   end
 
@@ -432,8 +431,8 @@ private definition ex_floor (x : ℝ) :=
       existsi some (archimedean_upper_strict x),
       let Har := some_spec (archimedean_upper_strict x),
       intros z Hz,
-      apply not_le_of_gt,
-      apply lt_of_lt_of_le,
+      apply algebra.not_le_of_gt,
+      apply algebra.lt_of_lt_of_le,
       apply Har,
       have H : of_int (some (archimedean_upper_strict x)) ≤ of_int z, begin
         apply of_int_le_of_int_of_le,
@@ -468,7 +467,7 @@ theorem le_ceil (x : ℝ) : x ≤ ceil x :=
 theorem lt_of_lt_ceil {x : ℝ} {z : ℤ} (Hz : z < ceil x) : z < x :=
   begin
     rewrite ↑ceil at Hz,
-    let Hz' := lt_of_floor_lt (iff.mp !int.lt_neg_iff_lt_neg Hz),
+    let Hz' := lt_of_floor_lt (iff.mp !lt_neg_iff_lt_neg Hz),
     rewrite [of_int_neg at Hz'],
     apply lt_of_neg_lt_neg Hz'
   end
@@ -477,37 +476,39 @@ theorem floor_succ (x : ℝ) : floor (x + 1) = floor x + 1 :=
   begin
     apply by_contradiction,
     intro H,
-    cases int.lt_or_gt_of_ne H with [Hgt, Hlt],
+    cases lt_or_gt_of_ne H with [Hgt, Hlt],
     let Hl := lt_of_floor_lt Hgt,
     rewrite [of_int_add at Hl],
     apply not_le_of_gt (lt_of_add_lt_add_right Hl) !floor_le,
-    let Hl := lt_of_floor_lt (iff.mp !int.add_lt_iff_lt_sub_right Hlt),
+    let Hl := lt_of_floor_lt (iff.mp !add_lt_iff_lt_sub_right Hlt),
     rewrite [of_int_sub at Hl],
     apply not_le_of_gt (iff.mpr !add_lt_iff_lt_sub_right Hl) !floor_le
   end
 
 theorem floor_sub_one_lt_floor (x : ℝ) : floor (x - 1) < floor x :=
   begin
-    apply @int.lt_of_add_lt_add_right _ 1,
+
+    apply @algebra.lt_of_add_lt_add_right ℤ _ _ 1,
     rewrite [-floor_succ (x - 1), sub_add_cancel],
-    apply int.lt_add_of_pos_right dec_trivial
+    apply lt_add_of_pos_right dec_trivial
   end
 
 theorem ceil_lt_ceil_succ (x : ℝ) : ceil x < ceil (x + 1) :=
   begin
     rewrite [↑ceil, neg_add],
-    apply int.neg_lt_neg,
+    apply neg_lt_neg,
     apply floor_sub_one_lt_floor
   end
-
+open nat
+set_option pp.coercions true
 theorem archimedean_small {ε : ℝ} (H : ε > 0) : ∃ (n : ℕ), 1 / succ n < ε :=
 let n := int.nat_abs (ceil (2 / ε)) in
-have int.of_nat n ≥ ceil (2 / ε),
-  by rewrite int.of_nat_nat_abs; apply int.le_abs_self,
+assert int.of_nat n ≥ ceil (2 / ε),
+  by rewrite of_nat_nat_abs; apply le_abs_self,
 have int.of_nat (succ n) ≥ ceil (2 / ε),
-  from int.le.trans this (int.of_nat_le_of_nat_of_le !le_succ),
+  begin apply algebra.le.trans, exact this, apply int.of_nat_le_of_nat_of_le, apply le_succ end,
 have H₁ : succ n ≥ ceil (2 / ε), from of_int_le_of_int_of_le this,
-have H₂ : succ n ≥ 2 / ε, from !le.trans !le_ceil H₁,
+have H₂ : succ n ≥ 2 / ε, from !algebra.le.trans !le_ceil H₁,
 have H₃ : 2 / ε > 0, from div_pos_of_pos_of_pos two_pos H,
 have 1 / succ n < ε, from calc
   1 / succ n ≤ 1 / (2 / ε) : one_div_le_one_div_of_le H₃ H₂
@@ -560,7 +561,7 @@ private theorem under_spec1 : of_rat under < elt :=
     apply of_int_lt_of_int_of_lt,
     apply floor_sub_one_lt_floor
   end,
-  lt_of_lt_of_le H !floor_le
+  algebra.lt_of_lt_of_le H !floor_le
 
 private theorem under_spec : ¬ ub under :=
   begin
@@ -580,14 +581,14 @@ private theorem over_spec1 : bound < of_rat over :=
     apply of_int_lt_of_int_of_lt,
     apply ceil_lt_ceil_succ
   end,
-  lt_of_le_of_lt !le_ceil H
+  algebra.lt_of_le_of_lt !le_ceil H
 
 private theorem over_spec : ub over :=
   begin
     rewrite ↑ub,
     intro y Hy,
-    apply le_of_lt,
-    apply lt_of_le_of_lt,
+    apply algebra.le_of_lt,
+    apply algebra.lt_of_le_of_lt,
     apply bdd,
     apply Hy,
     apply over_spec1
@@ -638,21 +639,23 @@ private theorem over_succ (n : ℕ) : over_seq (succ n) =
     apply H
   end
 
-private theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / (rat.pow 2 n) :=
+private theorem nat.zero_eq_0 : (zero : ℕ) = 0 := rfl
+
+private theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / ((2^n) : ℚ) :=
   nat.induction_on n
-    (by xrewrite [over_0, under_0, rat.pow_zero, rat.div_one])
+    (by xrewrite [nat.zero_eq_0, over_0, under_0, pow_zero, div_one])
     (begin
       intro a Ha,
       rewrite [over_succ, under_succ],
       let Hou := calc
-        (over_seq a) / 2 - (under_seq a) / 2 = ((over - under) / rat.pow 2 a) / 2 :
-                                               by rewrite [rat.div_sub_div_same, Ha]
-        ... = (over - under) / (rat.pow 2 a * 2) : rat.div_div_eq_div_mul
-        ... = (over - under) / rat.pow 2 (a + 1) : by rewrite rat.pow_add,
+        (over_seq a) / 2 - (under_seq a) / 2 = ((over - under) / 2^a) / 2 :
+                                               by rewrite [div_sub_div_same, Ha]
+        ... = (over - under) / ((2^a) * 2) : by rewrite div_div_eq_div_mul
+        ... = (over - under) / 2^(a + 1) : by rewrite pow_add,
       cases em (ub (avg_seq a)),
-      rewrite [*if_pos a_1, -add_one, -Hou, ↑avg_seq, ↑avg, rat.add.assoc, rat.div_two_sub_self],
-      rewrite [*if_neg a_1, -add_one, -Hou, ↑avg_seq, ↑avg, rat.sub_add_eq_sub_sub,
-              rat.sub_self_div_two]
+      rewrite [*if_pos a_1, -add_one, -Hou, ↑avg_seq, ↑avg, sub_eq_add_neg, algebra.add.assoc, -sub_eq_add_neg, div_two_sub_self],
+      rewrite [*if_neg a_1, -add_one, -Hou, ↑avg_seq, ↑avg, sub_add_eq_sub_sub,
+              algebra.sub_self_div_two]
     end)
 
 private theorem width_narrows : ∃ n : ℕ, over_seq n - under_seq n ≤ 1 :=
@@ -660,8 +663,8 @@ private theorem width_narrows : ∃ n : ℕ, over_seq n - under_seq n ≤ 1 :=
     cases binary_bound (over - under) with [a, Ha],
     existsi a,
     rewrite (width a),
-    apply rat.div_le_of_le_mul,
-    apply rat.pow_pos dec_trivial,
+    apply div_le_of_le_mul,
+    apply pow_pos dec_trivial,
     rewrite rat.mul_one,
     apply Ha
   end
@@ -682,17 +685,17 @@ private theorem under_seq'0 : under_seq' 0 = under' :=
 
 private theorem under_over' : over' - under' ≤ 1 := some_spec width_narrows
 
-private theorem width' (n : ℕ) : over_seq' n - under_seq' n ≤ 1 / rat.pow 2 n :=
+private theorem width' (n : ℕ) : over_seq' n - under_seq' n ≤ 1 / 2^n :=
   nat.induction_on n
     (begin
-      xrewrite [over_seq'0, under_seq'0, rat.pow_zero, rat.div_one],
+      xrewrite [nat.zero_eq_0, over_seq'0, under_seq'0, pow_zero, div_one],
       apply under_over'
     end)
     (begin
       intros a Ha,
       rewrite [↑over_seq' at *, ↑under_seq' at *, *succ_add at *, width at *,
-              -add_one, -(add_one a), rat.pow_add, rat.pow_add _ a 1, *rat.pow_one],
-      apply rat.div_mul_le_div_mul_of_div_le_div_pos' Ha dec_trivial
+              -add_one, -(add_one a), pow_add, pow_add _ a 1, *pow_one],
+      apply div_mul_le_div_mul_of_div_le_div_pos' Ha dec_trivial
     end)
 
 private theorem PA (n : ℕ) : ¬ ub (under_seq n) :=
@@ -726,7 +729,7 @@ private theorem under_lt_over : under < over :=
     cases exists_not_of_not_forall under_spec with [x, Hx],
     cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu],
     apply lt_of_of_rat_lt_of_rat,
-    apply lt_of_lt_of_le,
+    apply algebra.lt_of_lt_of_le,
     apply lt_of_not_ge Hxu,
     apply over_spec _ HXx
   end
@@ -737,7 +740,7 @@ private theorem under_seq_lt_over_seq : ∀ m n : ℕ, under_seq m < over_seq n
     cases exists_not_of_not_forall (PA m) with [x, Hx],
     cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu],
     apply lt_of_of_rat_lt_of_rat,
-    apply lt_of_lt_of_le,
+    apply algebra.lt_of_lt_of_le,
     apply lt_of_not_ge Hxu,
     apply PB,
     apply HXx
@@ -764,9 +767,9 @@ private theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i
       rewrite [if_neg Havg, ↑avg_seq, ↑avg],
       apply rat.le.trans,
       apply Ha,
-      rewrite -rat.add_halves at {1},
-      apply rat.add_le_add_right,
-      apply rat.div_le_div_of_le_of_pos,
+      rewrite -add_halves at {1},
+      apply add_le_add_right,
+      apply div_le_div_of_le_of_pos,
       apply rat.le_of_lt,
       apply under_seq_lt_over_seq,
       apply dec_trivial
@@ -778,7 +781,7 @@ private theorem under_seq_mono (i j : ℕ) (H : i ≤ j) : under_seq i ≤ under
     rewrite -Hk',
     apply under_seq_mono_helper
   end
-
+set_option pp.coercions true
 private theorem over_seq_mono_helper (i k : ℕ) : over_seq (i + k) ≤ over_seq i :=
   nat.induction_on k
     (by rewrite nat.add_zero; apply rat.le.refl)
@@ -791,9 +794,9 @@ private theorem over_seq_mono_helper (i k : ℕ) : over_seq (i + k) ≤ over_seq
       rotate 1,
       apply Ha,
       rotate 1,
-      rewrite -{over_seq (i + a)}rat.add_halves at {2},
-      apply rat.add_le_add_left,
-      apply rat.div_le_div_of_le_of_pos,
+      apply add_le_of_le_sub_left,
+      rewrite sub_self_div_two,
+      apply div_le_div_of_le_of_pos,
       apply rat.le_of_lt,
       apply under_seq_lt_over_seq,
       apply dec_trivial,
@@ -808,18 +811,18 @@ private theorem over_seq_mono (i j : ℕ) (H : i ≤ j) : over_seq j ≤ over_se
     apply over_seq_mono_helper
   end
 
-private theorem rat_power_two_inv_ge (k : ℕ+) : 1 / rat.pow 2 k~ ≤ k⁻¹ :=
-  rat.one_div_le_one_div_of_le !rat_of_pnat_is_pos !rat_power_two_le
+private theorem rat_power_two_inv_ge (k : ℕ+) : 1 / 2^k~ ≤ k⁻¹ :=
+  one_div_le_one_div_of_le !rat_of_pnat_is_pos !rat_power_two_le
 
 open rat_seq
 private theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)
         (H : ∀ n i : ℕ+, i ≥ n → under_seq' n~ ≤ s i ∧ s i ≤ over_seq' n~) :
-        rat.abs (s m - s n) ≤ m⁻¹ + n⁻¹ :=
+        abs (s m - s n) ≤ m⁻¹ + n⁻¹ :=
   begin
     cases H m n Hm with [T1under, T1over],
     cases H m m (!pnat.le.refl) with [T2under, T2over],
     apply rat.le.trans,
-    apply rat.dist_bdd_within_interval,
+    apply dist_bdd_within_interval,
     apply under_seq'_lt_over_seq'_single,
     rotate 1,
     repeat assumption,
@@ -827,7 +830,7 @@ private theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)
     apply width',
     apply rat.le.trans,
     apply rat_power_two_inv_ge,
-    apply rat.le_add_of_nonneg_right,
+    apply le_add_of_nonneg_right,
     apply rat.le_of_lt (!inv_pos)
   end
 
@@ -839,7 +842,7 @@ private theorem regular_lemma (s : seq) (H : ∀ n i : ℕ+, i ≥ n → under_s
     cases em (m ≤ n) with [Hm, Hn],
     apply regular_lemma_helper Hm H,
     let T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H,
-    rewrite [rat.abs_sub at T, {n⁻¹ + _}rat.add.comm at T],
+    rewrite [abs_sub at T, {n⁻¹ + _}rat.add.comm at T],
     exact T
   end
 
@@ -853,7 +856,8 @@ private theorem under_seq_regular : regular p_under_seq :=
     intros n i Hni,
     apply and.intro,
     apply under_seq_mono,
-    apply nat.add_le_add_right Hni,
+    apply add_le_add_right,
+    apply Hni,
     apply rat.le_of_lt,
     apply under_seq_lt_over_seq
   end
@@ -866,7 +870,8 @@ private theorem over_seq_regular : regular p_over_seq :=
     apply rat.le_of_lt,
     apply under_seq_lt_over_seq,
     apply over_seq_mono,
-    apply nat.add_le_add_right Hni
+    apply add_le_add_right,
+    apply Hni
   end
 
 private noncomputable definition sup_over : ℝ := quot.mk (reg_seq.mk p_over_seq over_seq_regular)
@@ -890,8 +895,8 @@ private theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y :=
     intro n,
     cases exists_not_of_not_forall (PA _) with [x, Hx],
     cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxn],
-    apply le.trans,
-    apply le_of_lt,
+    apply algebra.le.trans,
+    apply algebra.le_of_lt,
     apply lt_of_not_ge Hxn,
     apply Hy,
     apply HXx
@@ -902,11 +907,11 @@ private theorem under_over_equiv : p_under_seq ≡ p_over_seq :=
     intros,
     apply rat.le.trans,
     have H : p_under_seq n < p_over_seq n, from !under_seq_lt_over_seq,
-    rewrite [rat.abs_of_neg (iff.mpr !rat.sub_neg_iff_lt H), rat.neg_sub],
+    rewrite [abs_of_neg (iff.mpr !sub_neg_iff_lt H), neg_sub],
     apply width',
     apply rat.le.trans,
     apply rat_power_two_inv_ge,
-    apply rat.le_add_of_nonneg_left,
+    apply le_add_of_nonneg_left,
     apply rat.le_of_lt !inv_pos
   end