feat: nimber multiplication is bounded by natural multiplication

CombinatorialGames/NatOrdinal/Basic.lean

@@ -168,6 +168,22 @@ instance : AddMonoidWithOne NatOrdinal where
 @[simp] theorem of_natCast (n : ℕ) : of n = n := rfl
 @[simp] theorem val_natCast (n : ℕ) : val n = n := rfl
 
+@[simp, norm_cast] theorem natCast_le_of_iff {a : ℕ} {b : Ordinal} : a ≤ of b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem natCast_lt_of_iff {a : ℕ} {b : Ordinal} : a < of b ↔ a < b := .rfl
+@[simp, norm_cast] theorem natCast_eq_of_iff {a : ℕ} {b : Ordinal} : a = of b ↔ a = b := .rfl
+@[simp, norm_cast] theorem natCast_le_val_iff {a : ℕ} {b : NatOrdinal} : a ≤ val b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem natCast_lt_val_iff {a : ℕ} {b : NatOrdinal} : a < val b ↔ a < b := .rfl
+@[simp, norm_cast] theorem natCast_eq_val_iff {a : ℕ} {b : NatOrdinal} : a = val b ↔ a = b := .rfl
+
+@[simp, norm_cast] theorem of_le_natCast_iff {a : Ordinal} {b : ℕ} : of a ≤ b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem of_lt_natCast_iff {a : Ordinal} {b : ℕ} : of a < b ↔ a < b := .rfl
+@[simp, norm_cast] theorem of_eq_natCast_iff {a : Ordinal} {b : ℕ} : of a = b ↔ a = b := .rfl
+@[simp, norm_cast] theorem val_le_natCast_iff {a : NatOrdinal} {b : ℕ} : val a ≤ b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem val_lt_natCast_iff {a : NatOrdinal} {b : ℕ} : val a < b ↔ a < b := .rfl
+@[simp, norm_cast] theorem val_eq_natCast_iff {a : NatOrdinal} {b : ℕ} : val a = b ↔ a = b := .rfl
+
+@[simp] protected theorem succ_one : succ (1 : NatOrdinal) = 2 := Ordinal.succ_one
+
 @[simp]
 theorem natCast_image_Iio (n : ℕ) : Nat.cast '' Iio n = Iio (n : NatOrdinal) :=
   Ordinal.natCast_image_Iio n
@@ -316,6 +332,9 @@ instance : MulLeftMono NatOrdinal where
 instance : MulRightMono NatOrdinal where
   elim a b c h := by convert mul_le_mul_right h a using 1 <;> exact mul_comm ..
 
