From b2244f6fc5832d2e74f3990726e448489cb773bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Tue, 19 Nov 2024 04:07:31 +0000 Subject: [PATCH] =?UTF-8?q?chore(SetTheory/Ordinal/Basic):=20`Ordinal.NeZe?= =?UTF-8?q?ro.One`=20=E2=86=92=20`Ordinal.instNeZeroOne`=20(#19064)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/SetTheory/Nimber/Basic.lean | 14 ++++++------ Mathlib/SetTheory/Ordinal/Basic.lean | 14 ++++++------ Mathlib/SetTheory/Ordinal/NaturalOps.lean | 26 ++++++++++++----------- 3 files changed, 28 insertions(+), 26 deletions(-) diff --git a/Mathlib/SetTheory/Nimber/Basic.lean b/Mathlib/SetTheory/Nimber/Basic.lean index 28ff884f9c685..9f33020c6c6b5 100644 --- a/Mathlib/SetTheory/Nimber/Basic.lean +++ b/Mathlib/SetTheory/Nimber/Basic.lean @@ -44,16 +44,16 @@ noncomputable section /-! ### Basic casts between `Ordinal` and `Nimber` -/ -/-- A type synonym for ordinals with natural addition and multiplication. -/ +/-- A type synonym for ordinals with nimber addition and multiplication. -/ def Nimber : Type _ := Ordinal deriving Zero, Inhabited, One, Nontrivial, WellFoundedRelation -instance Nimber.linearOrder : LinearOrder Nimber := {Ordinal.linearOrder with} -instance Nimber.succOrder : SuccOrder Nimber := {Ordinal.instSuccOrder with} -instance Nimber.orderBot : OrderBot Nimber := {Ordinal.orderBot with} -instance Nimber.noMaxOrder : NoMaxOrder Nimber := {Ordinal.noMaxOrder with} -instance Nimber.zeroLEOneClass : ZeroLEOneClass Nimber := {Ordinal.zeroLEOneClass with} -instance Nimber.instNeZeroOne : NeZero (1 : Nimber) := Ordinal.NeZero.one +instance Nimber.instLinearOrder : LinearOrder Nimber := Ordinal.instLinearOrder +instance Nimber.instSuccOrder : SuccOrder Nimber := Ordinal.instSuccOrder +instance Nimber.instOrderBot : OrderBot Nimber := Ordinal.instOrderBot +instance Nimber.instNoMaxOrder : NoMaxOrder Nimber := Ordinal.instNoMaxOrder +instance Nimber.instZeroLEOneClass : ZeroLEOneClass Nimber := Ordinal.instZeroLEOneClass +instance Nimber.instNeZeroOne : NeZero (1 : Nimber) := Ordinal.instNeZeroOne /-- The identity function between `Ordinal` and `Nimber`. -/ @[match_pattern] diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 65e5733c47823..5a31bfe919ee9 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -287,7 +287,7 @@ instance partialOrder : PartialOrder Ordinal where Quotient.inductionOn₂ a b fun _ _ ⟨h₁⟩ ⟨h₂⟩ => Quot.sound ⟨InitialSeg.antisymm h₁ h₂⟩ -instance linearOrder : LinearOrder Ordinal := +instance : LinearOrder Ordinal := {inferInstanceAs (PartialOrder Ordinal) with le_total := fun a b => Quotient.inductionOn₂ a b fun ⟨_, r, _⟩ ⟨_, s, _⟩ => (InitialSeg.total r s).recOn (fun f => Or.inl ⟨f⟩) fun f => Or.inr ⟨f⟩ @@ -309,7 +309,7 @@ theorem _root_.PrincipalSeg.ordinal_type_lt {α β} {r : α → α → Prop} {s protected theorem zero_le (o : Ordinal) : 0 ≤ o := inductionOn o fun _ r _ => (InitialSeg.ofIsEmpty _ r).ordinal_type_le -instance orderBot : OrderBot Ordinal where +instance : OrderBot Ordinal where bot := 0 bot_le := Ordinal.zero_le @@ -330,10 +330,10 @@ protected theorem not_lt_zero (o : Ordinal) : ¬o < 0 := theorem eq_zero_or_pos : ∀ a : Ordinal, a = 0 ∨ 0 < a := eq_bot_or_bot_lt -instance zeroLEOneClass : ZeroLEOneClass Ordinal := +instance : ZeroLEOneClass Ordinal := ⟨Ordinal.zero_le _⟩ -instance NeZero.one : NeZero (1 : Ordinal) := +instance instNeZeroOne : NeZero (1 : Ordinal) := ⟨Ordinal.one_ne_zero⟩ theorem type_le_iff {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] @@ -875,13 +875,13 @@ private theorem succ_le_iff' {a b : Ordinal} : a + 1 ≤ b ↔ a < b := by · apply (RelEmbedding.ofMonotone (Sum.recOn · f fun _ ↦ f.top) ?_).ordinal_type_le simpa [f.map_rel_iff] using f.lt_top -instance noMaxOrder : NoMaxOrder Ordinal := +instance : NoMaxOrder Ordinal := ⟨fun _ => ⟨_, succ_le_iff'.1 le_rfl⟩⟩ -instance instSuccOrder : SuccOrder Ordinal.{u} := +instance : SuccOrder Ordinal.{u} := SuccOrder.ofSuccLeIff (fun o => o + 1) succ_le_iff' -instance instSuccAddOrder : SuccAddOrder Ordinal := ⟨fun _ => rfl⟩ +instance : SuccAddOrder Ordinal := ⟨fun _ => rfl⟩ @[simp] theorem add_one_eq_succ (o : Ordinal) : o + 1 = succ o := diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean index c7ac9850362c8..7463af175343e 100644 --- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean +++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean @@ -53,10 +53,12 @@ def NatOrdinal : Type _ := -- Porting note: used to derive LinearOrder & SuccOrder but need to manually define Ordinal deriving Zero, Inhabited, One, WellFoundedRelation -instance NatOrdinal.linearOrder : LinearOrder NatOrdinal := {Ordinal.linearOrder with} -instance NatOrdinal.instSuccOrder : SuccOrder NatOrdinal := {Ordinal.instSuccOrder with} -instance NatOrdinal.orderBot : OrderBot NatOrdinal := {Ordinal.orderBot with} -instance NatOrdinal.noMaxOrder : NoMaxOrder NatOrdinal := {Ordinal.noMaxOrder with} +instance NatOrdinal.instLinearOrder : LinearOrder NatOrdinal := Ordinal.instLinearOrder +instance NatOrdinal.instSuccOrder : SuccOrder NatOrdinal := Ordinal.instSuccOrder +instance NatOrdinal.instOrderBot : OrderBot NatOrdinal := Ordinal.instOrderBot +instance NatOrdinal.instNoMaxOrder : NoMaxOrder NatOrdinal := Ordinal.instNoMaxOrder +instance NatOrdinal.instZeroLEOneClass : ZeroLEOneClass NatOrdinal := Ordinal.instZeroLEOneClass +instance NatOrdinal.instNeZeroOne : NeZero (1 : NatOrdinal) := Ordinal.instNeZeroOne /-- The identity function between `Ordinal` and `NatOrdinal`. -/ @[match_pattern] @@ -316,19 +318,19 @@ open Ordinal NaturalOps instance : Add NatOrdinal := ⟨nadd⟩ instance : SuccAddOrder NatOrdinal := ⟨fun x => (nadd_one x).symm⟩ -instance addLeftStrictMono : AddLeftStrictMono NatOrdinal.{u} := +instance : AddLeftStrictMono NatOrdinal.{u} := ⟨fun a _ _ h => nadd_lt_nadd_left h a⟩ -instance addLeftMono : AddLeftMono NatOrdinal.{u} := +instance : AddLeftMono NatOrdinal.{u} := ⟨fun a _ _ h => nadd_le_nadd_left h a⟩ -instance addLeftReflectLE : AddLeftReflectLE NatOrdinal.{u} := +instance : AddLeftReflectLE NatOrdinal.{u} := ⟨fun a b c h => by by_contra! h' exact h.not_lt (add_lt_add_left h' a)⟩ -instance orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid NatOrdinal := - { NatOrdinal.linearOrder with +instance : OrderedCancelAddCommMonoid NatOrdinal := + { NatOrdinal.instLinearOrder with add := (· + ·) add_assoc := nadd_assoc add_le_add_left := fun _ _ => add_le_add_left @@ -339,7 +341,7 @@ instance orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid NatOrdinal := add_comm := nadd_comm nsmul := nsmulRec } -instance addMonoidWithOne : AddMonoidWithOne NatOrdinal := +instance : AddMonoidWithOne NatOrdinal := AddMonoidWithOne.unary @[deprecated Order.succ_eq_add_one (since := "2024-09-04")] @@ -674,8 +676,8 @@ instance : Mul NatOrdinal := -- Porting note: had to add universe annotations to ensure that the -- two sources lived in the same universe. instance : OrderedCommSemiring NatOrdinal.{u} := - { NatOrdinal.orderedCancelAddCommMonoid.{u}, - NatOrdinal.linearOrder.{u} with + { NatOrdinal.instOrderedCancelAddCommMonoid.{u}, + NatOrdinal.instLinearOrder.{u} with mul := (· * ·) left_distrib := nmul_nadd right_distrib := nadd_nmul