From a084bd518bdc76e34834d5fd57bc6a5024530d9d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 9 Nov 2023 04:02:44 +0000 Subject: [PATCH] style(SetTheory): remove useless parentheses (#8279) These were caused by a bad notation precedence in mathlib3, where the local version of `^` was given precedence 0. We're not using the local notation at all in Mathlib4 (partly because it was broken, which this PR fixes). --- Mathlib/SetTheory/Cardinal/Basic.lean | 71 +++++++------ Mathlib/SetTheory/Cardinal/Ordinal.lean | 2 +- Mathlib/SetTheory/Ordinal/Exponential.lean | 117 +++++++++++---------- 3 files changed, 96 insertions(+), 94 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index acf217ffe7bdc..389766475abf1 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -65,7 +65,7 @@ We define cardinal numbers as a quotient of types under the equivalence relation * There is an instance `Pow Cardinal`, but this will only fire if Lean already knows that both the base and the exponent live in the same universe. As a workaround, you can add ``` - local infixr:0 "^'" => @Pow.pow Cardinal Cardinal Cardinal.instPowCardinal + local infixr:80 " ^' " => @HPow.hPow Cardinal Cardinal Cardinal _ ``` to a file. This notation will work even if Lean doesn't know yet that the base and the exponent live in the same universe (but no exponents in other types can be used). @@ -489,7 +489,7 @@ instance instPowCardinal : Pow Cardinal.{u} Cardinal.{u} := -- with `HPow`, but somebody should figure out -- if this is still relevant in Lean4. -- mathport name: cardinal.pow -local infixr:0 "^'" => @HPow.hPow Cardinal Cardinal Cardinal.instPowCardinal +local infixr:80 " ^' " => @HPow.hPow Cardinal Cardinal Cardinal _ -- -- mathport name: cardinal.pow.nat local infixr:80 " ^ℕ " => @HPow.hPow Cardinal ℕ Cardinal instHPow @@ -502,22 +502,22 @@ theorem mk_arrow (α : Type u) (β : Type v) : #(α → β) = (lift.{u} #β^lift #align cardinal.mk_arrow Cardinal.mk_arrow @[simp] -theorem lift_power (a b : Cardinal.{u}) : lift.{v} (a ^ b) = ((lift.{v} a) ^ (lift.{v} b)) := +theorem lift_power (a b : Cardinal.{u}) : lift.{v} (a ^ b) = lift.{v} a ^ lift.{v} b := inductionOn₂ a b fun _ _ => mk_congr <| Equiv.ulift.trans (Equiv.ulift.arrowCongr Equiv.ulift).symm #align cardinal.lift_power Cardinal.lift_power @[simp] -theorem power_zero {a : Cardinal} : (a ^ 0) = 1 := +theorem power_zero {a : Cardinal} : a ^ 0 = 1 := inductionOn a fun _ => mk_eq_one _ #align cardinal.power_zero Cardinal.power_zero @[simp] -theorem power_one {a : Cardinal.{u}} : (a ^ 1) = a := +theorem power_one {a : Cardinal.{u}} : a ^ 1 = a := inductionOn a fun α => mk_congr (Equiv.funUnique (ULift.{u} (Fin 1)) α) #align cardinal.power_one Cardinal.power_one -theorem power_add {a b c : Cardinal} : (a ^ (b + c)) = (a ^ b) * (a ^ c) := +theorem power_add {a b c : Cardinal} : a ^ (b + c) = a ^ b * a ^ c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumArrowEquivProdArrow β γ α #align cardinal.power_add Cardinal.power_add @@ -538,9 +538,9 @@ instance commSemiring : CommSemiring Cardinal.{u} where mul_comm := mul_comm' left_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodSumDistrib α β γ right_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumProdDistrib α β γ - npow n c := c^n + npow n c := c ^ n npow_zero := @power_zero - npow_succ n c := show (c ^ (n + 1 : ℕ)) = c * (c ^ n) + npow_succ n c := show c ^ (n + 1 : ℕ) = c * (c ^ n) by rw [Cardinal.cast_succ, power_add, power_one, mul_comm'] natCast := (fun n => lift.{u} #(Fin n) : ℕ → Cardinal.{u}) natCast_zero := rfl @@ -551,19 +551,19 @@ section deprecated set_option linter.deprecated false @[deprecated] -theorem power_bit0 (a b : Cardinal) : (a ^ bit0 b) = (a ^ b) * (a ^ b) := +theorem power_bit0 (a b : Cardinal) : a ^ bit0 b = a ^ b * a ^ b := power_add #align cardinal.power_bit0 Cardinal.power_bit0 @[deprecated] -theorem power_bit1 (a b : Cardinal) : (a ^ bit1 b) = (a ^ b) * (a ^ b) * a := by +theorem power_bit1 (a b : Cardinal) : a ^ bit1 b = a ^ b * a ^ b * a := by rw [bit1, ← power_bit0, power_add, power_one] #align cardinal.power_bit1 Cardinal.power_bit1 end deprecated @[simp] -theorem one_power {a : Cardinal} : (1 ^ a) = 1 := +theorem one_power {a : Cardinal} : 1 ^ a = 1 := inductionOn a fun _ => mk_eq_one _ #align cardinal.one_power Cardinal.one_power @@ -578,7 +578,7 @@ theorem mk_Prop : #Prop = 2 := by simp #align cardinal.mk_Prop Cardinal.mk_Prop @[simp] -theorem zero_power {a : Cardinal} : a ≠ 0 → (0 ^ a) = 0 := +theorem zero_power {a : Cardinal} : a ≠ 0 → 0 ^ a = 0 := inductionOn a fun _ heq => mk_eq_zero_iff.2 <| isEmpty_pi.2 <| @@ -586,23 +586,23 @@ theorem zero_power {a : Cardinal} : a ≠ 0 → (0 ^ a) = 0 := ⟨a, inferInstance⟩ #align cardinal.zero_power Cardinal.zero_power -theorem power_ne_zero {a : Cardinal} (b) : a ≠ 0 → (a ^ b) ≠ 0 := +theorem power_ne_zero {a : Cardinal} (b : Cardinal) : a ≠ 0 → a ^ b ≠ 0 := inductionOn₂ a b fun _ _ h => let ⟨a⟩ := mk_ne_zero_iff.1 h mk_ne_zero_iff.2 ⟨fun _ => a⟩ #align cardinal.power_ne_zero Cardinal.power_ne_zero -theorem mul_power {a b c : Cardinal} : ((a * b) ^ c) = (a ^ c) * (b ^ c) := +theorem mul_power {a b c : Cardinal} : (a * b) ^ c = a ^ c * b ^ c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.arrowProdEquivProdArrow α β γ #align cardinal.mul_power Cardinal.mul_power -theorem power_mul {a b c : Cardinal} : (a ^ (b * c)) = ((a ^ b) ^ c) := by +theorem power_mul {a b c : Cardinal} : a ^ (b * c) = (a ^ b) ^ c := by rw [mul_comm b c] exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α #align cardinal.power_mul Cardinal.power_mul @[simp] -theorem pow_cast_right (a : Cardinal.{u}) (n : ℕ) : (a^(↑n : Cardinal.{u})) = a ^ℕ n := +theorem pow_cast_right (a : Cardinal.{u}) (n : ℕ) : a ^ (↑n : Cardinal.{u}) = a ^ℕ n := rfl #align cardinal.pow_cast_right Cardinal.pow_cast_right @@ -642,16 +642,17 @@ theorem lift_two : lift.{u, v} 2 = 2 := by simp [←one_add_one_eq_two] #align cardinal.lift_two Cardinal.lift_two @[simp] -theorem mk_set {α : Type u} : #(Set α) = (2 ^ #α) := by simp [←one_add_one_eq_two, Set, mk_arrow] +theorem mk_set {α : Type u} : #(Set α) = 2 ^ #α := by simp [←one_add_one_eq_two, Set, mk_arrow] #align cardinal.mk_set Cardinal.mk_set /-- A variant of `Cardinal.mk_set` expressed in terms of a `Set` instead of a `Type`. -/ @[simp] -theorem mk_powerset {α : Type u} (s : Set α) : #(↥(𝒫 s)) = (2 ^ #(↥s)) := +theorem mk_powerset {α : Type u} (s : Set α) : #(↥(𝒫 s)) = 2 ^ #(↥s) := (mk_congr (Equiv.Set.powerset s)).trans mk_set #align cardinal.mk_powerset Cardinal.mk_powerset -theorem lift_two_power (a) : lift.{v} (2 ^ a) = (2 ^ lift.{v} a) := by simp [←one_add_one_eq_two] +theorem lift_two_power (a : Cardinal) : lift.{v} (2 ^ a) = 2 ^ lift.{v} a := by + simp [←one_add_one_eq_two] #align cardinal.lift_two_power Cardinal.lift_two_power section OrderProperties @@ -714,20 +715,20 @@ instance : CommMonoidWithZero Cardinal.{u} := instance : CommMonoid Cardinal.{u} := { Cardinal.canonicallyOrderedCommSemiring with } -theorem zero_power_le (c : Cardinal.{u}) : ((0 : Cardinal.{u})^c) ≤ 1 := by +theorem zero_power_le (c : Cardinal.{u}) : (0 : Cardinal.{u}) ^ c ≤ 1 := by by_cases h : c = 0 · rw [h, power_zero] · rw [zero_power h] apply zero_le #align cardinal.zero_power_le Cardinal.zero_power_le -theorem power_le_power_left : ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → (a^b) ≤ (a^c) := by +theorem power_le_power_left : ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c := by rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩ let ⟨a⟩ := mk_ne_zero_iff.1 hα exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩ #align cardinal.power_le_power_left Cardinal.power_le_power_left -theorem self_le_power (a : Cardinal) {b : Cardinal} (hb : 1 ≤ b) : a ≤ (a^b) := by +theorem self_le_power (a : Cardinal) {b : Cardinal} (hb : 1 ≤ b) : a ≤ a ^ b := by rcases eq_or_ne a 0 with (rfl | ha) · exact zero_le _ · convert power_le_power_left ha hb @@ -735,7 +736,7 @@ theorem self_le_power (a : Cardinal) {b : Cardinal} (hb : 1 ≤ b) : a ≤ (a^b) #align cardinal.self_le_power Cardinal.self_le_power /-- **Cantor's theorem** -/ -theorem cantor (a : Cardinal.{u}) : a < (2^a) := by +theorem cantor (a : Cardinal.{u}) : a < 2 ^ a := by induction' a using Cardinal.inductionOn with α rw [← mk_set] refine' ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, _⟩ @@ -752,17 +753,17 @@ theorem one_lt_iff_nontrivial {α : Type u} : 1 < #α ↔ Nontrivial α := by rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not] #align cardinal.one_lt_iff_nontrivial Cardinal.one_lt_iff_nontrivial -theorem power_le_max_power_one {a b c : Cardinal} (h : b ≤ c) : (a^b) ≤ max (a^c) 1 := by +theorem power_le_max_power_one {a b c : Cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1 := by by_cases ha : a = 0 · simp [ha, zero_power_le] · exact (power_le_power_left ha h).trans (le_max_left _ _) #align cardinal.power_le_max_power_one Cardinal.power_le_max_power_one -theorem power_le_power_right {a b c : Cardinal} : a ≤ b → (a^c) ≤ (b^c) := +theorem power_le_power_right {a b c : Cardinal} : a ≤ b → a ^ c ≤ b ^ c := inductionOn₃ a b c fun _ _ _ ⟨e⟩ => ⟨Embedding.arrowCongrRight e⟩ #align cardinal.power_le_power_right Cardinal.power_le_power_right -theorem power_pos {a : Cardinal} (b) (ha : 0 < a) : 0 < (a^b) := +theorem power_pos {a : Cardinal} (b : Cardinal) (ha : 0 < a) : 0 < a ^ b := (power_ne_zero _ ha.ne').bot_lt #align cardinal.power_pos Cardinal.power_pos @@ -1051,12 +1052,12 @@ theorem mk_pi {ι : Type u} (α : ι → Type v) : #(∀ i, α i) = prod fun i = @[simp] theorem prod_const (ι : Type u) (a : Cardinal.{v}) : - (prod fun _ : ι => a) = (lift.{u} a^lift.{v} #ι) := + (prod fun _ : ι => a) = lift.{u} a ^ lift.{v} #ι := inductionOn a fun _ => mk_congr <| Equiv.piCongr Equiv.ulift.symm fun _ => outMkEquiv.trans Equiv.ulift.symm #align cardinal.prod_const Cardinal.prod_const -theorem prod_const' (ι : Type u) (a : Cardinal.{u}) : (prod fun _ : ι => a) = (a^#ι) := +theorem prod_const' (ι : Type u) (a : Cardinal.{u}) : (prod fun _ : ι => a) = a ^ #ι := inductionOn a fun _ => (mk_pi _).symm #align cardinal.prod_const' Cardinal.prod_const' @@ -1346,7 +1347,7 @@ theorem card_le_of_finset {α} (s : Finset α) : (s.card : Cardinal) ≤ #α := -- Porting note: was `simp`. LHS is not normal form. -- @[simp, norm_cast] @[norm_cast] -theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = (m^n) := by +theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = m ^ n := by induction n <;> simp [pow_succ', power_add, *, Pow.pow] #align cardinal.nat_cast_pow Cardinal.natCast_pow @@ -1398,7 +1399,7 @@ theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : Finset α, s.card ≤ n) exact n.lt_succ_self #align cardinal.card_le_of Cardinal.card_le_of -theorem cantor' (a) {b : Cardinal} (hb : 1 < b) : a < (b^a) := by +theorem cantor' (a) {b : Cardinal} (hb : 1 < b) : a < b ^ a := by rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb exact (cantor a).trans_le (power_le_power_right hb) #align cardinal.cantor' Cardinal.cantor' @@ -1598,7 +1599,7 @@ theorem mul_lt_aleph0_iff_of_ne_zero {a b : Cardinal} (ha : a ≠ 0) (hb : b ≠ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀ := by simp [mul_lt_aleph0_iff, ha, hb] #align cardinal.mul_lt_aleph_0_iff_of_ne_zero Cardinal.mul_lt_aleph0_iff_of_ne_zero -theorem power_lt_aleph0 {a b : Cardinal} (ha : a < ℵ₀) (hb : b < ℵ₀) : (a^b) < ℵ₀ := +theorem power_lt_aleph0 {a b : Cardinal} (ha : a < ℵ₀) (hb : b < ℵ₀) : a ^ b < ℵ₀ := match a, b, lt_aleph0.1 ha, lt_aleph0.1 hb with | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by rw [← natCast_pow]; apply nat_lt_aleph0 #align cardinal.power_lt_aleph_0 Cardinal.power_lt_aleph0 @@ -2413,13 +2414,13 @@ def powerlt (a b : Cardinal.{u}) : Cardinal.{u} := @[inherit_doc] infixl:80 " ^< " => powerlt -theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : (a^c) ≤ a ^< b := by - refine le_ciSup (f := fun y : Iio b => a^y) ?_ ⟨c, h⟩ +theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : a ^ c ≤ a ^< b := by + refine le_ciSup (f := fun y : Iio b => a ^ y) ?_ ⟨c, h⟩ rw [← image_eq_range] exact bddAbove_image.{u, u} _ bddAbove_Iio #align cardinal.le_powerlt Cardinal.le_powerlt -theorem powerlt_le {a b c : Cardinal.{u}} : a ^< b ≤ c ↔ ∀ x < b, (a^x) ≤ c := by +theorem powerlt_le {a b c : Cardinal.{u}} : a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c := by rw [powerlt, ciSup_le_iff'] · simp · rw [← image_eq_range] @@ -2433,7 +2434,7 @@ theorem powerlt_le_powerlt_left {a b c : Cardinal} (h : b ≤ c) : a ^< b ≤ a theorem powerlt_mono_left (a) : Monotone fun c => a ^< c := fun _ _ => powerlt_le_powerlt_left #align cardinal.powerlt_mono_left Cardinal.powerlt_mono_left -theorem powerlt_succ {a b : Cardinal} (h : a ≠ 0) : a ^< succ b = (a^b) := +theorem powerlt_succ {a b : Cardinal} (h : a ≠ 0) : a ^< succ b = a ^ b := (powerlt_le.2 fun _ h' => power_le_power_left h <| le_of_lt_succ h').antisymm <| le_powerlt a (lt_succ b) #align cardinal.powerlt_succ Cardinal.powerlt_succ diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index 8f73315497585..e5ff4faed8fcb 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Ordinal.lean @@ -899,7 +899,7 @@ theorem add_one_le_add_one_iff_of_lt_aleph_0 {α β : Cardinal} : α + 1 ≤ β /-! ### Properties about power -/ --Porting note: Annoying workaround because `c ^ n` when `n` is a `ℕ` coerces `c` for some reason. -local infixr:0 "^'" => @HPow.hPow Cardinal Cardinal Cardinal.instPowCardinal +local infixr:80 " ^' " => @HPow.hPow Cardinal Cardinal Cardinal _ -- -- mathport name: cardinal.pow.nat local infixr:80 " ^ℕ " => @HPow.hPow Cardinal ℕ Cardinal instHPow diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index d43ce11b7e73a..c8e20f4ca2d0c 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -10,7 +10,7 @@ import Mathlib.SetTheory.Ordinal.Arithmetic /-! # Ordinal exponential In this file we define the power function and the logarithm function on ordinals. The two are -related by the lemma `Ordinal.opow_le_iff_le_log : (b^c) ≤ x ↔ c ≤ log b x` for nontrivial inputs +related by the lemma `Ordinal.opow_le_iff_le_log : b ^ c ≤ x ↔ c ≤ log b x` for nontrivial inputs `b`, `c`. -/ @@ -33,53 +33,53 @@ instance pow : Pow Ordinal Ordinal := -- local infixr:0 "^" => @Pow.pow Ordinal Ordinal Ordinal.instPowOrdinalOrdinal theorem opow_def (a b : Ordinal) : - (a^b) = if a = 0 then 1 - b else limitRecOn b 1 (fun _ IH => IH * a) fun b _ => bsup.{u, u} b := + a ^ b = if a = 0 then 1 - b else limitRecOn b 1 (fun _ IH => IH * a) fun b _ => bsup.{u, u} b := rfl #align ordinal.opow_def Ordinal.opow_def -- Porting note: `if_pos rfl` → `if_true` -theorem zero_opow' (a : Ordinal) : (0^a) = 1 - a := by simp only [opow_def, if_true] +theorem zero_opow' (a : Ordinal) : 0 ^ a = 1 - a := by simp only [opow_def, if_true] #align ordinal.zero_opow' Ordinal.zero_opow' @[simp] -theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0^a) = 0 := by +theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : 0 ^ a = 0 := by rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero] #align ordinal.zero_opow Ordinal.zero_opow @[simp] -theorem opow_zero (a : Ordinal) : (a^0) = 1 := by +theorem opow_zero (a : Ordinal) : a ^ 0 = 1 := by by_cases h : a = 0 · simp only [opow_def, if_pos h, sub_zero] · simp only [opow_def, if_neg h, limitRecOn_zero] #align ordinal.opow_zero Ordinal.opow_zero @[simp] -theorem opow_succ (a b : Ordinal) : (a^succ b) = (a^b) * a := +theorem opow_succ (a b : Ordinal) : a ^ succ b = a ^ b * a := if h : a = 0 then by subst a; simp only [zero_opow (succ_ne_zero _), mul_zero] else by simp only [opow_def, limitRecOn_succ, if_neg h] #align ordinal.opow_succ Ordinal.opow_succ theorem opow_limit {a b : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) : - (a^b) = bsup.{u, u} b fun c _ => a^c := by + a ^ b = bsup.{u, u} b fun c _ => a ^ c := by simp only [opow_def, if_neg a0]; rw [limitRecOn_limit _ _ _ _ h] #align ordinal.opow_limit Ordinal.opow_limit theorem opow_le_of_limit {a b c : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) : - (a^b) ≤ c ↔ ∀ b' < b, (a^b') ≤ c := by rw [opow_limit a0 h, bsup_le_iff] + a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c := by rw [opow_limit a0 h, bsup_le_iff] #align ordinal.opow_le_of_limit Ordinal.opow_le_of_limit theorem lt_opow_of_limit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) : - a < (b^c) ↔ ∃ c' < c, a < (b^c') := by + a < b ^ c ↔ ∃ c' < c, a < b ^ c' := by rw [← not_iff_not, not_exists]; simp only [not_lt, opow_le_of_limit b0 h, exists_prop, not_and] #align ordinal.lt_opow_of_limit Ordinal.lt_opow_of_limit @[simp] -theorem opow_one (a : Ordinal) : (a^1) = a := by +theorem opow_one (a : Ordinal) : a ^ 1 = a := by rw [← succ_zero, opow_succ]; simp only [opow_zero, one_mul] #align ordinal.opow_one Ordinal.opow_one @[simp] -theorem one_opow (a : Ordinal) : (1^a) = 1 := by +theorem one_opow (a : Ordinal) : 1 ^ a = 1 := by induction a using limitRecOn with | H₁ => simp only [opow_zero] | H₂ _ ih => @@ -90,8 +90,8 @@ theorem one_opow (a : Ordinal) : (1^a) = 1 := by exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩ #align ordinal.one_opow Ordinal.one_opow -theorem opow_pos {a : Ordinal} (b) (a0 : 0 < a) : 0 < (a^b) := by - have h0 : 0 < (a^0) := by simp only [opow_zero, zero_lt_one] +theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by + have h0 : 0 < a ^ 0 := by simp only [opow_zero, zero_lt_one] induction b using limitRecOn with | H₁ => exact h0 | H₂ b IH => @@ -101,33 +101,33 @@ theorem opow_pos {a : Ordinal} (b) (a0 : 0 < a) : 0 < (a^b) := by exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩ #align ordinal.opow_pos Ordinal.opow_pos -theorem opow_ne_zero {a : Ordinal} (b) (a0 : a ≠ 0) : (a^b) ≠ 0 := +theorem opow_ne_zero {a : Ordinal} (b : Ordinal) (a0 : a ≠ 0) : a ^ b ≠ 0 := Ordinal.pos_iff_ne_zero.1 <| opow_pos b <| Ordinal.pos_iff_ne_zero.2 a0 #align ordinal.opow_ne_zero Ordinal.opow_ne_zero -theorem opow_isNormal {a : Ordinal} (h : 1 < a) : IsNormal ((·^·) a) := +theorem opow_isNormal {a : Ordinal} (h : 1 < a) : IsNormal (a ^ ·) := have a0 : 0 < a := zero_lt_one.trans h ⟨fun b => by simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h, fun b l c => opow_le_of_limit (ne_of_gt a0) l⟩ #align ordinal.opow_is_normal Ordinal.opow_isNormal -theorem opow_lt_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : (a^b) < (a^c) ↔ b < c := +theorem opow_lt_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : a ^ b < a ^ c ↔ b < c := (opow_isNormal a1).lt_iff #align ordinal.opow_lt_opow_iff_right Ordinal.opow_lt_opow_iff_right -theorem opow_le_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : (a^b) ≤ (a^c) ↔ b ≤ c := +theorem opow_le_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : a ^ b ≤ a ^ c ↔ b ≤ c := (opow_isNormal a1).le_iff #align ordinal.opow_le_opow_iff_right Ordinal.opow_le_opow_iff_right -theorem opow_right_inj {a b c : Ordinal} (a1 : 1 < a) : (a^b) = (a^c) ↔ b = c := +theorem opow_right_inj {a b c : Ordinal} (a1 : 1 < a) : a ^ b = a ^ c ↔ b = c := (opow_isNormal a1).inj #align ordinal.opow_right_inj Ordinal.opow_right_inj -theorem opow_isLimit {a b : Ordinal} (a1 : 1 < a) : IsLimit b → IsLimit (a^b) := +theorem opow_isLimit {a b : Ordinal} (a1 : 1 < a) : IsLimit b → IsLimit (a ^ b) := (opow_isNormal a1).isLimit #align ordinal.opow_is_limit Ordinal.opow_isLimit -theorem opow_isLimit_left {a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLimit (a^b) := by +theorem opow_isLimit_left {a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLimit (a ^ b) := by rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l') · exact absurd e hb · rw [opow_succ] @@ -135,7 +135,7 @@ theorem opow_isLimit_left {a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLim · exact opow_isLimit l.one_lt l' #align ordinal.opow_is_limit_left Ordinal.opow_isLimit_left -theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : (a^b) ≤ (a^c) := by +theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c := by cases' lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ h₁ · exact (opow_le_opow_iff_right h₁).2 h₂ · subst a @@ -143,7 +143,7 @@ theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : ( simp only [one_opow, le_refl] #align ordinal.opow_le_opow_right Ordinal.opow_le_opow_right -theorem opow_le_opow_left {a b : Ordinal} (c) (ab : a ≤ b) : (a^c) ≤ (b^c) := by +theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c ≤ b ^ c := by by_cases a0 : a = 0 -- Porting note: `le_refl` is required. · subst a @@ -161,7 +161,7 @@ theorem opow_le_opow_left {a b : Ordinal} (c) (ab : a ≤ b) : (a^c) ≤ (b^c) : (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le) #align ordinal.opow_le_opow_left Ordinal.opow_le_opow_left -theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ (a^b) := by +theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := by nth_rw 1 [← opow_one a] cases' le_or_gt a 1 with a1 a1 · cases' lt_or_eq_of_le a1 with a0 a1 @@ -172,18 +172,18 @@ theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ (a^b) := b rwa [opow_le_opow_iff_right a1, one_le_iff_pos] #align ordinal.left_le_opow Ordinal.left_le_opow -theorem right_le_opow {a : Ordinal} (b) (a1 : 1 < a) : b ≤ (a^b) := +theorem right_le_opow {a : Ordinal} (b : Ordinal) (a1 : 1 < a) : b ≤ a ^ b := (opow_isNormal a1).self_le _ #align ordinal.right_le_opow Ordinal.right_le_opow -theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : (a^succ c) < (b^succ c) := by +theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c := by rw [opow_succ, opow_succ] exact (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab))) #align ordinal.opow_lt_opow_left_of_succ Ordinal.opow_lt_opow_left_of_succ -theorem opow_add (a b c : Ordinal) : a^(b + c) = (a^b) * (a^c) := by +theorem opow_add (a b c : Ordinal) : a ^ (b + c) = a ^ b * a ^ c := by rcases eq_or_ne a 0 with (rfl | a0) · rcases eq_or_ne c 0 with (rfl | c0) · simp @@ -207,14 +207,14 @@ theorem opow_add (a b c : Ordinal) : a^(b + c) = (a^b) * (a^c) := by l).symm #align ordinal.opow_add Ordinal.opow_add -theorem opow_one_add (a b : Ordinal) : a^(1 + b) = a * (a^b) := by rw [opow_add, opow_one] +theorem opow_one_add (a b : Ordinal) : a ^ (1 + b) = a * a ^ b := by rw [opow_add, opow_one] #align ordinal.opow_one_add Ordinal.opow_one_add -theorem opow_dvd_opow (a) {b c : Ordinal} (h : b ≤ c) : (a^b) ∣ (a^c) := - ⟨a^(c - b), by rw [← opow_add, Ordinal.add_sub_cancel_of_le h]⟩ +theorem opow_dvd_opow (a : Ordinal) {b c : Ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c := + ⟨a ^ (c - b), by rw [← opow_add, Ordinal.add_sub_cancel_of_le h]⟩ #align ordinal.opow_dvd_opow Ordinal.opow_dvd_opow -theorem opow_dvd_opow_iff {a b c : Ordinal} (a1 : 1 < a) : (a^b) ∣ (a^c) ↔ b ≤ c := +theorem opow_dvd_opow_iff {a b c : Ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c := ⟨fun h => le_of_not_lt fun hn => not_le_of_lt ((opow_lt_opow_iff_right a1).2 hn) <| @@ -222,7 +222,7 @@ theorem opow_dvd_opow_iff {a b c : Ordinal} (a1 : 1 < a) : (a^b) ∣ (a^c) ↔ b opow_dvd_opow _⟩ #align ordinal.opow_dvd_opow_iff Ordinal.opow_dvd_opow_iff -theorem opow_mul (a b c : Ordinal) : a^(b * c) = ((a^b)^c) := by +theorem opow_mul (a b c : Ordinal) : a ^ (b * c) = (a ^ b) ^ c := by by_cases b0 : b = 0; · simp only [b0, zero_mul, opow_zero, one_opow] by_cases a0 : a = 0 · subst a @@ -254,15 +254,15 @@ theorem opow_mul (a b c : Ordinal) : a^(b * c) = ((a^b)^c) := by `w < b ^ u`. -/ -- @[pp_nodot] -- Porting note: Unknown attribute. def log (b : Ordinal) (x : Ordinal) : Ordinal := - if _h : 1 < b then pred (sInf { o | x < (b^o) }) else 0 + if _h : 1 < b then pred (sInf { o | x < b ^ o }) else 0 #align ordinal.log Ordinal.log /-- The set in the definition of `log` is nonempty. -/ -theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o | x < (b^o) }.Nonempty := +theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o | x < b ^ o }.Nonempty := ⟨_, succ_le_iff.1 (right_le_opow _ h)⟩ #align ordinal.log_nonempty Ordinal.log_nonempty -theorem log_def {b : Ordinal} (h : 1 < b) (x : Ordinal) : log b x = pred (sInf { o | x < (b^o) }) := +theorem log_def {b : Ordinal} (h : 1 < b) (x : Ordinal) : log b x = pred (sInf { o | x < b ^ o }) := by simp only [log, dif_pos h] #align ordinal.log_def Ordinal.log_def @@ -296,9 +296,9 @@ theorem log_one_left : ∀ b, log 1 b = 0 := #align ordinal.log_one_left Ordinal.log_one_left theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : - succ (log b x) = sInf { o | x < (b^o) } := by - let t := sInf { o | x < (b^o) } - have : x < (b^t) := csInf_mem (log_nonempty hb) + succ (log b x) = sInf { o | x < b ^ o } := by + let t := sInf { o | x < b ^ o } + have : x < b ^ t := csInf_mem (log_nonempty hb) rcases zero_or_succ_or_limit t with (h | h | h) · refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim simpa only [h, opow_zero] using this @@ -308,26 +308,26 @@ theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : #align ordinal.succ_log_def Ordinal.succ_log_def theorem lt_opow_succ_log_self {b : Ordinal} (hb : 1 < b) (x : Ordinal) : - x < (b^succ (log b x)) := by + x < b ^ succ (log b x) := by rcases eq_or_ne x 0 with (rfl | hx) · apply opow_pos _ (zero_lt_one.trans hb) · rw [succ_log_def hb hx] exact csInf_mem (log_nonempty hb) #align ordinal.lt_opow_succ_log_self Ordinal.lt_opow_succ_log_self -theorem opow_log_le_self (b) {x : Ordinal} (hx : x ≠ 0) : (b^log b x) ≤ x := by +theorem opow_log_le_self (b : Ordinal) {x : Ordinal} (hx : x ≠ 0) : b ^ log b x ≤ x := by rcases eq_or_ne b 0 with (rfl | b0) · rw [zero_opow'] refine' (sub_le_self _ _).trans (one_le_iff_ne_zero.2 hx) rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl) · refine' le_of_not_lt fun h => (lt_succ (log b x)).not_le _ - have := @csInf_le' _ _ { o | x < (b^o) } _ h + have := @csInf_le' _ _ { o | x < b ^ o } _ h rwa [← succ_log_def hb hx] at this · rwa [one_opow, one_le_iff_ne_zero] #align ordinal.opow_log_le_self Ordinal.opow_log_le_self /-- `opow b` and `log b` (almost) form a Galois connection. -/ -theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : (b^c) ≤ x ↔ c ≤ log b x := +theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : b ^ c ≤ x ↔ c ≤ log b x := ⟨fun h => le_of_not_lt fun hn => (lt_opow_succ_log_self hb x).not_le <| @@ -335,7 +335,7 @@ theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : (b^c) fun h => ((opow_le_opow_iff_right hb).2 h).trans (opow_log_le_self b hx)⟩ #align ordinal.opow_le_iff_le_log Ordinal.opow_le_iff_le_log -theorem lt_opow_iff_log_lt {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < (b^c) ↔ log b x < c := +theorem lt_opow_iff_log_lt {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < b ^ c ↔ log b x < c := lt_iff_lt_of_le_iff_le (opow_le_iff_le_log hb hx) #align ordinal.lt_opow_iff_log_lt Ordinal.lt_opow_iff_log_lt @@ -354,7 +354,7 @@ theorem log_eq_zero {b o : Ordinal} (hbo : o < b) : log b o = 0 := by #align ordinal.log_eq_zero Ordinal.log_eq_zero @[mono] -theorem log_mono_right (b) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y := +theorem log_mono_right (b : Ordinal) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y := if hx : x = 0 then by simp only [hx, log_zero_right, Ordinal.zero_le] else if hb : 1 < b then @@ -375,15 +375,15 @@ theorem log_one_right (b : Ordinal) : log b 1 = 0 := if hb : 1 < b then log_eq_zero hb else log_of_not_one_lt_left hb 1 #align ordinal.log_one_right Ordinal.log_one_right -theorem mod_opow_log_lt_self (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b^log b o) < o := by +theorem mod_opow_log_lt_self (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b ^ log b o) < o := by rcases eq_or_ne b 0 with (rfl | hb) · simpa using Ordinal.pos_iff_ne_zero.2 ho · exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho) #align ordinal.mod_opow_log_lt_self Ordinal.mod_opow_log_lt_self theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : - log b (o % (b^log b o)) < log b o := by - cases' eq_or_ne (o % (b^log b o)) 0 with h h + log b (o % (b ^ log b o)) < log b o := by + cases' eq_or_ne (o % (b ^ log b o)) 0 with h h · rw [h, log_zero_right] apply log_pos hb ho hbo · rw [← succ_le_iff, succ_log_def hb h] @@ -393,24 +393,25 @@ theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) exact opow_pos _ (zero_lt_one.trans hb) #align ordinal.log_mod_opow_log_lt_log_self Ordinal.log_mod_opow_log_lt_log_self -theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u) (hv : v ≠ 0) (w) : 0 < (b^u) * v + w := +theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u : Ordinal) (hv : v ≠ 0) (w : Ordinal) : + 0 < b ^ u * v + w := (opow_pos u <| Ordinal.pos_iff_ne_zero.2 hb).trans_le <| (le_mul_left _ <| Ordinal.pos_iff_ne_zero.2 hv).trans <| le_add_right _ _ #align ordinal.opow_mul_add_pos Ordinal.opow_mul_add_pos -theorem opow_mul_add_lt_opow_mul_succ {b u w : Ordinal} (v : Ordinal) (hw : w < (b^u)) : - (b^u) * v + w < (b^u) * succ v := by rwa [mul_succ, add_lt_add_iff_left] +theorem opow_mul_add_lt_opow_mul_succ {b u w : Ordinal} (v : Ordinal) (hw : w < b ^ u) : + b ^ u * v + w < b ^ u * succ v := by rwa [mul_succ, add_lt_add_iff_left] #align ordinal.opow_mul_add_lt_opow_mul_succ Ordinal.opow_mul_add_lt_opow_mul_succ -theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < (b^u)) : - (b^u) * v + w < (b^succ u) := by +theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < b ^ u) : + b ^ u * v + w < b ^ succ u := by convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le (mul_le_mul_left' (succ_le_of_lt hvb) _) using 1 exact opow_succ b u #align ordinal.opow_mul_add_lt_opow_succ Ordinal.opow_mul_add_lt_opow_succ theorem log_opow_mul_add {b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hvb : v < b) - (hw : w < (b^u)) : log b ((b^u) * v + w) = u := by + (hw : w < b ^ u) : log b (b ^ u * v + w) = u := by have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne' by_contra' hne cases' lt_or_gt_of_ne hne with h h @@ -421,20 +422,20 @@ theorem log_opow_mul_add {b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hvb : exact (not_lt_of_le h) (opow_mul_add_lt_opow_succ hvb hw) #align ordinal.log_opow_mul_add Ordinal.log_opow_mul_add -theorem log_opow {b : Ordinal} (hb : 1 < b) (x : Ordinal) : log b (b^x) = x := by +theorem log_opow {b : Ordinal} (hb : 1 < b) (x : Ordinal) : log b (b ^ x) = x := by convert log_opow_mul_add hb zero_ne_one.symm hb (opow_pos x (zero_lt_one.trans hb)) using 1 rw [add_zero, mul_one] #align ordinal.log_opow Ordinal.log_opow -theorem div_opow_log_pos (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : 0 < o / (b^log b o) := by +theorem div_opow_log_pos (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : 0 < o / (b ^ log b o) := by rcases eq_zero_or_pos b with (rfl | hb) · simpa using Ordinal.pos_iff_ne_zero.2 ho · rw [div_pos (opow_ne_zero _ hb.ne')] exact opow_log_le_self b ho #align ordinal.div_opow_log_pos Ordinal.div_opow_log_pos -theorem div_opow_log_lt {b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b^log b o) < b := by +theorem div_opow_log_lt {b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b ^ log b o) < b := by rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ] exact lt_opow_succ_log_self hb o #align ordinal.div_opow_log_lt Ordinal.div_opow_log_lt @@ -451,18 +452,18 @@ theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y /-! ### Interaction with `Nat.cast` -/ @[simp, norm_cast] -theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ((m ^ n : ℕ) : Ordinal) = (m^n) +theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ((m ^ n : ℕ) : Ordinal) = m ^ n | 0 => by simp | n + 1 => by rw [pow_succ', nat_cast_mul, nat_cast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ] #align ordinal.nat_cast_opow Ordinal.nat_cast_opow -theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o^n) = (o^ω) := by +theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o ^ n) = o ^ ω := by rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with (ho₁ | rfl) · exact (opow_isNormal ho₁).apply_omega · rw [one_opow] refine' le_antisymm (sup_le fun n => by rw [one_opow]) _ - convert le_sup (fun n : ℕ => 1^n) 0 + convert le_sup (fun n : ℕ => 1 ^ n) 0 rw [Nat.cast_zero, opow_zero] #align ordinal.sup_opow_nat Ordinal.sup_opow_nat