From a3e15d84c240dbe5089cec3f55d0379a9fe72a52 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 18 Jul 2023 05:18:46 +0000 Subject: [PATCH] chore: forward port #14324 (#5973) This is the remainder of the forward port of https://github.com/leanprover-community/mathlib/pull/14324. See https://leanprover-community.github.io/mathlib-port-status/file/set_theory/ordinal/natural_ops for the relevant #outofsync page. Co-authored-by: Scott Morrison --- Mathlib/SetTheory/Ordinal/NaturalOps.lean | 411 +++++++++++++++++++++- 1 file changed, 400 insertions(+), 11 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean index daefd16c3c3c8..bcfece40d121b 100644 --- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean +++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Violeta Hernández Palacios ! This file was ported from Lean 3 source module set_theory.ordinal.natural_ops -! leanprover-community/mathlib commit 740acc0e6f9adf4423f92a485d0456fc271482da +! leanprover-community/mathlib commit 31b269b60935483943542d547a6dd83a66b37dc7 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -79,8 +79,6 @@ namespace NatOrdinal open Ordinal -variable {a b c : NatOrdinal.{u}} - @[simp] theorem toOrdinal_symm_eq : NatOrdinal.toOrdinal.symm = Ordinal.toNatOrdinal := rfl @@ -183,16 +181,20 @@ theorem toNatOrdinal_eq_one (a) : toNatOrdinal a = 1 ↔ a = 1 := #align ordinal.to_nat_ordinal_eq_one Ordinal.toNatOrdinal_eq_one @[simp] -theorem toNatOrdinal_max : toNatOrdinal (max a b) = max (toNatOrdinal a) (toNatOrdinal b ) := +theorem toNatOrdinal_max (a b : Ordinal) : + toNatOrdinal (max a b) = max (toNatOrdinal a) (toNatOrdinal b) := rfl #align ordinal.to_nat_ordinal_max Ordinal.toNatOrdinal_max @[simp] -theorem toNatOrdinal_min : +theorem toNatOrdinal_min (a b : Ordinal) : toNatOrdinal (linearOrder.min a b) = linearOrder.min (toNatOrdinal a) (toNatOrdinal b) := rfl #align ordinal.to_nat_ordinal_min Ordinal.toNatOrdinal_min +/-! We place the definitions of `nadd` and `nmul` before actually developing their API, as this +guarantees we only need to open the `NaturalOps` locale once. -/ + /-- Natural addition on ordinals `a ♯ b`, also known as the Hessenberg sum, is recursively defined as the least ordinal greater than `a' ♯ b` and `a ♯ b'` for all `a' < a` and `b' < b`. In contrast to normal ordinal addition, it is commutative. @@ -210,6 +212,24 @@ scoped[NaturalOps] infixl:65 " ♯ " => Ordinal.nadd open NaturalOps +/-- Natural multiplication on ordinals `a ⨳ b`, also known as the Hessenberg product, is recursively +defined as the least ordinal such that `a ⨳ b + a' ⨳ b'` is greater than `a' ⨳ b + a ⨳ b'` for all +`a' < a` and `b < b'`. In contrast to normal ordinal multiplication, it is commutative and +distributive (over natural addition). + +Natural multiplication can equivalently be characterized as the ordinal resulting from multiplying +the Cantor normal forms of `a` and `b` as if they were polynomials in `ω`. Addition of exponents is +done via natural addition. -/ +noncomputable def nmul : Ordinal.{u} → Ordinal.{u} → Ordinal.{u} + | a, b => sInf {c | ∀ a' < a, ∀ b' < b, nmul a' b ♯ nmul a b' < c ♯ nmul a' b'} +termination_by nmul a b => (a, b) +#align ordinal.nmul Ordinal.nmul + +@[inherit_doc] +scoped[NaturalOps] infixl:70 " ⨳ " => Ordinal.nmul + +/-! ### Natural addition -/ + theorem nadd_def (a b : Ordinal) : a ♯ b = max (blsub.{u, u} a fun a' _ => a' ♯ b) (blsub.{u, u} b fun b' _ => a ♯ b') := by rw [nadd] @@ -336,10 +356,10 @@ theorem add_le_nadd : a + b ≤ a ♯ b := by end Ordinal -open Ordinal - namespace NatOrdinal +open Ordinal NaturalOps + instance : Add NatOrdinal := ⟨nadd⟩ @@ -358,7 +378,7 @@ instance add_contravariantClass_le : exact h.not_lt (add_lt_add_left h' a)⟩ #align nat_ordinal.add_contravariant_class_le NatOrdinal.add_contravariantClass_le -instance : OrderedCancelAddCommMonoid NatOrdinal := +instance orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid NatOrdinal := { NatOrdinal.linearOrder with add := (· + ·) add_assoc := nadd_assoc @@ -381,9 +401,8 @@ theorem add_one_eq_succ : ∀ a : NatOrdinal, a + 1 = succ a := theorem toOrdinal_cast_nat (n : ℕ) : toOrdinal n = n := by induction' n with n hn · rfl - · change nadd (toOrdinal n) 1 = n + 1 - rw [hn] - apply nadd_one + · change (toOrdinal n) ♯ 1 = n + 1 + rw [hn]; exact nadd_one n #align nat_ordinal.to_ordinal_cast_nat NatOrdinal.toOrdinal_cast_nat end NatOrdinal @@ -394,6 +413,10 @@ open NaturalOps namespace Ordinal +theorem nadd_eq_add (a b : Ordinal) : a ♯ b = toOrdinal (toNatOrdinal a + toNatOrdinal b) := + rfl +#align ordinal.nadd_eq_add Ordinal.nadd_eq_add + @[simp] theorem toNatOrdinal_cast_nat (n : ℕ) : toNatOrdinal n = n := by rw [← toOrdinal_cast_nat n] @@ -432,6 +455,22 @@ theorem nadd_le_nadd_iff_right : ∀ (a) {b c}, b ♯ a ≤ c ♯ a ↔ b ≤ c @_root_.add_le_add_iff_right NatOrdinal _ _ _ _ #align ordinal.nadd_le_nadd_iff_right Ordinal.nadd_le_nadd_iff_right +theorem nadd_le_nadd : ∀ {a b c d}, a ≤ b → c ≤ d → a ♯ c ≤ b ♯ d := + @add_le_add NatOrdinal _ _ _ _ +#align ordinal.nadd_le_nadd Ordinal.nadd_le_nadd + +theorem nadd_lt_nadd : ∀ {a b c d}, a < b → c < d → a ♯ c < b ♯ d := + @add_lt_add NatOrdinal _ _ _ _ +#align ordinal.nadd_lt_nadd Ordinal.nadd_lt_nadd + +theorem nadd_lt_nadd_of_lt_of_le : ∀ {a b c d}, a < b → c ≤ d → a ♯ c < b ♯ d := + @add_lt_add_of_lt_of_le NatOrdinal _ _ _ _ +#align ordinal.nadd_lt_nadd_of_lt_of_le Ordinal.nadd_lt_nadd_of_lt_of_le + +theorem nadd_lt_nadd_of_le_of_lt : ∀ {a b c d}, a ≤ b → c < d → a ♯ c < b ♯ d := + @add_lt_add_of_le_of_lt NatOrdinal _ _ _ _ +#align ordinal.nadd_lt_nadd_of_le_of_lt Ordinal.nadd_lt_nadd_of_le_of_lt + theorem nadd_left_cancel : ∀ {a b c}, a ♯ b = a ♯ c → b = c := @_root_.add_left_cancel NatOrdinal _ _ #align ordinal.nadd_left_cancel Ordinal.nadd_left_cancel @@ -448,4 +487,354 @@ theorem nadd_right_cancel_iff : ∀ {a b c}, b ♯ a = c ♯ a ↔ b = c := @add_right_cancel_iff NatOrdinal _ _ #align ordinal.nadd_right_cancel_iff Ordinal.nadd_right_cancel_iff +theorem le_nadd_self {a b} : a ≤ b ♯ a := by simpa using nadd_le_nadd_right (Ordinal.zero_le b) a +#align ordinal.le_nadd_self Ordinal.le_nadd_self + +theorem le_nadd_left {a b c} (h : a ≤ c) : a ≤ b ♯ c := + le_nadd_self.trans (nadd_le_nadd_left h b) +#align ordinal.le_nadd_left Ordinal.le_nadd_left + +theorem le_self_nadd {a b} : a ≤ a ♯ b := by simpa using nadd_le_nadd_left (Ordinal.zero_le b) a +#align ordinal.le_self_nadd Ordinal.le_self_nadd + +theorem le_nadd_right {a b c} (h : a ≤ b) : a ≤ b ♯ c := + le_self_nadd.trans (nadd_le_nadd_right h c) +#align ordinal.le_nadd_right Ordinal.le_nadd_right + +theorem nadd_left_comm : ∀ a b c, a ♯ (b ♯ c) = b ♯ (a ♯ c) := + @add_left_comm NatOrdinal _ +#align ordinal.nadd_left_comm Ordinal.nadd_left_comm + +theorem nadd_right_comm : ∀ a b c, a ♯ b ♯ c = a ♯ c ♯ b := + @add_right_comm NatOrdinal _ +#align ordinal.nadd_right_comm Ordinal.nadd_right_comm + +/-! ### Natural multiplication -/ + +variable {a b c d : Ordinal.{u}} + +theorem nmul_def (a b : Ordinal) : + a ⨳ b = sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} := by rw [nmul] +#align ordinal.nmul_def Ordinal.nmul_def + +/-- The set in the definition of `nmul` is nonempty. -/ +theorem nmul_nonempty (a b : Ordinal.{u}) : + {c : Ordinal.{u} | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}.Nonempty := + ⟨_, fun _ ha _ hb => (lt_blsub₂.{u, u, u} _ ha hb).trans_le le_self_nadd⟩ +#align ordinal.nmul_nonempty Ordinal.nmul_nonempty + +theorem nmul_nadd_lt {a' b' : Ordinal} (ha : a' < a) (hb : b' < b) : + a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b' := by + rw [nmul_def a b] + exact csInf_mem (nmul_nonempty a b) a' ha b' hb +#align ordinal.nmul_nadd_lt Ordinal.nmul_nadd_lt + +theorem nmul_nadd_le {a' b' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) : + a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b' := by + rcases lt_or_eq_of_le ha with (ha | rfl) + · rcases lt_or_eq_of_le hb with (hb | rfl) + · exact (nmul_nadd_lt ha hb).le + · rw [nadd_comm] + · exact le_rfl +#align ordinal.nmul_nadd_le Ordinal.nmul_nadd_le + +theorem lt_nmul_iff : c < a ⨳ b ↔ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b' := by + refine' ⟨fun h => _, _⟩ + · rw [nmul] at h + simpa using not_mem_of_lt_csInf h ⟨0, fun _ _ => bot_le⟩ + · rintro ⟨a', ha, b', hb, h⟩ + have := h.trans_lt (nmul_nadd_lt ha hb) + rwa [nadd_lt_nadd_iff_right] at this +#align ordinal.lt_nmul_iff Ordinal.lt_nmul_iff + +theorem nmul_le_iff : a ⨳ b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b' := by + rw [← not_iff_not]; simp [lt_nmul_iff] +#align ordinal.nmul_le_iff Ordinal.nmul_le_iff + +theorem nmul_comm : ∀ a b, a ⨳ b = b ⨳ a + | a, b => by + rw [nmul, nmul] + congr; ext x; constructor <;> intro H c hc d hd + -- Porting note: had to add additional arguments to `nmul_comm` here + -- for the termination checker. + · rw [nadd_comm, ← nmul_comm d b, ← nmul_comm a c, ← nmul_comm d] + exact H _ hd _ hc + · rw [nadd_comm, nmul_comm a d, nmul_comm c, nmul_comm c] + exact H _ hd _ hc +termination_by nmul_comm a b => (a, b) +#align ordinal.nmul_comm Ordinal.nmul_comm + +@[simp] +theorem nmul_zero (a) : a ⨳ 0 = 0 := by + rw [← Ordinal.le_zero, nmul_le_iff] + exact fun _ _ a ha => (Ordinal.not_lt_zero a ha).elim +#align ordinal.nmul_zero Ordinal.nmul_zero + +@[simp] +theorem zero_nmul (a) : 0 ⨳ a = 0 := by rw [nmul_comm, nmul_zero] +#align ordinal.zero_nmul Ordinal.zero_nmul + +@[simp] +theorem nmul_one (a : Ordinal) : a ⨳ 1 = a := by + rw [nmul] + simp only [lt_one_iff_zero, forall_eq, nmul_zero, nadd_zero] + convert csInf_Ici (α := Ordinal) + ext b + -- Porting note: added this `simp` line, as the result from `convert` + -- is slightly different. + simp only [Set.mem_setOf_eq, Set.mem_Ici] + refine' ⟨fun H => le_of_forall_lt fun c hc => _, fun ha c hc => _⟩ + -- Porting note: had to add arguments to `nmul_one` in the next two lines + -- for the termination checker. + · simpa only [nmul_one c] using H c hc + · simpa only [nmul_one c] using hc.trans_le ha +termination_by nmul_one a => a +#align ordinal.nmul_one Ordinal.nmul_one + +@[simp] +theorem one_nmul (a) : 1 ⨳ a = a := by rw [nmul_comm, nmul_one] +#align ordinal.one_nmul Ordinal.one_nmul + +theorem nmul_lt_nmul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c ⨳ a < c ⨳ b := + lt_nmul_iff.2 ⟨0, h₂, a, h₁, by simp⟩ +#align ordinal.nmul_lt_nmul_of_pos_left Ordinal.nmul_lt_nmul_of_pos_left + +theorem nmul_lt_nmul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a ⨳ c < b ⨳ c := + lt_nmul_iff.2 ⟨a, h₁, 0, h₂, by simp⟩ +#align ordinal.nmul_lt_nmul_of_pos_right Ordinal.nmul_lt_nmul_of_pos_right + +theorem nmul_le_nmul_of_nonneg_left (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c ⨳ a ≤ c ⨳ b := by + rcases lt_or_eq_of_le h₁ with (h₁ | rfl) <;> rcases lt_or_eq_of_le h₂ with (h₂ | rfl) + · exact (nmul_lt_nmul_of_pos_left h₁ h₂).le + all_goals simp +#align ordinal.nmul_le_nmul_of_nonneg_left Ordinal.nmul_le_nmul_of_nonneg_left + +theorem nmul_le_nmul_of_nonneg_right (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a ⨳ c ≤ b ⨳ c := by + rw [nmul_comm, nmul_comm b] + exact nmul_le_nmul_of_nonneg_left h₁ h₂ +#align ordinal.nmul_le_nmul_of_nonneg_right Ordinal.nmul_le_nmul_of_nonneg_right + +theorem nmul_nadd : ∀ a b c, a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c + | a, b, c => by + refine le_antisymm (nmul_le_iff.2 fun a' ha d hd => ?_) + (nadd_le_iff.2 ⟨fun d hd => ?_, fun d hd => ?_⟩) + · -- Porting note: adding arguments to `nmul_nadd` for the termination checker. + rw [nmul_nadd a' b c] + rcases lt_nadd_iff.1 hd with (⟨b', hb, hd⟩ | ⟨c', hc, hd⟩) + · have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha hb) (nmul_nadd_le ha.le hd) + -- Porting note: adding arguments to `nmul_nadd` for the termination checker. + rw [nmul_nadd a' b' c, nmul_nadd a b' c] at this + simp only [nadd_assoc] at this + rwa [nadd_left_comm, nadd_left_comm _ (a ⨳ b'), nadd_left_comm (a ⨳ b), + nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ b), nadd_left_comm (a ⨳ b), + nadd_lt_nadd_iff_left, ← nadd_assoc, ← nadd_assoc] at this + · have := nadd_lt_nadd_of_le_of_lt (nmul_nadd_le ha.le hd) (nmul_nadd_lt ha hc) + -- Porting note: adding arguments to `nmul_nadd` for the termination checker. + rw [nmul_nadd a' b c', nmul_nadd a b c'] at this + simp only [nadd_assoc] at this + rwa [nadd_left_comm, nadd_comm (a ⨳ c), nadd_left_comm (a' ⨳ d), nadd_left_comm (a ⨳ c'), + nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left, nadd_comm (a' ⨳ c), nadd_left_comm (a ⨳ d), + nadd_left_comm (a' ⨳ b), nadd_left_comm (a ⨳ b), nadd_lt_nadd_iff_left, nadd_comm (a ⨳ d), + nadd_comm (a' ⨳ d), ← nadd_assoc, ← nadd_assoc] at this + · rcases lt_nmul_iff.1 hd with ⟨a', ha, b', hb, hd⟩ + have := nadd_lt_nadd_of_le_of_lt hd (nmul_nadd_lt ha (nadd_lt_nadd_right hb c)) + -- Porting note: adding arguments to `nmul_nadd` for the termination checker. + rw [nmul_nadd a' b c, nmul_nadd a b' c, nmul_nadd a'] at this + simp only [nadd_assoc] at this + rwa [nadd_left_comm (a' ⨳ b'), nadd_left_comm, nadd_lt_nadd_iff_left, nadd_left_comm, + nadd_left_comm _ (a' ⨳ b'), nadd_left_comm (a ⨳ b'), nadd_lt_nadd_iff_left, + nadd_left_comm (a' ⨳ c), nadd_left_comm, nadd_lt_nadd_iff_left, nadd_left_comm, + nadd_comm _ (a' ⨳ c), nadd_lt_nadd_iff_left] at this + · rcases lt_nmul_iff.1 hd with ⟨a', ha, c', hc, hd⟩ + have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha (nadd_lt_nadd_left hc b)) hd + -- Porting note: adding arguments to `nmul_nadd` for the termination checker. + rw [nmul_nadd a' b c, nmul_nadd a b c', nmul_nadd a'] at this + simp only [nadd_assoc] at this + rwa [nadd_left_comm _ (a' ⨳ b), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c'), + nadd_left_comm _ (a' ⨳ c), nadd_lt_nadd_iff_left, nadd_left_comm, nadd_comm (a' ⨳ c'), + nadd_left_comm _ (a ⨳ c'), nadd_lt_nadd_iff_left, nadd_comm _ (a' ⨳ c'), + nadd_comm _ (a' ⨳ c'), nadd_left_comm, nadd_lt_nadd_iff_left] at this +termination_by nmul_nadd a b c => (a, b, c) +#align ordinal.nmul_nadd Ordinal.nmul_nadd + +theorem nadd_nmul (a b c) : (a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c := by + rw [nmul_comm, nmul_nadd, nmul_comm, nmul_comm c] +#align ordinal.nadd_nmul Ordinal.nadd_nmul + +theorem nmul_nadd_lt₃ {a' b' c' : Ordinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) : + a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < + a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' := by + simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_lt (nmul_nadd_lt ha hb) hc +#align ordinal.nmul_nadd_lt₃ Ordinal.nmul_nadd_lt₃ + +theorem nmul_nadd_le₃ {a' b' c' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) : + a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤ + a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' := by + simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_le (nmul_nadd_le ha hb) hc +#align ordinal.nmul_nadd_le₃ Ordinal.nmul_nadd_le₃ + +theorem nmul_nadd_lt₃' {a' b' c' : Ordinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) : + a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') < + a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') := by + simp only [nmul_comm _ (_ ⨳ _)] + convert nmul_nadd_lt₃ hb hc ha using 1 <;> + · simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]; abel_nf +#align ordinal.nmul_nadd_lt₃' Ordinal.nmul_nadd_lt₃' + +theorem nmul_nadd_le₃' {a' b' c' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) : + a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') ≤ + a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') := by + simp only [nmul_comm _ (_ ⨳ _)] + convert nmul_nadd_le₃ hb hc ha using 1 <;> + · simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]; abel_nf +#align ordinal.nmul_nadd_le₃' Ordinal.nmul_nadd_le₃' + +theorem lt_nmul_iff₃ : + d < a ⨳ b ⨳ c ↔ + ∃ a' < a, ∃ b' < b, ∃ c' < c, + d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ + a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' := by + -- Porting note: was `refine' ⟨fun h => _, _⟩`, but can't get that to work? + constructor + · intro h + rcases lt_nmul_iff.1 h with ⟨e, he, c', hc, H₁⟩ + rcases lt_nmul_iff.1 he with ⟨a', ha, b', hb, H₂⟩ + refine' ⟨a', ha, b', hb, c', hc, _⟩ + have := nadd_le_nadd H₁ (nmul_nadd_le H₂ hc.le) + simp only [nadd_nmul, nadd_assoc] at this + rw [nadd_left_comm, nadd_left_comm d, nadd_left_comm, nadd_le_nadd_iff_left, + nadd_left_comm (a ⨳ b' ⨳ c), nadd_left_comm (a' ⨳ b ⨳ c), nadd_left_comm (a ⨳ b ⨳ c'), + nadd_le_nadd_iff_left, nadd_left_comm (a ⨳ b ⨳ c'), nadd_left_comm (a ⨳ b ⨳ c')] at this + simpa only [nadd_assoc] + · rintro ⟨a', ha, b', hb, c', hc, h⟩ + have := h.trans_lt (nmul_nadd_lt₃ ha hb hc) + repeat' rw [nadd_lt_nadd_iff_right] at this + assumption +#align ordinal.lt_nmul_iff₃ Ordinal.lt_nmul_iff₃ + +theorem nmul_le_iff₃ : + a ⨳ b ⨳ c ≤ d ↔ + ∀ a' < a, ∀ b' < b, ∀ c' < c, + a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < + d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' := by + rw [← not_iff_not]; simp [lt_nmul_iff₃] +#align ordinal.nmul_le_iff₃ Ordinal.nmul_le_iff₃ + +theorem lt_nmul_iff₃' : + d < a ⨳ (b ⨳ c) ↔ + ∃ a' < a, ∃ b' < b, ∃ c' < c, + d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤ + a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') := by + simp only [nmul_comm _ (_ ⨳ _), lt_nmul_iff₃, nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal] + constructor <;> rintro ⟨b', hb, c', hc, a', ha, h⟩ + · use a', ha, b', hb, c', hc; convert h using 1 <;> abel_nf + · use c', hc, a', ha, b', hb; convert h using 1 <;> abel_nf +#align ordinal.lt_nmul_iff₃' Ordinal.lt_nmul_iff₃' + +theorem nmul_le_iff₃' : + a ⨳ (b ⨳ c) ≤ d ↔ + ∀ a' < a, ∀ b' < b, ∀ c' < c, + a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') < + d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') := by + rw [← not_iff_not]; simp [lt_nmul_iff₃'] +#align ordinal.nmul_le_iff₃' Ordinal.nmul_le_iff₃' + +theorem nmul_assoc : ∀ a b c, a ⨳ b ⨳ c = a ⨳ (b ⨳ c) + | a, b, c => by + apply le_antisymm + · rw [nmul_le_iff₃] + intro a' ha b' hb c' hc + -- Porting note: the next line was just + -- repeat' rw [nmul_assoc] + -- but we need to spell out the arguments for the termination checker. + rw [nmul_assoc a' b c, nmul_assoc a b' c, nmul_assoc a b c', nmul_assoc a' b' c', + nmul_assoc a' b' c, nmul_assoc a' b c', nmul_assoc a b' c'] + exact nmul_nadd_lt₃' ha hb hc + · rw [nmul_le_iff₃'] + intro a' ha b' hb c' hc + -- Porting note: the next line was just + -- repeat' rw [← nmul_assoc] + -- but we need to spell out the arguments for the termination checker. + rw [← nmul_assoc a' b c, ← nmul_assoc a b' c, ← nmul_assoc a b c', ← nmul_assoc a' b' c', + ← nmul_assoc a' b' c, ← nmul_assoc a' b c', ← nmul_assoc a b' c'] + exact nmul_nadd_lt₃ ha hb hc +termination_by nmul_assoc a b c => (a, b, c) +#align ordinal.nmul_assoc Ordinal.nmul_assoc + +end Ordinal + +open Ordinal + +instance : Mul NatOrdinal := + ⟨nmul⟩ + +-- 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 + mul := (· * ·) + left_distrib := nmul_nadd + right_distrib := nadd_nmul + zero_mul := zero_nmul + mul_zero := nmul_zero + mul_assoc := nmul_assoc + one := 1 + one_mul := one_nmul + mul_one := nmul_one + mul_comm := nmul_comm + zero_le_one := @zero_le_one Ordinal _ _ _ _ + mul_le_mul_of_nonneg_left := fun a b c => nmul_le_nmul_of_nonneg_left + mul_le_mul_of_nonneg_right := fun a b c => nmul_le_nmul_of_nonneg_right } + +namespace Ordinal + +theorem nmul_eq_mul (a b) : a ⨳ b = toOrdinal (toNatOrdinal a * toNatOrdinal b) := + rfl +#align ordinal.nmul_eq_mul Ordinal.nmul_eq_mul + +theorem nmul_nadd_one : ∀ a b, a ⨳ (b ♯ 1) = a ⨳ b ♯ a := + @mul_add_one NatOrdinal _ _ _ +#align ordinal.nmul_nadd_one Ordinal.nmul_nadd_one + +theorem nadd_one_nmul : ∀ a b, (a ♯ 1) ⨳ b = a ⨳ b ♯ b := + @add_one_mul NatOrdinal _ _ _ +#align ordinal.nadd_one_nmul Ordinal.nadd_one_nmul + +theorem nmul_succ (a b) : a ⨳ succ b = a ⨳ b ♯ a := by rw [← nadd_one, nmul_nadd_one] +#align ordinal.nmul_succ Ordinal.nmul_succ + +theorem succ_nmul (a b) : succ a ⨳ b = a ⨳ b ♯ b := by rw [← nadd_one, nadd_one_nmul] +#align ordinal.succ_nmul Ordinal.succ_nmul + +theorem nmul_add_one : ∀ a b, a ⨳ (b + 1) = a ⨳ b ♯ a := + nmul_succ +#align ordinal.nmul_add_one Ordinal.nmul_add_one + +theorem add_one_nmul : ∀ a b, (a + 1) ⨳ b = a ⨳ b ♯ b := + succ_nmul +#align ordinal.add_one_nmul Ordinal.add_one_nmul + end Ordinal + +namespace NatOrdinal + +open Ordinal + +theorem mul_le_nmul (a b : Ordinal.{u}) : a * b ≤ a ⨳ b := by + refine b.limitRecOn ?_ ?_ ?_ + · simp + · intro c h + rw [mul_succ, nmul_succ] + exact (add_le_nadd _ a).trans (nadd_le_nadd_right h a) + · intro c hc H + rcases eq_zero_or_pos a with (rfl | ha) + · simp + · -- Porting note: `this` was inline in the `rw`, but now needs a preliminary `dsimp at this`. + have := IsNormal.blsub_eq.{u, u} (mul_isNormal ha) hc + dsimp at this + rw [← this, blsub_le_iff] + exact fun i hi => (H i hi).trans_lt (nmul_lt_nmul_of_pos_left hi ha) +#align nat_ordinal.mul_le_nmul NatOrdinal.mul_le_nmul + +end NatOrdinal