+protected theorem mul_lt_mul {a b c d : NatOrdinal} (h₁ : a < c) (h₂ : b < d) : a * b < c * d :=
+  mul_lt_mul'' h₁ h₂ (zero_le _) (zero_le _)
+
 private theorem mul_add (a b c : NatOrdinal) : a * (b + c) = a * b + a * c := by
   refine le_antisymm (mul_le_iff.2 fun a' ha d hd => ?_)
     (add_le_iff.2 ⟨fun d hd => ?_, fun d hd => ?_⟩)

CombinatorialGames/NatOrdinal/Pow.lean

@@ -8,6 +8,8 @@ module
 public import CombinatorialGames.NatOrdinal.Basic
 public import Mathlib.SetTheory.Ordinal.Exponential
 
+import Mathlib.SetTheory.Ordinal.Principal
+
 /-!
 # Natural operations on `ω ^ x`
 
@@ -32,11 +34,6 @@ notation `ω^ x` for `of (ω ^ x.val)`. This typeclass will get reused for `IGam
 
 open Ordinal
 
-theorem Ordinal.lt_mul_add_one {x y z : Ordinal} : x < y * (z + 1) ↔ ∃ w < y, x ≤ y * z + w := by
-  obtain rfl | hy := eq_or_ne y 0
-  · simp
-  · rw [mul_add_one, lt_add_iff hy]
-
 /-- A typeclass for the the `ω^` notation. -/
 class Wpow (α : Type*) where
   /-- The `ω`-map, i.e. base `ω` exponentiation. -/
@@ -58,6 +55,7 @@ theorem wpow_def (x : NatOrdinal) : ω^ x = of (ω ^ x.val) := rfl
 @[simp] theorem wpow_zero : ω^ (0 : NatOrdinal) = 1 := by simp [wpow_def]
 @[simp] theorem wpow_pos (x : NatOrdinal) : 0 < ω^ x := opow_pos _ omega0_pos
 @[simp] theorem wpow_ne_zero (x : NatOrdinal) : ω^ x ≠ 0 := (wpow_pos x).ne'
+@[simp] theorem wpow_one : ω^ (1 : NatOrdinal) = of ω := by simp [wpow_def]
 
 theorem isNormal_wpow : Order.IsNormal (ω^ · : NatOrdinal → NatOrdinal) :=
   Ordinal.isNormal_opow one_lt_omega0
@@ -99,7 +97,7 @@ private theorem wpow_mul_natCast_add_of_lt_aux {x y : NatOrdinal} (hy : y < ω^
           obtain (⟨a, ha, hz⟩ | h) := lt_add_iff.1 hz
           · have hxn := (wpow_mul_natCast_add_of_lt_aux (wpow_pos x) (n + 1)).2
             simp_rw [val_zero, add_zero] at hxn
-            rw [hxn, ← val_lt_iff, Nat.cast_add_one, lt_mul_add_one] at ha
+            rw [hxn, ← val_lt_iff, Nat.cast_add_one, lt_mul_add_one_iff] at ha
             obtain ⟨b, (hb : of b < ω^ x), hbw⟩ := ha
             rw [val_le_iff, ← val_of b, ← (wpow_mul_natCast_add_of_lt_aux hb n).2] at hbw
             refine ⟨_, hb, hz.trans <| (add_le_add_left hbw _).trans ?_⟩
@@ -119,17 +117,22 @@ termination_by (x, n, y)
 theorem add_lt_wpow (hx : x < ω^ z) (hy : y < ω^ z) : x + y < ω^ z :=
   (wpow_mul_natCast_add_of_lt_aux hy 0).1 x hx
 
-/-- See `wpow_mul_natCast_add_of_lt` for a stronger version. -/
-theorem wpow_mul_natCast_add_of_lt' (hy : y < ω^ x) (n : ℕ) :
-    ω^ x * n + y = of (ω ^ x.val * n + y.val) :=
-  (wpow_mul_natCast_add_of_lt_aux hy n).2
+/-- See `of_omega0_opow_mul_natCast_add` for a stronger version. -/
+theorem of_omega0_opow_mul_natCast_add' {x y : Ordinal} (hy : y < ω ^ x) (n : ℕ) :
+    of (ω ^ x * n + y) = ω^ of x * n + of y :=
+  (wpow_mul_natCast_add_of_lt_aux hy n).2.symm
+
+/-- See `of_omega0_opow_add` for a stronger version. -/
+theorem of_omega0_opow_add' {x y : Ordinal} (hy : y < ω ^ x) :
+    of (ω ^ x + y) = ω^ of x + of y := by
+  simpa using of_omega0_opow_mul_natCast_add' hy 1
 
-/-- See `wpow_add_of_lt` for a stronger version. -/
-theorem wpow_add_of_lt' (hy : y < ω^ x) : ω^ x + y = of (ω ^ x.val + y.val) := by
-  simpa using wpow_mul_natCast_add_of_lt' hy 1
+@[simp]
+theorem of_omega0_opow_mul_natCast (x : Ordinal) (n : ℕ) : of (ω ^ x * n) = ω^ of x * n := by
+  simpa using of_omega0_opow_mul_natCast_add' (opow_pos _ omega0_pos) n
 
 theorem wpow_mul_natCast (x : NatOrdinal) (n : ℕ) : ω^ x * n = of (ω ^ x.val * n) := by
-  simpa using wpow_mul_natCast_add_of_lt' (wpow_pos _) n
+  simp
 
 theorem wpow_mul_natCast_lt (h : x < y) (n : ℕ) : ω^ x * n < ω^ y := by
   rw [wpow_mul_natCast]
@@ -154,25 +157,70 @@ theorem wpow_add_one_le_iff : ω^ (x + 1) ≤ y ↔ ∀ n : ℕ, ω^ x * n ≤ y
   rw [← not_lt, lt_wpow_add_one_iff]
   simp
 
-theorem wpow_mul_natCast_add_of_lt (hy : y < ω^ (x + 1)) (n : ℕ) :
-    ω^ x * n + y = of (ω ^ x.val * n + y.val) := by
-  obtain ⟨z, hz, m, rfl⟩ : ∃ z < ω^ x, ∃ m : ℕ, y = ω^ x * m + z := by
-    rw [wpow_def, ← val_lt_iff, val_add_one, opow_add, opow_one, Ordinal.lt_mul_iff_div_lt] at hy
-    · obtain ⟨m, hm⟩ := Ordinal.lt_omega0.1 hy
-      have hx : of (y.val % ω ^ x.val) < ω^ x := mod_lt _ (wpow_ne_zero _)
-      use of (y.val % ω ^ x.val), hx, m
-      rw [wpow_mul_natCast_add_of_lt' hx, ← hm]
-      exact (div_add_mod ..).symm
-    · exact wpow_ne_zero _
-  simp_rw [← add_assoc, wpow_mul_natCast_add_of_lt' hz, val_of, ← add_assoc, ← mul_add,
-    ← Nat.cast_add, wpow_mul_natCast_add_of_lt' hz]
-
-theorem wpow_add_of_lt (hy : y < ω^ (x + 1)) : ω^ x + y = of (ω ^ x.val + y.val) := by
-  simpa using wpow_mul_natCast_add_of_lt hy 1
-
-theorem wpow_add_wpow (h : x ≤ y) : ω^ y + ω^ x = of (ω ^ y.val + ω ^ x.val) := by
-  rw [wpow_add_of_lt, val_wpow]
-  simpa using Order.lt_succ_of_le h
+theorem of_omega0_opow_mul_natCast_add {x y : Ordinal} (hy : y < ω ^ (x + 1)) (n : ℕ) :
+    of (ω ^ x * n + y) = ω^ of x * n + of y := by
+  simp_rw [opow_add_one, Ordinal.lt_mul_iff, Ordinal.lt_omega0] at hy
+  obtain ⟨_, ⟨m, rfl⟩, ⟨r, hr, rfl⟩⟩ := hy
+  rw [of_omega0_opow_mul_natCast_add' hr]
+  simp_rw [← add_assoc, ← mul_add, ← Nat.cast_add, of_omega0_opow_mul_natCast_add' hr]
+
+theorem of_omega0_opow_add {x y : Ordinal} (hy : y < ω ^ (x + 1)) :
+    of (ω ^ x + y) = ω^ of x + of y := by
+  simpa using of_omega0_opow_mul_natCast_add hy 1
+
+theorem of_omega0_opow_add_omega0_opow {x y : Ordinal} (h : x ≤ y) :
+    of (ω ^ y + ω ^ x) = ω^ of y + ω^ of x := by
+  rw [of_omega0_opow_add, of_omega0_opow]
+  rwa [opow_lt_opow_iff_right one_lt_omega0, Order.lt_add_one_iff]
+
+theorem of_natCast_opow_mul_natCast_add_of_lt {x y : Ordinal} {m : ℕ} (hy : y < m ^ x * ω) (n : ℕ) :
+    of (m ^ x * n + y) = of (m ^ x) * n + of y := by
+  obtain hm | hm := le_or_gt m 1
+  · obtain rfl | rfl := Nat.le_one_iff_eq_zero_or_eq_one.1 hm
+    · obtain rfl | hx := eq_or_ne x 0
+      · rw [opow_zero, one_mul] at hy
+        obtain ⟨m, rfl⟩ := Ordinal.lt_omega0.1 hy
+        simp
+      · simp [hx]
+    · rw [Nat.cast_one, one_opow, one_mul] at hy
+      obtain ⟨m, rfl⟩ := Ordinal.lt_omega0.1 hy
+      simp
+  · obtain ⟨k, hk⟩ := Ordinal.lt_omega0.1 (mod_lt x omega0_ne_zero)
+    rw [← div_add_mod x ω, opow_add, opow_mul, natCast_opow_omega0 hm, hk,
+      mul_assoc, opow_natCast, ← natCast_pow] at hy ⊢
+    rw [← natCast_mul, of_omega0_opow_mul_natCast_add, of_omega0_opow_mul_natCast,
+      Nat.cast_mul, mul_assoc]
+    apply hy.trans_eq
+    rw [opow_add_one, natCast_mul_omega0 (Nat.pow_pos hm.pos)]
+
+/-- See `of_natCast_opow_mul_natCast_add_of_lt` for a stronger version. -/
+theorem of_natCast_opow_mul_natCast_add_of_lt' {x y : Ordinal} {m : ℕ} (hy : y < m ^ x) (n : ℕ) :
+    of (m ^ x * n + y) = of (m ^ x) * n + of y :=
+  of_natCast_opow_mul_natCast_add_of_lt (hy.trans_le <| Ordinal.le_mul_left _ omega0_pos) n
+
+theorem of_natCast_opow_add_of_lt {x y : Ordinal} {m : ℕ} (hy : y < m ^ x * ω) :
+    of (m ^ x + y) = of (m ^ x) + of y := by
+  simpa using of_natCast_opow_mul_natCast_add_of_lt hy 1
+
+/-- See `of_natCast_opow_add_of_lt` for a stronger version. -/
+theorem of_natCast_opow_add_of_lt' {x y : Ordinal} {m : ℕ} (hy : y < m ^ x) :
+    of (m ^ x + y) = of (m ^ x) + of y := by
+  simpa using of_natCast_opow_mul_natCast_add_of_lt' hy 1
+
+@[simp]
+theorem of_natCast_opow_mul_natCast {x : Ordinal} (m n : ℕ) : of (m ^ x * n) = of (m ^ x) * n := by
+  cases m with
+  | zero =>
+    obtain rfl | hx := eq_or_ne x 0
+    · simp
+    · simp [hx]
+  | succ m => simpa using
+      of_natCast_opow_mul_natCast_add_of_lt' (opow_pos x m.cast_add_one_pos) n (m := m + 1)
+
+theorem two_opow_log_add {o : Ordinal} (ho : o ≠ 0) :
+    of (2 ^ log 2 o) + of (o % 2 ^ log 2 o) = of o := by
+  conv_rhs => rw [← Ordinal.two_opow_log_add ho]
+  exact (of_natCast_opow_add_of_lt' (mod_lt _ (opow_ne_zero _ two_ne_zero))).symm
 
 theorem wpow_add (x y : NatOrdinal) : ω^ (x + y) = ω^ x * ω^ y := by
   obtain rfl | hx := eq_or_ne x 0; · simp
@@ -196,5 +244,21 @@ theorem wpow_add (x y : NatOrdinal) : ω^ (x + y) = ω^ x * ω^ y := by
       exact wpow_mul_natCast_lt (add_lt_add_right hb x) m
 termination_by (x, y)
 
+theorem mul_lt_wpow_wpow (hx : x < ω^ ω^ z) (hy : y < ω^ ω^ z) : x * y < ω^ ω^ z := by
+  induction x with | mk x
+  induction y with | mk y
+  obtain rfl | hz := eq_or_ne z 0
+  · simp_rw [wpow_zero, wpow_one, of.lt_iff_lt, Ordinal.lt_omega0] at hx hy
+    obtain ⟨m, rfl⟩ := hx
+    obtain ⟨n, rfl⟩ := hy
+    simpa [← Nat.cast_mul] using Ordinal.natCast_lt_omega0 (m * n)
+  · rw [← val_ne_zero] at hz
+    rw [wpow_def, of.lt_iff_lt, val_wpow, lt_omega0_omega0_opow hz] at hx hy
+    obtain ⟨a, ha, m, hm⟩ := hx
+    obtain ⟨b, hb, n, hn⟩ := hy
+    rw [← of.lt_iff_lt] at hm hn
+    apply (mul_le_mul' hm.le hn.le).trans_lt
+    simpa [← wpow_add] using add_lt_wpow (wpow_mul_natCast_lt ha m) (wpow_mul_natCast_lt hb n)
+
 end NatOrdinal
 end

CombinatorialGames/Nimber/Basic.lean

@@ -6,7 +6,7 @@ Authors: Violeta Hernández Palacios
 module
 
 public meta import CombinatorialGames.Tactic.Register
-public import Mathlib.SetTheory.Ordinal.Family
+public import CombinatorialGames.NatOrdinal.Basic
 
 import CombinatorialGames.Tactic.OrdinalAlias
 import Mathlib.Data.Nat.Bitwise
@@ -64,6 +64,9 @@ theorem lt_two_iff {x : Nimber} : x < ∗2 ↔ x = 0 ∨ x = 1 := Set.ext_iff.1
 
 @[simp] theorem succ_one : Order.succ 1 = ∗2 := one_add_one_eq_two (R := Ordinal)
 
+theorem lt_omega0 {o : Nimber} : o < ∗.omega0 ↔ ∃ n : ℕ, o = ∗n :=
+  Ordinal.lt_omega0
+
 theorem not_small_nimber : ¬ Small.{u} Nimber.{u} := not_small_ordinal
 
 /-! ### Nimber addition -/
@@ -112,6 +115,21 @@ private theorem add_ne_of_lt (a b : Nimber) :
   rw [← add_def] at H
   simpa using H
 
+/-- A version of `add_le_nadd` stated in terms of `Ordinal`. -/
+theorem add_le_nadd' (a b : Ordinal) : (∗a + ∗b).val ≤ (NatOrdinal.of a + NatOrdinal.of b).val := by
+  rw [val_le_iff]
+  apply add_le_of_forall_ne
+  all_goals
+    intro c hc
+    induction c with | mk c
+    rw [← val_eq_iff.ne]
+    apply ((add_le_nadd' ..).trans_lt _).ne
+    simpa
+termination_by (a, b)
+
+theorem add_le_nadd (a b : Nimber) : a + b ≤ ∗(NatOrdinal.of a.val + NatOrdinal.of b.val).val :=
+  add_le_nadd' ..
+
 protected theorem add_comm (a b : Nimber) : a + b = b + a := by
   rw [add_def, add_def]
   simp_rw [or_comm]