Port/SetTheory.Ordinal.NaturalOps (#2353)

Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>

Mathlib.lean

@@ -975,6 +975,7 @@ import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Lists
 import Mathlib.SetTheory.Ordinal.Arithmetic
 import Mathlib.SetTheory.Ordinal.Basic
+import Mathlib.SetTheory.Ordinal.NaturalOps
 import Mathlib.SetTheory.Ordinal.Topology
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Alias

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -537,7 +537,7 @@ theorem sub_nonempty {a b : Ordinal} : { o | a ≤ b + o }.Nonempty :=
 #align ordinal.sub_nonempty Ordinal.sub_nonempty
 
 /-- `a - b` is the unique ordinal satisfying `b + (a - b) = a` when `b ≤ a`. -/
-instance : Sub Ordinal :=
+instance hasSub : Sub Ordinal :=
   ⟨fun a b => infₛ { o | a ≤ b + o }⟩
 
 theorem le_add_sub (a b : Ordinal) : a ≤ b + (a - b) :=
@@ -582,7 +582,7 @@ theorem sub_lt_of_le {a b c : Ordinal} (h : b ≤ a) : a - b < c ↔ a < b + c :
   lt_iff_lt_of_le_iff_le (le_sub_of_le h)
 #align ordinal.sub_lt_of_le Ordinal.sub_lt_of_le
 
-instance : ExistsAddOfLE Ordinal :=
+instance existsAddOfLE : ExistsAddOfLE Ordinal :=
   ⟨fun h => ⟨_, (Ordinal.add_sub_cancel_of_le h).symm⟩⟩
 
 @[simp]
@@ -685,13 +685,13 @@ private theorem mul_eq_zero' {a b : Ordinal} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
       rw [or_comm]
       exact isEmpty_prod
 
-instance : MonoidWithZero Ordinal :=
+instance monoidWithZero : MonoidWithZero Ordinal :=
   { Ordinal.monoid with
     zero := 0
     mul_zero := fun _a => mul_eq_zero'.2 <| Or.inr rfl
     zero_mul := fun _a => mul_eq_zero'.2 <| Or.inl rfl }
 
-instance : NoZeroDivisors Ordinal :=
+instance noZeroDivisors : NoZeroDivisors Ordinal :=
   ⟨fun {_ _} => mul_eq_zero'.1⟩
 
 @[simp]
@@ -708,7 +708,7 @@ theorem card_mul (a b) : card (a * b) = card a * card b :=
   Quotient.inductionOn₂ a b fun ⟨α, _r, _⟩ ⟨β, _s, _⟩ => mul_comm (#β) (#α)
 #align ordinal.card_mul Ordinal.card_mul
 
-instance : LeftDistribClass Ordinal.{u} :=
+instance leftDistribClass : LeftDistribClass Ordinal.{u} :=
   ⟨fun a b c =>
     Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ =>
       Quotient.sound
@@ -875,7 +875,7 @@ theorem div_nonempty {a b : Ordinal} (h : b ≠ 0) : { o | a < b * succ o }.None
 #align ordinal.div_nonempty Ordinal.div_nonempty
 
 /-- `a / b` is the unique ordinal `o` satisfying `a = b * o + o'` with `o' < b`. -/
-instance : Div Ordinal :=
+instance hasDiv : Div Ordinal :=
   ⟨fun a b => if _h : b = 0 then 0 else infₛ { o | a < b * succ o }⟩
 
 @[simp]
@@ -1019,12 +1019,12 @@ theorem dvd_antisymm {a b : Ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b :
     else (le_of_dvd b0 h₁).antisymm (le_of_dvd a0 h₂)
 #align ordinal.dvd_antisymm Ordinal.dvd_antisymm
 
-instance : IsAntisymm Ordinal (· ∣ ·) :=
+instance isAntisymm : IsAntisymm Ordinal (· ∣ ·) :=
   ⟨@dvd_antisymm⟩
 
 /-- `a % b` is the unique ordinal `o'` satisfying
   `a = b * o + o'` with `o' < b`. -/
-instance : Mod Ordinal :=
+instance hasMod : Mod Ordinal :=
   ⟨fun a b => a - b * (a / b)⟩
 
 theorem mod_def (a b : Ordinal) : a % b = a - b * (a / b) :=
@@ -2268,7 +2268,7 @@ end
 
 
 /-- The ordinal exponential, defined by transfinite recursion. -/
-instance : Pow Ordinal Ordinal :=
+instance  hasPow: Pow Ordinal Ordinal :=
   ⟨fun a b => if a = 0 then 1 - b else limitRecOn b 1 (fun _ IH => IH * a) fun b _ => bsup.{u, u} b⟩
 
 -- Porting note: Ambiguous notations.

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -128,7 +128,7 @@ attribute [instance] WellOrder.wo
 
 namespace WellOrder
 
-instance : Inhabited WellOrder :=
+instance inhabited : Inhabited WellOrder :=
   ⟨⟨PEmpty, _, inferInstanceAs (IsWellOrder PEmpty EmptyRelation)⟩⟩
 
 @[simp]
@@ -174,13 +174,13 @@ def type (r : α → α → Prop) [wo : IsWellOrder α r] : Ordinal :=
   ⟦⟨α, r, wo⟩⟧
 #align ordinal.type Ordinal.type
 
-instance : Zero Ordinal :=
+instance hasZero : Zero Ordinal :=
   ⟨type <| @EmptyRelation PEmpty⟩
 
-instance : Inhabited Ordinal :=
+instance inhabited : Inhabited Ordinal :=
   ⟨0⟩
 
-instance : One Ordinal :=
+instance hasOne : One Ordinal :=
   ⟨type <| @EmptyRelation PUnit⟩
 
 /-- The order type of an element inside a well order. For the embedding as a principal segment, see
@@ -293,7 +293,7 @@ protected theorem one_ne_zero : (1 : Ordinal) ≠ 0 :=
   type_ne_zero_of_nonempty _
 #align ordinal.one_ne_zero Ordinal.one_ne_zero
 
-instance : Nontrivial Ordinal.{u} :=
+instance nontrivial : Nontrivial Ordinal.{u} :=
   ⟨⟨1, 0, Ordinal.one_ne_zero⟩⟩
 
 --@[simp] -- Porting note: not in simp nf, added aux lemma below
@@ -316,7 +316,7 @@ theorem inductionOn {C : Ordinal → Prop} (o : Ordinal)
 /-! ### The order on ordinals -/
 
 
-instance : PartialOrder Ordinal
+instance partialOrder : PartialOrder Ordinal
     where
   le a b :=
     Quotient.liftOn₂ a b (fun ⟨_, r, _⟩ ⟨_, s, _⟩ => Nonempty (r ≼i s))
@@ -387,7 +387,7 @@ protected theorem zero_le (o : Ordinal) : 0 ≤ o :=
   inductionOn o fun _ r _ => (InitialSeg.ofIsEmpty _ r).ordinal_type_le
 #align ordinal.zero_le Ordinal.zero_le
 
-instance : OrderBot Ordinal where
+instance orderBot : OrderBot Ordinal where
   bot := 0
   bot_le := Ordinal.zero_le
 
@@ -413,7 +413,7 @@ theorem eq_zero_or_pos : ∀ a : Ordinal, a = 0 ∨ 0 < a :=
   eq_bot_or_bot_lt
 #align ordinal.eq_zero_or_pos Ordinal.eq_zero_or_pos
 
-instance : ZeroLEOneClass Ordinal :=
+instance zeroLEOneClass : ZeroLEOneClass Ordinal :=
   ⟨Ordinal.zero_le _⟩
 
 instance NeZero.one : NeZero (1 : Ordinal) :=
@@ -574,7 +574,7 @@ theorem lt_wf : @WellFounded Ordinal (· < ·) :=
           exact IH _ ((typein_lt_typein r).1 h)⟩⟩
 #align ordinal.lt_wf Ordinal.lt_wf
 
-instance : WellFoundedRelation Ordinal :=
+instance wellFoundedRelation : WellFoundedRelation Ordinal :=
   ⟨(· < ·), lt_wf⟩
 
 /-- Reformulation of well founded induction on ordinals as a lemma that works with the
@@ -885,12 +885,12 @@ the addition, together with properties of the other operations, are proved in
 
 /-- `o₁ + o₂` is the order on the disjoint union of `o₁` and `o₂` obtained by declaring that
   every element of `o₁` is smaller than every element of `o₂`. -/
-instance : Add Ordinal.{u} :=
+instance hasAdd : Add Ordinal.{u} :=
   ⟨fun o₁ o₂ =>
     Quotient.liftOn₂ o₁ o₂ (fun ⟨_, r, _⟩ ⟨_, s, _⟩ => type (Sum.Lex r s))
       fun _ _ _ _ ⟨f⟩ ⟨g⟩ => Quot.sound ⟨RelIso.sumLexCongr f g⟩⟩
 
-instance : AddMonoidWithOne Ordinal.{u}
+instance addMonoidWithOne : AddMonoidWithOne Ordinal.{u}
     where
   add := (· + ·)
   zero := 0
@@ -977,7 +977,7 @@ theorem le_add_left (a b : Ordinal) : a ≤ b + a := by
   simpa only [zero_add] using add_le_add_right (Ordinal.zero_le b) a
 #align ordinal.le_add_left Ordinal.le_add_left
 
-instance : LinearOrder Ordinal :=
+instance linearOrder : LinearOrder Ordinal :=
   {inferInstanceAs (PartialOrder Ordinal) with
     le_total := fun a b =>
       match lt_or_eq_of_le (le_add_left b a), lt_or_eq_of_le (le_add_right a b) with
@@ -999,10 +999,10 @@ instance : LinearOrder Ordinal :=
                   exact Or.inr (Or.inl h)]
     decidable_le := Classical.decRel _ }
 
-instance : WellFoundedLT Ordinal :=
+instance wellFoundedLT : WellFoundedLT Ordinal :=
   ⟨lt_wf⟩
 
-instance : IsWellOrder Ordinal (· < ·) where
+instance isWellOrder : IsWellOrder Ordinal (· < ·) where
 
 instance : ConditionallyCompleteLinearOrderBot Ordinal :=
   IsWellOrder.conditionallyCompleteLinearOrderBot _
@@ -1055,10 +1055,10 @@ private theorem succ_le_iff' {a b : Ordinal} : a + 1 ≤ b ↔ a < b :=
             cases' (hf b).1 h with w h
             exact ⟨Sum.inl w, h⟩⟩
 
-instance : NoMaxOrder Ordinal :=
+instance noMaxOrder : NoMaxOrder Ordinal :=
   ⟨fun _ => ⟨_, succ_le_iff'.1 le_rfl⟩⟩
 
-instance : SuccOrder Ordinal.{u} :=
+instance succOrder : SuccOrder Ordinal.{u} :=
   SuccOrder.ofSuccLeIff (fun o => o + 1) succ_le_iff'
 
 @[simp]