chore(SetTheory/Ordinal/Basic): Ordinal.NeZero.One → `Ordinal.instN…

…eZeroOne` (#19064)

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]

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

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