diff --git a/.travis.yml b/.travis.yml
index ccbac5ce6ee90..be80891dc5fdc 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -2,7 +2,7 @@ language: generic
 
 install:
   - LEAN_VERSION="lean-3.3.1"
-  - NIGHTLY="nightly-2018-04-02"
+  - NIGHTLY="nightly-2018-04-06"
   - curl https://github.com/leanprover/lean-nightly/releases/download/$NIGHTLY/$LEAN_VERSION-$NIGHTLY-linux.tar.gz -L | tar xz -C ..
   - export PATH=../$LEAN_VERSION-$NIGHTLY-linux/bin:$PATH
 
diff --git a/algebra/group_power.lean b/algebra/group_power.lean
index 86b15357dc3e9..d89db16074aa9 100644
--- a/algebra/group_power.lean
+++ b/algebra/group_power.lean
@@ -121,7 +121,7 @@ attribute [to_additive smul_add_comm] pow_mul_comm
 @list.prod_repeat (multiplicative β) _
 attribute [to_additive list.sum_repeat] list.prod_repeat
 
-def powers (x : α) : set α := {y | ∃ n, x^n = y}
+def powers (x : α) : set α := {y | ∃ n:ℕ, x^n = y}
 
 instance powers.is_submonoid (x : α) : is_submonoid α (powers x) :=
 { one_mem := ⟨0, by simp⟩,
@@ -141,7 +141,7 @@ by rw mul_comm; induction m; simp [succ_smul', nat.mul_succ, *]
 section comm_monoid
 variables [comm_monoid α] {β : Type*} [add_comm_monoid β]
 
-theorem mul_pow (a b : α) : ∀ n, (a * b)^n = a^n * b^n
+theorem mul_pow (a b : α) : ∀ n:ℕ, (a * b)^n = a^n * b^n
 | 0     := by simp
 | (n+1) := by simp [pow_succ, mul_assoc, mul_left_comm]; rw mul_pow
 theorem add_monoid.smul_add : ∀ (a b : β) n, n•(a + b) = n•a + n•b :=
@@ -155,7 +155,7 @@ variables [group α] {β : Type*} [add_group β]
 
 section nat
 
-@[simp] theorem inv_pow (a : α) : ∀n, (a⁻¹)^n = (a^n)⁻¹
+@[simp] theorem inv_pow (a : α) : ∀n:ℕ, (a⁻¹)^n = (a^n)⁻¹
 | 0     := by simp
 | (n+1) := by rw [pow_succ', pow_succ, mul_inv_rev, inv_pow]
 @[simp] theorem add_monoid.neg_smul : ∀ (a : β) n, n•(-a) = -(n•a) :=
@@ -170,7 +170,7 @@ theorem add_monoid.smul_sub : ∀ (a : β) {m n : ℕ}, m ≥ n → (m - n)•a
 @pow_sub (multiplicative β) _
 attribute [to_additive add_monoid.smul_sub] inv_pow
 
-theorem pow_inv_comm (a : α) (m n) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
+theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
 by rw inv_pow; exact inv_comm_of_comm (pow_mul_comm _ _ _)
 theorem add_monoid.smul_neg_comm : ∀ (a : β) m n, m•(-a) + n•a = n•a + m•(-a) :=
 @pow_inv_comm (multiplicative β) _
@@ -237,7 +237,7 @@ theorem neg_one_gsmul (x : β) : (-1:ℤ) • x = -x := by simp
 attribute [to_additive neg_one_gsmul] gpow_neg_one
 
 @[to_additive neg_gsmul]
-theorem inv_gpow (a : α) : ∀n, a⁻¹ ^ n = (a ^ n)⁻¹
+theorem inv_gpow (a : α) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
 | (n : ℕ) := inv_pow a n
 | -[1+ n] := by simp [inv_pow]
 
@@ -332,25 +332,25 @@ by rw [gsmul_eq_mul, gsmul_eq_mul, mul_assoc]
 theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 by induction n with n ih; simp [pow_succ, mul_eq_zero, *]
 
-@[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) : ∀ n, (1 / a) ^ n = 1 / a ^ n
+@[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) : ∀ n : ℕ, (1 / a) ^ n = 1 / a ^ n
 | 0     := by simp
 | (n+1) := by rw [pow_succ', pow_succ,
   ← division_ring.one_div_mul_one_div (pow_ne_zero n ha) ha, one_div_pow]
 
-@[simp] theorem division_ring.inv_pow [division_ring α] {a : α} (ha : a ≠ 0) (n) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
+@[simp] theorem division_ring.inv_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
 by simp [inv_eq_one_div, -one_div_eq_inv, ha]
 
-@[simp] theorem div_pow [field α] (a : α) {b : α} (hb : b ≠ 0) (n) : (a / b) ^ n = a ^ n / b ^ n :=
+@[simp] theorem div_pow [field α] (a : α) {b : α} (hb : b ≠ 0) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n :=
 by rw [div_eq_mul_one_div, mul_pow, one_div_pow hb, ← div_eq_mul_one_div]
 
 theorem add_monoid.smul_nonneg [ordered_comm_monoid α] {a : α} (H : 0 ≤ a) : ∀ n, 0 ≤ n • a
 | 0     := le_refl _
 | (n+1) := add_nonneg' H (add_monoid.smul_nonneg n)
 
-lemma pow_abs [decidable_linear_ordered_comm_ring α] (a : α) (n) : (abs a)^n = abs (a^n) :=
+lemma pow_abs [decidable_linear_ordered_comm_ring α] (a : α) (n : ℕ) : (abs a)^n = abs (a^n) :=
 by induction n; simp [*, pow_succ, abs_mul]
 
-lemma pow_inv [division_ring α] (a : α) : ∀ n, a ≠ 0 → (a^n)⁻¹ = (a⁻¹)^n
+lemma pow_inv [division_ring α] (a : α) : ∀ n : ℕ, a ≠ 0 → (a^n)⁻¹ = (a⁻¹)^n
 | 0     ha := by simp [pow_zero]
 | (n+1) ha := by rw [pow_succ, pow_succ', mul_inv_eq (pow_ne_zero _ ha) ha, pow_inv _ ha]
 
diff --git a/analysis/limits.lean b/analysis/limits.lean
index 8b79b285155bd..c2dde5eb0876c 100644
--- a/analysis/limits.lean
+++ b/analysis/limits.lean
@@ -125,7 +125,7 @@ calc tendsto (f ∘ nat.succ) at_top x ↔ tendsto f (map nat.succ at_top) x : b
  ... ↔ _ : by rw [map_succ_at_top_eq]
 
 lemma tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
-  tendsto (λn, r^n) at_top (nhds 0) :=
+  tendsto (λn:ℕ, r^n) at_top (nhds 0) :=
 by_cases
   (assume : r = 0, tendsto_comp_succ_at_top_iff.mp $ by simp [pow_succ, this, tendsto_const_nhds])
   (assume : r ≠ 0,
@@ -150,7 +150,7 @@ calc (range n).sum (λi, r ^ i) = (range n).sum (λi, ((r - 1) + 1) ^ i) :
     by simp
 
 lemma is_sum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
-  is_sum (λn, r ^ n) (1 / (1 - r)) :=
+  is_sum (λn:ℕ, r ^ n) (1 / (1 - r)) :=
 have r ≠ 1, from ne_of_lt h₂,
 have r + -1 ≠ 0,
   by rw [←sub_eq_add_neg, ne, sub_eq_iff_eq_add]; simp; assumption,
diff --git a/analysis/measure_theory/outer_measure.lean b/analysis/measure_theory/outer_measure.lean
index dd1e0f9235897..2f31ac05b1737 100644
--- a/analysis/measure_theory/outer_measure.lean
+++ b/analysis/measure_theory/outer_measure.lean
@@ -147,8 +147,8 @@ section of_function
 set_option eqn_compiler.zeta true
 
 -- TODO: if we move this proof into the definition of inf it does not terminate anymore
-private lemma aux {ε : ℝ} (hε : 0 < ε) : (∑i, of_real ((ε / 2) * 2⁻¹ ^ i)) = of_real ε :=
-let ε' := λi, (ε / 2) * 2⁻¹ ^ i in
+private lemma aux {ε : ℝ} (hε : 0 < ε) : (∑i:ℕ, of_real ((ε / 2) * 2⁻¹ ^ i)) = of_real ε :=
+let ε' := λi:ℕ, (ε / 2) * 2⁻¹ ^ i in
 have hε' : ∀i, 0 < ε' i,
   from assume i, mul_pos (div_pos_of_pos_of_pos hε two_pos) $ pow_pos (inv_pos two_pos) _,
 have is_sum (λi, 2⁻¹ ^ i : ℕ → ℝ) (1 / (1 - 2⁻¹)),
@@ -178,7 +178,7 @@ let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑i, m (f i) in
     infi_le_infi2 $ assume hb, ⟨subset.trans hs hb, le_refl _⟩,
   Union_nat := assume s, ennreal.le_of_forall_epsilon_le $
     assume ε hε (hb : (∑i, μ (s i)) < ⊤),
-    let ε' := λi, (ε / 2) * 2⁻¹ ^ i in
+    let ε' := λi:ℕ, (ε / 2) * 2⁻¹ ^ i in
     have hε' : ∀i, 0 < ε' i,
       from assume i, mul_pos (div_pos_of_pos_of_pos hε two_pos) $ pow_pos (inv_pos two_pos) _,
     have ∀i, ∃f:ℕ → set α, s i ⊆ (⋃i, f i) ∧ (∑i, m (f i)) < μ (s i) + of_real (ε' i),
diff --git a/data/int/basic.lean b/data/int/basic.lean
index 80304a71a2944..edcb5aa36d9c6 100644
--- a/data/int/basic.lean
+++ b/data/int/basic.lean
@@ -833,11 +833,11 @@ lemma shiftr_add : ∀ (m : ℤ) (n k : ℕ), shiftr m (n + k) = shiftr (shiftr
 | -[1+ m] n k := by rw [shiftr_neg_succ, shiftr_neg_succ,
                         ← int.coe_nat_add, shiftr_neg_succ, nat.shiftr_add]
 
-lemma shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * (2 ^ n : ℕ)
+lemma shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * ↑(2 ^ n)
 | (m : ℕ) n := congr_arg coe (nat.shiftl_eq_mul_pow _ _)
 | -[1+ m] n := @congr_arg ℕ ℤ _ _ (λi, -i) (nat.shiftl'_tt_eq_mul_pow _ _)
 
-lemma shiftr_eq_div_pow : ∀ (m : ℤ) (n : ℕ), shiftr m n = m / (2 ^ n : ℕ)
+lemma shiftr_eq_div_pow : ∀ (m : ℤ) (n : ℕ), shiftr m n = m / ↑(2 ^ n)
 | (m : ℕ) n := by rw shiftr_coe_nat; exact congr_arg coe (nat.shiftr_eq_div_pow _ _)
 | -[1+ m] n := begin
   rw [shiftr_neg_succ, neg_succ_of_nat_div, nat.shiftr_eq_div_pow], refl,
diff --git a/data/nat/sqrt.lean b/data/nat/sqrt.lean
index c9253d09652a4..00c1ef7c68c3e 100644
--- a/data/nat/sqrt.lean
+++ b/data/nat/sqrt.lean
@@ -57,7 +57,7 @@ end
 
 private def is_sqrt (n q : ℕ) : Prop := q*q ≤ n ∧ n < (q+1)*(q+1)
 
-private lemma sqrt_aux_is_sqrt_lemma (m r n)
+private lemma sqrt_aux_is_sqrt_lemma (m r n : ℕ)
   (h₁ : r*r ≤ n)
   (m') (hm : shiftr (2^m * 2^m) 2 = m')
   (H1 : n < (r + 2^m) * (r + 2^m) →
diff --git a/data/pnat.lean b/data/pnat.lean
index ee94a343ab2f8..3a6f616819fe8 100644
--- a/data/pnat.lean
+++ b/data/pnat.lean
@@ -70,6 +70,6 @@ def pow (m : ℕ+) (n : ℕ) : ℕ+ :=
 
 instance : has_pow ℕ+ ℕ := ⟨pow⟩
 
-@[simp] theorem pow_coe (m : ℕ+) (n) : ((m ^ n : ℕ+) : ℕ) = m ^ n := rfl
+@[simp] theorem pow_coe (m : ℕ+) (n : ℕ) : (↑(m ^ n) : ℕ) = m ^ n := rfl
 
 end pnat
diff --git a/group_theory/subgroup.lean b/group_theory/subgroup.lean
index dd2edc80c1f7e..c43704f2ecd0b 100644
--- a/group_theory/subgroup.lean
+++ b/group_theory/subgroup.lean
@@ -98,7 +98,7 @@ lemma group_equiv_cosets_times_subgroup (hs : is_subgroup s) : nonempty (α ≃
 
 end is_subgroup
 
-lemma is_subgroup_range_gpow : is_subgroup (range $ (^) a) :=
+lemma is_subgroup_range_gpow : is_subgroup (range ((^) a : ℤ → α)) :=
 ⟨⟨0, rfl⟩, assume a ⟨i, ha⟩ b ⟨j, hb⟩, ⟨i - j, by simp [gpow_add, gpow_neg, ha.symm, hb.symm]⟩⟩
 
 section finite_group
@@ -113,9 +113,7 @@ have a ^ (i - j) = 1,
   by simp [gpow_add, gpow_neg, a_eq],
 ⟨i - j, sub_ne_zero.mpr ne, this⟩
 
-local infixr `^m`:73 := @has_pow.pow α ℕ monoid.has_pow
-
-lemma exists_pow_eq_one (a : α) : ∃i≠0, a ^m i = 1 :=
+lemma exists_pow_eq_one (a : α) : ∃i≠0, a ^ i = 1 :=
 let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in
 begin
   cases i,
@@ -126,37 +124,37 @@ end
 /-- `order_of a` is the order of the element, i.e. the `n ≥ 1`, s.t. `a ^ n = 1` -/
 def order_of (a : α) : ℕ := nat.find (exists_pow_eq_one a)
 
-lemma pow_order_of_eq_one (a : α) : a ^m order_of a = 1 :=
+lemma pow_order_of_eq_one (a : α) : a ^ order_of a = 1 :=
 let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₂
 
 lemma order_of_ne_zero (a : α) : order_of a ≠ 0 :=
 let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₁
 
 private lemma pow_injective_aux {n m : ℕ} (a : α) (h : n ≤ m)
-  (hn : n < order_of a) (hm : m < order_of a) (eq : a ^m n = a ^m m) : n = m :=
+  (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
 decidable.by_contradiction $ assume ne : n ≠ m,
   have h₁ : m - n ≠ 0, by simp [nat.sub_eq_iff_eq_add h, ne.symm],
-  have h₂ : a ^m (m - n) = 1, by simp [pow_sub _ h, eq],
+  have h₂ : a ^ (m - n) = 1, by simp [pow_sub _ h, eq],
   have le : order_of a ≤ m - n, from nat.find_min' (exists_pow_eq_one a) ⟨h₁, h₂⟩,
   have lt : m - n < order_of a,
     from (nat.sub_lt_left_iff_lt_add h).mpr $ nat.lt_add_left _ _ _ hm,
   lt_irrefl _ (lt_of_le_of_lt le lt)
 
 lemma pow_injective_of_lt_order_of {n m : ℕ} (a : α)
-  (hn : n < order_of a) (hm : m < order_of a) (eq : a ^m n = a ^m m) : n = m :=
+  (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
 (le_total n m).elim
   (assume h, pow_injective_aux a h hn hm eq)
   (assume h, (pow_injective_aux a h hm hn eq.symm).symm)
 
 lemma order_of_le_card_univ : order_of a ≤ fintype.card α :=
-finset.card_le_of_inj_on ((^m) a)
+finset.card_le_of_inj_on ((^) a)
   (assume n _, fintype.complete _)
   (assume i j, pow_injective_of_lt_order_of a)
 
-lemma pow_eq_mod_order_of {n : ℕ} : a ^m n = a ^m (n % order_of a) :=
-calc a ^m n = a ^m (n % order_of a + order_of a * (n / order_of a)) :
+lemma pow_eq_mod_order_of {n : ℕ} : a ^ n = a ^ (n % order_of a) :=
+calc a ^ n = a ^ (n % order_of a + order_of a * (n / order_of a)) :
     by rw [nat.mod_add_div]
-  ... = a ^m (n % order_of a) :
+  ... = a ^ (n % order_of a) :
     by simp [pow_add, pow_mul, pow_order_of_eq_one]
 
 lemma gpow_eq_mod_order_of {i : ℤ} : a ^ i = a ^ (i % order_of a) :=
@@ -166,20 +164,20 @@ calc a ^ i = a ^ (i % order_of a + order_of a * (i / order_of a)) :
     by simp [gpow_add, gpow_mul, pow_order_of_eq_one]
 
 lemma mem_range_gpow_iff_mem_range_order_of {a a' : α} :
-  a' ∈ range ((^) a) ↔ a' ∈ (finset.range (order_of a)).image ((^m) a) :=
+  a' ∈ range ((^) a : ℤ → α) ↔ a' ∈ (finset.range (order_of a)).image ((^) a : ℕ → α) :=
 finset.mem_range_iff_mem_finset_range_of_mod_eq
   (nat.pos_iff_ne_zero.mpr (order_of_ne_zero a))
   (assume i, gpow_eq_mod_order_of.symm)
 
-instance decidable_range_gpow : decidable_pred (range ((^) a)) :=
-assume a', decidable_of_iff
-  (a' ∈ (finset.range (order_of a)).image ((^m) a))
-  mem_range_gpow_iff_mem_range_order_of.symm
+instance decidable_range_gpow : decidable_pred (range ((^) a : ℤ → α)) :=
+assume a', decidable_of_iff'
+  (a' ∈ (finset.range (order_of a)).image ((^) a))
+  mem_range_gpow_iff_mem_range_order_of
 
 section
 local attribute [instance] set_fintype
 
-lemma order_eq_card_range_gpow : order_of a = fintype.card (range ((^) a)) :=
+lemma order_eq_card_range_gpow : order_of a = fintype.card (range ((^) a : ℤ → α)) :=
 begin
   refine (finset.card_eq_of_bijective _ _ _ _).symm,
   { exact λn hn, ⟨gpow a n, mem_range_self n⟩ },
diff --git a/leanpkg.toml b/leanpkg.toml
index 00eb1b3fdc69e..e2df7dd914258 100644
--- a/leanpkg.toml
+++ b/leanpkg.toml
@@ -1,6 +1,6 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "nightly-2018-04-02"
+lean_version = "nightly-2018-04-06"
 
 [dependencies]
diff --git a/linear_algebra/multivariate_polynomial.lean b/linear_algebra/multivariate_polynomial.lean
index f84c0ad84fdf5..0f1cef5d91848 100644
--- a/linear_algebra/multivariate_polynomial.lean
+++ b/linear_algebra/multivariate_polynomial.lean
@@ -156,7 +156,7 @@ begin
   apply @finsupp.single_induction_on σ ℕ _ _ s,
   { show M (monomial 0 a), from h_C a, },
   { assume n e p hpn he ih,
-    have : ∀e, M (monomial p a * X n ^ e),
+    have : ∀e:ℕ, M (monomial p a * X n ^ e),
     { intro e,
       induction e,
       { simp [ih] },
diff --git a/number_theory/pell.lean b/number_theory/pell.lean
index 99ed81ebc4e9c..74c416633aafe 100644
--- a/number_theory/pell.lean
+++ b/number_theory/pell.lean
@@ -830,14 +830,14 @@ section
   ... = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0) : by simp [mul_add]
 
   theorem x_sub_y_dvd_pow (y : ℕ) :
-    ∀ n, (2*a*y - y*y - 1 : ℤ) ∣ yz n * (a - y) + (y^n:ℕ) - xz n
+    ∀ n, (2*a*y - y*y - 1 : ℤ) ∣ yz n * (a - y) + ↑(y^n) - xz n
   | 0 := by simp [xz, yz, int.coe_nat_zero, int.coe_nat_one]
   | 1 := by simp [xz, yz, int.coe_nat_zero, int.coe_nat_one]
   | (n+2) :=
     have (2*a*y - y*y - 1 : ℤ) ∣ ↑(y^(n + 2)) - ↑(2 * a) * ↑(y^(n + 1)) + ↑(y^n), from
     ⟨-↑(y^n), by simp [nat.pow_succ, mul_add, int.coe_nat_mul,
         show ((2:ℕ):ℤ) = 2, from rfl, mul_comm, mul_left_comm]⟩,
-    by rw [xz_succ_succ, yz_succ_succ, x_sub_y_dvd_pow_lem a1 (y^(n+2):ℕ) (y^(n+1):ℕ) (y^n:ℕ)]; exact
+    by rw [xz_succ_succ, yz_succ_succ, x_sub_y_dvd_pow_lem a1 ↑(y^(n+2)) ↑(y^(n+1)) ↑(y^n)]; exact
     dvd_sub (dvd_add this $ dvd_mul_of_dvd_right (x_sub_y_dvd_pow (n+1)) _) (x_sub_y_dvd_pow n)
 
   theorem xn_modeq_x2n_add_lem (n j) : xn n ∣ d * yn n * (yn n * xn j) + xn j :=
@@ -1105,7 +1105,7 @@ a > 1 ∧ k ≤ y ∧
 end⟩⟩
 
 lemma eq_pow_of_pell_lem {a y k} (a1 : 1 < a) (ypos : y > 0) : k > 0 → a > y^k →
-  ((y^k:ℕ) : ℤ) < 2*a*y - y*y - 1 :=
+  (↑(y^k) : ℤ) < 2*a*y - y*y - 1 :=
 have y < a → 2*a*y ≥ a + (y*y + 1), begin
   intro ya, induction y with y IH, exact absurd ypos (lt_irrefl _),
   cases nat.eq_zero_or_pos y with y0 ypos,
@@ -1148,7 +1148,7 @@ k = 0 ∧ m = 1 ∨ k > 0 ∧
   let x := xn a1 k, y := yn a1 k in
   let ⟨z, ze⟩ := show w ∣ yn w1 w, from modeq.modeq_zero_iff.1 $
     modeq.trans (yn_modeq_a_sub_one w1 w) (modeq.modeq_zero_iff.2 $ dvd_refl _) in
-  have nt : ((n^k:ℕ) : ℤ) < 2 * a * n - n * n - 1, from
+  have nt : (↑(n^k) : ℤ) < 2 * a * n - n * n - 1, from
     eq_pow_of_pell_lem a1 npos kpos $ calc
       n^k ≤ n^w       : nat.pow_le_pow_of_le_right npos kw
       ... < (w + 1)^w : nat.pow_lt_pow_of_lt_left (nat.lt_succ_of_le nw) wpos
@@ -1198,7 +1198,7 @@ k = 0 ∧ m = 1 ∨ k > 0 ∧
   have wj : w ≤ j, from nat.le_of_dvd jpos $ modeq.modeq_zero_iff.1 $
     (yn_modeq_a_sub_one w1 j).symm.trans $
     modeq.modeq_zero_iff.2 ⟨z, yj.symm⟩,
-  have nt : ((n^k:ℕ) : ℤ) < 2 * a * n - n * n - 1, from
+  have nt : (↑(n^k) : ℤ) < 2 * a * n - n * n - 1, from
     eq_pow_of_pell_lem a1 npos kpos $ calc
       n^k ≤ n^j       : nat.pow_le_pow_of_le_right npos (le_trans kw wj)
       ... < (w + 1)^j : nat.pow_lt_pow_of_lt_left (nat.lt_succ_of_le nw) jpos
diff --git a/set_theory/cardinal.lean b/set_theory/cardinal.lean
index d219f9a5248a0..a2974ac464a70 100644
--- a/set_theory/cardinal.lean
+++ b/set_theory/cardinal.lean
@@ -140,7 +140,8 @@ protected def power (a b : cardinal.{u}) : cardinal.{u} :=
 quotient.lift_on₂ a b (λα β, mk (β → α)) $ assume α₁ α₂ β₁ β₂ ⟨e₁⟩ ⟨e₂⟩,
   quotient.sound ⟨equiv.arrow_congr e₂ e₁⟩
 
-local notation a ^ b := cardinal.power a b
+instance : has_pow cardinal cardinal := ⟨cardinal.power⟩
+local infixr ^ := @has_pow.pow cardinal cardinal cardinal.has_pow
 
 @[simp] theorem power_def (α β) : mk α ^ mk β = mk (β → α) := rfl
 
@@ -526,7 +527,7 @@ theorem fintype_card (α : Type u) [fintype α] : mk α = fintype.card α :=
 by rw [← lift_mk_fin.{u}, ← lift_id (mk α), lift_mk_eq.{u 0 u}];
    exact fintype.card_eq.1 (by simp)
 
-@[simp] theorem nat_cast_pow {m n : ℕ} : (@has_pow.pow _ _ _ m n : cardinal) = m ^ n :=
+@[simp] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
 by induction n; simp [nat.pow_succ, -_root_.add_comm, power_add, *]
 
 @[simp] theorem nat_cast_le {m n : ℕ} : (m : cardinal) ≤ n ↔ m ≤ n :=
diff --git a/set_theory/cofinality.lean b/set_theory/cofinality.lean
index a64897545e96d..668bfb6f73334 100644
--- a/set_theory/cofinality.lean
+++ b/set_theory/cofinality.lean
@@ -315,7 +315,7 @@ end ordinal
 namespace cardinal
 open ordinal
 
-local infix ` ^ ` := cardinal.power
+local infixr ^ := @pow cardinal.{u} cardinal cardinal.has_pow
 
 /-- A cardinal is a limit if it is not zero or a successor
   cardinal. Note that `ω` is a limit cardinal by this definition. -/
diff --git a/set_theory/ordinal.lean b/set_theory/ordinal.lean
index a4fdc780b6c33..1b240656baa91 100644
--- a/set_theory/ordinal.lean
+++ b/set_theory/ordinal.lean
@@ -1921,24 +1921,25 @@ def power (a b : ordinal) : ordinal :=
 if a = 0 then 1 - b else
 limit_rec_on b 1 (λ _ IH, IH * a) (λ b _, bsup.{u u} b)
 
-local infixr ` ^ ` := power
+instance : has_pow ordinal ordinal := ⟨power⟩
+local infixr ^ := @pow ordinal ordinal ordinal.has_pow
 
 theorem zero_power' (a : ordinal) : 0 ^ a = 1 - a :=
-by simp [power]
+by simp [pow, power]
 
 @[simp] theorem zero_power {a : ordinal} (a0 : a ≠ 0) : 0 ^ a = 0 :=
 by rwa [zero_power', sub_eq_zero_iff_le, one_le_iff_ne_zero]
 
 @[simp] theorem power_zero (a : ordinal) : a ^ 0 = 1 :=
-by by_cases a = 0; simp [power, h]
+by by_cases a = 0; simp [pow, power, h]
 
 @[simp] theorem power_succ (a b : ordinal) : a ^ succ b = a ^ b * a :=
 if h : a = 0 then by subst a; simp [succ_ne_zero]
-else by simp [power, h]
+else by simp [pow, power, h]
 
 theorem power_limit {a b : ordinal} (a0 : a ≠ 0) (h : is_limit b) :
   a ^ b = bsup.{u u} b (λ c _, a ^ c) :=
-by simp [power, a0]; rw limit_rec_on_limit _ _ _ _ h; refl
+by simp [pow, power, a0]; rw limit_rec_on_limit _ _ _ _ h; refl
 
 theorem power_le_of_limit {a b c : ordinal} (a0 : a ≠ 0) (h : is_limit b) :
   a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c :=
@@ -1978,7 +1979,7 @@ pos_iff_ne_zero.1 $ power_pos b $ pos_iff_ne_zero.2 a0
 
 theorem power_is_normal {a : ordinal} (h : 1 < a) : is_normal ((^) a) :=
 have a0 : 0 < a, from lt_trans zero_lt_one h,
-⟨λ b, by rw power_succ; simpa using
+⟨λ b, by simpa using
   (mul_lt_mul_iff_left (power_pos b a0)).2 h,
  λ b l c, power_le_of_limit (ne_of_gt a0) l⟩
 
@@ -2178,7 +2179,7 @@ else by simp [b1, zero_le]
 by induction n with n IH; [simp, rw [nat.mul_succ,
   nat.cast_add, IH, nat.cast_succ, mul_add_one]]
 
-@[simp] theorem nat_cast_power {m n} : (@has_pow.pow ℕ ℕ _ m n : ordinal) = m ^ n :=
+@[simp] theorem nat_cast_power {m n : ℕ} : ((pow m n : ℕ) : ordinal) = m ^ n :=
 by induction n with n IH; [simp, rw [nat.pow_succ,
   nat_cast_mul, IH, nat.cast_succ, ← succ_eq_add_one, power_succ]]
 
@@ -2331,7 +2332,7 @@ begin
     intro e, simp [e] }
 end
 
-local infixr ` ^ ` := power
+local infixr ^ := @pow ordinal ordinal ordinal.has_pow
 
 theorem power_lt_omega {a b : ordinal} (ha : a < omega) (hb : b < omega) : a ^ b < omega :=
 match a, b, lt_omega.1 ha, lt_omega.1 hb with
@@ -2438,11 +2439,11 @@ theorem mul_omega_dvd {a : ordinal}
   (a0 : 0 < a) (ha : a < omega) : ∀ {b}, omega ∣ b → a * b = b
 | _ ⟨b, rfl⟩ := by rw [← mul_assoc, mul_omega a0 ha]
 
-theorem mul_omega_power_power {a b : ordinal} (a0 : 0 < a) (h : a < omega ^ (omega ^ b)) :
-  a * omega ^ (omega ^ b) = omega ^ (omega ^ b) :=
+theorem mul_omega_power_power {a b : ordinal} (a0 : 0 < a) (h : a < omega ^ omega ^ b) :
+  a * omega ^ omega ^ b = omega ^ omega ^ b :=
 begin
   by_cases b0 : b = 0, {simp [b0] at h ⊢, simp [mul_omega a0 h]},
-  refine le_antisymm _ (by simpa using mul_le_mul_right (omega^(omega^b)) (one_le_iff_pos.2 a0)),
+  refine le_antisymm _ (by simpa using mul_le_mul_right (omega^omega^b) (one_le_iff_pos.2 a0)),
   rcases (lt_power_of_limit omega_ne_zero (power_is_limit_left omega_is_limit b0)).1 h
     with ⟨x, xb, ax⟩,
   refine le_trans (mul_le_mul_right _ (le_of_lt ax)) _,
diff --git a/set_theory/ordinal_notation.lean b/set_theory/ordinal_notation.lean
index 327606b454cb6..41e78c71d0bfe 100644
--- a/set_theory/ordinal_notation.lean
+++ b/set_theory/ordinal_notation.lean
@@ -8,8 +8,7 @@ Ordinal notations (constructive ordinal arithmetic for ordinals < ε₀).
 import set_theory.ordinal data.pnat
 open ordinal
 
-local infixr ` ^ ` := power
-local notation `ω` := omega
+local notation `ω` := omega.{0}
 
 /-- Recursive definition of an ordinal notation. `zero` denotes the
   ordinal 0, and `oadd e n a` is intended to refer to `ω^e * n + a`.
@@ -533,6 +532,10 @@ match split o₁ with
   end
 end
 
+instance : has_pow onote onote := ⟨power⟩
+
+theorem power_def (o₁ o₂ : onote) : o₁ ^ o₂ = power._match_1 o₂ (split o₁) := rfl
+
 theorem split_eq_scale_split' : ∀ {o o' m} [NF o], split' o = (o', m) → split o = (scale 1 o', m)  
 | 0            o' m h p := by injection p; substs o' m; refl
 | (oadd e n a) o' m h p := begin
@@ -559,7 +562,7 @@ theorem NF_repr_split' : ∀ {o o' m} [NF o], split' o = (o', m) → NF o' ∧ r
     cases NF_repr_split' h' with IH₁ IH₂,
     simp [IH₂, split'],
     intros, substs o' m,
-    have : ω ^ repr e = ω ^ 1 * ω ^ (repr e - 1),
+    have : ω ^ repr e = ω ^ (1 : ordinal.{0}) * ω ^ (repr e - 1),
     { have := mt repr_inj.1 e0,
       rw [← power_add, add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)] },
     refine ⟨NF.oadd (by apply_instance) _ _, _⟩,
@@ -625,7 +628,7 @@ instance NF_power_aux (e a0 a) [NF e] [NF a0] [NF a] : ∀ k m, NF (power_aux e
 | (k+1) (m+1) := by haveI := NF_power_aux k;
   simp [power_aux, nat.succ_ne_zero]; apply_instance
 
-instance NF_power (o₁ o₂) [NF o₁] [NF o₂] : NF (power o₁ o₂) :=
+instance NF_power (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) :=
 begin
   cases e₁ : split o₁ with a m,
   have na := (NF_repr_split e₁).1,
@@ -633,9 +636,9 @@ begin
   haveI := (NF_repr_split' e₂).1,
   cases a with a0 n a',
   { cases m with m,
-    { by_cases o₂ = 0; simp [power, e₁, h]; apply_instance },
-    { by_cases m = 0; simp [power, e₁, e₂, h]; apply_instance } },
-  { simp [power, e₁, e₂, split_eq_scale_split' e₂],
+    { by_cases o₂ = 0; simp [pow, power, e₁, h]; apply_instance },
+    { by_cases m = 0; simp [pow, power, e₁, e₂, h]; apply_instance } },
+  { simp [pow, power, e₁, e₂, split_eq_scale_split' e₂],
     have := na.fst,
     cases k with k; simp [succ_eq_add_one, power]; apply_instance }
 end
@@ -670,6 +673,9 @@ begin
     simpa using mul_le_mul_right ω (one_le_iff_ne_zero.2 e0) }
 end
 
+section
+local infixr ^ := @pow ordinal.{0} ordinal ordinal.has_pow
+
 theorem repr_power_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ)
   (d : ω ∣ repr a')
   (e0 : repr a0 ≠ 0) (h : repr a' + m < ω ^ repr a0) (n : ℕ+) (k : ℕ) :
@@ -735,17 +741,19 @@ begin
       simpa [α', repr] using omega_le_oadd a0 n a' } }
 end
 
-theorem repr_power (o₁ o₂) [NF o₁] [NF o₂] : repr (power o₁ o₂) = (repr o₁).power (repr o₂) :=
+end
+
+theorem repr_power (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o₁ ^ repr o₂ :=
 begin
   cases e₁ : split o₁ with a m,
   cases NF_repr_split e₁ with N₁ r₁,
   cases a with a0 n a',
   { cases m with m,
-    { by_cases o₂ = 0; simp [power, e₁, h, r₁],
+    { by_cases o₂ = 0; simp [power_def, power, e₁, h, r₁],
       have := mt repr_inj.1 h, rw zero_power this },
     { cases e₂ : split' o₂ with b' k,
       cases NF_repr_split' e₂ with _ r₂,
-      by_cases m = 0; simp [power, e₁, h, r₁, e₂, r₂, -nat.cast_succ],
+      by_cases m = 0; simp [power_def, power, e₁, h, r₁, e₂, r₂, -nat.cast_succ],
       rw [power_add, power_mul, power_omega _ (nat_lt_omega _)],
       simpa using nat_cast_lt.2 (nat.succ_lt_succ $ nat.pos_iff_ne_zero.2 h) } },
   { haveI := N₁.fst, haveI := N₁.snd,
@@ -754,7 +762,7 @@ begin
     have aa : repr (a' + of_nat m) = repr a' + m, {simp},
     cases e₂ : split' o₂ with b' k,
     cases NF_repr_split' e₂ with _ r₂,
-    simp [power, e₁, r₁, split_eq_scale_split' e₂],
+    simp [power_def, power, e₁, r₁, split_eq_scale_split' e₂],
     cases k with k,
     { simp [power, r₂, power_mul, repr_power_aux₁ a00 al aa] },
     { simp [succ_eq_add_one, power, r₂, power_add, power_mul, mul_assoc],
diff --git a/tactic/ring.lean b/tactic/ring.lean
index 472ba4d5432c2..8dca2eb8b7512 100644
--- a/tactic/ring.lean
+++ b/tactic/ring.lean
@@ -311,8 +311,8 @@ do α0 ← expr.of_nat c.α 0,
    return (c.cs_app ``horner [α1, e, n1, α0], c.cs_app ``horner_atom [e])
 
 lemma subst_into_pow {α} [monoid α] (l r tl tr t)
-  (prl : l = tl) (prr : r = tr) (prt : (tl : α) ^ tr = t) : l ^ r = t :=
-by simp [prl, prr, prt]
+  (prl : (l : α) = tl) (prr : (r : ℕ) = tr) (prt : tl ^ tr = t) : l ^ r = t :=
+by simp [prl, prr, prt] 
 
 meta def eval (c : cache) : expr → tactic (expr × expr)
 | `(%%e₁ + %%e₂) := do
@@ -363,10 +363,10 @@ by simp [horner, mul_comm]
 theorem mul_assoc_rev {α} [semigroup α] (a b c : α) : a * (b * c) = a * b * c :=
 by simp [mul_assoc]
 
-theorem pow_add_rev {α} [monoid α] (a b : α) (m n) : a ^ m * a ^ n = a ^ (m + n) :=
+theorem pow_add_rev {α} [monoid α] (a b : α) (m n : ℕ) : a ^ m * a ^ n = a ^ (m + n) :=
 by simp [pow_add]
 
-theorem pow_add_rev_right {α} [monoid α] (a b : α) (m n) : b * a ^ m * a ^ n = b * a ^ (m + n) :=
+theorem pow_add_rev_right {α} [monoid α] (a b : α) (m n : ℕ) : b * a ^ m * a ^ n = b * a ^ (m + n) :=
 by simp [pow_add, mul_assoc]
 
 theorem add_neg_eq_sub {α : Type u} [add_group α] (a b : α) : a + -b = a - b := rfl