fix(*): update to lean

.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
 

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]
 

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,

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),

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,

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) →

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

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⟩ },

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]

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] },

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

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 :=

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. -/