feat(SetTheory/Surreal/Basic): surreal number multiplication (#14044)

prove multiplication of surreal numbers is well-defined, thus they form an ordered commutative ring


This is a port of a Lean 3 proof from [this mathlib branch](https://github.com/leanprover-community/mathlib/blob/surreal_mul_symm'/src/set_theory/surreal/basic.lean). It shows that multiplication of surreal numbers is well-defined, and therefore the surreal numbers form an ordered commutative ring.

Because `Surreal` is now a ring, the simp normal-form for scalar multiplication (by integers) is now `*`. This required changes throughout `SetTheory/Surreal/Dyadic`.

For the most part, I translated the Lean 3 code directly to Lean 4, although in a few cases, I couldn't get that to work and wrote a new proof instead.

There were some lemmas used that were in the mathlib branch that were not ported to mathlib4. I have ported those lemmas and put them in an appropriate place in mathlib4.

I copied over the author names from the Lean 3 code and added myself.



Co-authored-by: Junyan Xu <[email protected]>

Mathlib.lean

@@ -3800,6 +3800,7 @@ import Mathlib.SetTheory.Ordinal.Principal
 import Mathlib.SetTheory.Ordinal.Topology
 import Mathlib.SetTheory.Surreal.Basic
 import Mathlib.SetTheory.Surreal.Dyadic
+import Mathlib.SetTheory.Surreal.Multiplication
 import Mathlib.SetTheory.ZFC.Basic
 import Mathlib.SetTheory.ZFC.Ordinal
 import Mathlib.Tactic

Mathlib/Logic/Hydra.lean

@@ -86,6 +86,9 @@ theorem cutExpand_add_left {t u} (s) : CutExpand r (s + t) (s + u) ↔ CutExpand
   exists₂_congr fun _ _ ↦ and_congr Iff.rfl <| by rw [add_assoc, add_assoc, add_left_cancel_iff]
 #align relation.cut_expand_add_left Relation.cutExpand_add_left
 
+lemma cutExpand_add_right {s' s} (t) : CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s := by
+  convert cutExpand_add_left t using 2 <;> apply add_comm
+
 theorem cutExpand_iff [DecidableEq α] [IsIrrefl α r] {s' s : Multiset α} :
     CutExpand r s' s ↔
       ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t := by
@@ -104,6 +107,8 @@ theorem not_cutExpand_zero [IsIrrefl α r] (s) : ¬CutExpand r s 0 := by
   rintro ⟨_, _, _, ⟨⟩, _⟩
 #align relation.not_cut_expand_zero Relation.not_cutExpand_zero
 
+lemma cutExpand_zero {x} : CutExpand r 0 {x} := ⟨0, x, nofun, add_comm 0 _⟩
+
 /-- For any relation `r` on `α`, multiset addition `Multiset α × Multiset α → Multiset α` is a
   fibration between the game sum of `CutExpand r` with itself and `CutExpand r` itself. -/
 theorem cutExpand_fibration (r : α → α → Prop) :
@@ -121,6 +126,32 @@ theorem cutExpand_fibration (r : α → α → Prop) :
     · rw [add_assoc, erase_add_right_pos _ h]
 #align relation.cut_expand_fibration Relation.cutExpand_fibration
 
+/-- `cut_expand` preserves leftward-closedness under a relation. -/
+lemma cutExpand_closed [IsIrrefl α r] (p : α → Prop)
+    (h : ∀ {a' a}, r a' a → p a → p a') :
+    ∀ {s' s}, CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a := by
+  intros s' s
+  classical
+  rw [cutExpand_iff]
+  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
+  obtain (h'|h') := mem_add.1 h'
+  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]
+
+lemma cutExpand_double {a a₁ a₂} (h₁ : r a₁ a) (h₂ : r a₂ a) : CutExpand r {a₁, a₂} {a} :=
+  cutExpand_singleton <| by
+    simp only [insert_eq_cons, mem_cons, mem_singleton, forall_eq_or_imp, forall_eq]
+    tauto
+
+lemma cutExpand_pair_left {a' a b} (hr : r a' a) : CutExpand r {a', b} {a, b} :=
+    (cutExpand_add_right {b}).2 (cutExpand_singleton_singleton hr)
+
+lemma cutExpand_pair_right {a b' b} (hr : r b' b) : CutExpand r {a, b'} {a, b} :=
+    (cutExpand_add_left {a}).2 (cutExpand_singleton_singleton hr)
+
+lemma cutExpand_double_left {a a₁ a₂ b} (h₁ : r a₁ a) (h₂ : r a₂ a) :
+    CutExpand r {a₁, a₂, b} {a, b} :=
+  (cutExpand_add_right {b}).2 (cutExpand_double h₁ h₂)
+
 /-- A multiset is accessible under `CutExpand` if all its singleton subsets are,
   assuming `r` is irreflexive. -/
 theorem acc_of_singleton [IsIrrefl α r] {s : Multiset α} (hs : ∀ a ∈ s, Acc (CutExpand r) {a}) :

Mathlib/Logic/Relation.lean

@@ -527,6 +527,10 @@ theorem TransGen.closed {p : α → α → Prop} :
   TransGen.lift' id
 #align relation.trans_gen.closed Relation.TransGen.closed
 
+lemma TransGen.closed' {P : α → Prop} (dc : ∀ {a b}, r a b → P b → P a)
+    {a b : α} (h : TransGen r a b) : P b → P a :=
+  h.head_induction_on dc fun hr _ hi ↦ dc hr ∘ hi
+
 theorem TransGen.mono {p : α → α → Prop} :
     (∀ a b, r a b → p a b) → TransGen r a b → TransGen p a b :=
   TransGen.lift id

Mathlib/SetTheory/Game/Basic.lean

@@ -519,6 +519,8 @@ theorem quot_mul_neg (x y : PGame) : ⟦x * -y⟧ = (-⟦x * y⟧ : Game) :=
   Quot.sound (mulNegRelabelling x y).equiv
 #align pgame.quot_mul_neg SetTheory.PGame.quot_mul_neg
 
+theorem quot_neg_mul_neg (x y : PGame) : ⟦-x * -y⟧ = (⟦x * y⟧: Game) := by simp
+
 @[simp]
 theorem quot_left_distrib (x y z : PGame) : (⟦x * (y + z)⟧ : Game) = ⟦x * y⟧ + ⟦x * z⟧ :=
   match x, y, z with
@@ -843,6 +845,72 @@ theorem mul_assoc_equiv (x y z : PGame) : x * y * z ≈ x * (y * z) :=
   Quotient.exact <| quot_mul_assoc _ _ _
 #align pgame.mul_assoc_equiv SetTheory.PGame.mul_assoc_equiv
 
+/-- The left options of `x * y` of the first kind, i.e. of the form `xL * y + x * yL - xL * yL`. -/
+def mulOption (x y : PGame) (i: LeftMoves x) (j: LeftMoves y) : PGame :=
+    x.moveLeft i * y + x * y.moveLeft j - x.moveLeft i * y.moveLeft j
+
+/-- Any left option of `x * y` of the first kind is also a left option of `x * -(-y)` of
+  the first kind. -/
+lemma mulOption_neg_neg {x} (y) {i j} :
+    mulOption x y i j = mulOption x (-(-y)) i (toLeftMovesNeg $ toRightMovesNeg j) := by
+  dsimp only [mulOption]
+  congr 2
+  rw [neg_neg]
+  iterate 2 rw [moveLeft_neg, moveRight_neg, neg_neg]
+
+/-- The left options of `x * y` agree with that of `y * x` up to equivalence. -/
+lemma mulOption_symm (x y) {i j} : ⟦mulOption x y i j⟧ = (⟦mulOption y x j i⟧: Game) := by
+  dsimp only [mulOption, quot_sub, quot_add]
+  rw [add_comm]
+  congr 1
+  on_goal 1 => congr 1
+  all_goals rw [quot_mul_comm]
+
+/-- The left options of `x * y` of the second kind are the left options of `(-x) * (-y)` of the
+  first kind, up to equivalence. -/
+lemma leftMoves_mul_iff {x y : PGame} (P : Game → Prop) :
+    (∀ k, P ⟦(x * y).moveLeft k⟧) ↔
+    (∀ i j, P ⟦mulOption x y i j⟧) ∧ (∀ i j, P ⟦mulOption (-x) (-y) i j⟧) := by
+  cases x; cases y
+  constructor <;> intro h
+  on_goal 1 =>
+    constructor <;> intros i j
+    · exact h (Sum.inl (i, j))
+    convert h (Sum.inr (i, j)) using 1
+  on_goal 2 =>
+    rintro (⟨i, j⟩ | ⟨i, j⟩)
+    exact h.1 i j
+    convert h.2 i j using 1
+  all_goals
+    dsimp only [mk_mul_moveLeft_inr, quot_sub, quot_add, neg_def, mulOption, moveLeft_mk]
+    rw [← neg_def, ← neg_def]
+    congr 1
+    on_goal 1 => congr 1
+    all_goals rw [quot_neg_mul_neg]
+
+/-- The right options of `x * y` are the left options of `x * (-y)` and of `(-x) * y` of the first
+  kind, up to equivalence. -/
+lemma rightMoves_mul_iff {x y : PGame} (P : Game → Prop) :
+    (∀ k, P ⟦(x * y).moveRight k⟧) ↔
+    (∀ i j, P (-⟦mulOption x (-y) i j⟧)) ∧ (∀ i j, P (-⟦mulOption (-x) y i j⟧)) := by
+  cases x; cases y
+  constructor <;> intro h
+  on_goal 1 =>
+    constructor <;> intros i j
+    convert h (Sum.inl (i, j))
+  on_goal 2 => convert h (Sum.inr (i, j))
+  on_goal 3 =>
+    rintro (⟨i, j⟩ | ⟨i, j⟩)
+    convert h.1 i j using 1
+    on_goal 2 => convert h.2 i j using 1
+  all_goals
+    dsimp [mulOption]
+    rw [neg_sub', neg_add, ← neg_def]
+    congr 1
+    on_goal 1 => congr 1
+  any_goals rw [quot_neg_mul, neg_neg]
+  iterate 6 rw [quot_mul_neg, neg_neg]
+
 /-- Because the two halves of the definition of `inv` produce more elements
 on each side, we have to define the two families inductively.
 This is the indexing set for the function, and `invVal` is the function part. -/

Mathlib/SetTheory/Surreal/Basic.lean

@@ -30,27 +30,22 @@ Surreal numbers inherit the relations `≤` and `<` from games (`Surreal.instLE`
 
 ## Algebraic operations
 
-We show that the surreals form a linear ordered commutative group.
+In this file, we show that the surreals form a linear ordered commutative group.
 
-One can also map all the ordinals into the surreals!
-
-### Multiplication of surreal numbers
-
-The proof that multiplication lifts to surreal numbers is surprisingly difficult and is currently
-missing in the library. A sample proof can be found in Theorem 3.8 in the second reference below.
-The difficulty lies in the length of the proof and the number of theorems that need to proven
-simultaneously. This will make for a fun and challenging project.
+In `Mathlib.SetTheory.Surreal.Multiplication`, we define multiplication and show that the
+surreals form a linear ordered commutative ring.
 
-The branch `surreal_mul` contains some progress on this proof.
+One can also map all the ordinals into the surreals!
 
 ### Todo
 
 - Define the field structure on the surreals.
 
 ## References
 
-* [Conway, *On numbers and games*][conway2001]
-* [Schleicher, Stoll, *An introduction to Conway's games and numbers*][schleicher_stoll]
+* [Conway, *On numbers and games*][Conway2001]
+* [Schleicher, Stoll, *An introduction to Conway's games and numbers*][SchleicherStoll]
+
 -/
 
 
@@ -94,6 +89,11 @@ theorem moveRight {x : PGame} (o : Numeric x) (j : x.RightMoves) : Numeric (x.mo
   cases x; exact o.2.2 j
 #align pgame.numeric.move_right SetTheory.PGame.Numeric.moveRight
 
+lemma isOption {x' x} (h : IsOption x' x) (hx : Numeric x) : Numeric x' := by
+  cases h
+  · apply hx.moveLeft
+  · apply hx.moveRight
+
 end Numeric
 
 @[elab_as_elim]

Mathlib/SetTheory/Surreal/Dyadic.lean

@@ -8,7 +8,7 @@ import Mathlib.Algebra.Order.Group.Basic
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.SetTheory.Game.Birthday
-import Mathlib.SetTheory.Surreal.Basic
+import Mathlib.SetTheory.Surreal.Multiplication
 
 #align_import set_theory.surreal.dyadic from "leanprover-community/mathlib"@"92ca63f0fb391a9ca5f22d2409a6080e786d99f7"
 
@@ -179,54 +179,55 @@ theorem powHalf_zero : powHalf 0 = 1 :=
 #align surreal.pow_half_zero Surreal.powHalf_zero
 
 @[simp]
-theorem double_powHalf_succ_eq_powHalf (n : ℕ) : 2 • powHalf n.succ = powHalf n := by
-  rw [two_nsmul]; exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)
+theorem double_powHalf_succ_eq_powHalf (n : ℕ) : 2 * powHalf (n + 1) = powHalf n := by
+  rw [two_mul]; exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)
 #align surreal.double_pow_half_succ_eq_pow_half Surreal.double_powHalf_succ_eq_powHalf
 
 @[simp]
-theorem nsmul_pow_two_powHalf (n : ℕ) : 2 ^ n • powHalf n = 1 := by
+theorem nsmul_pow_two_powHalf (n : ℕ) : 2 ^ n * powHalf n = 1 := by
   induction' n with n hn
-  · simp only [Nat.zero_eq, pow_zero, powHalf_zero, one_smul]
-  · rw [← hn, ← double_powHalf_succ_eq_powHalf n, smul_smul (2 ^ n) 2 (powHalf n.succ), mul_comm,
-      pow_succ']
+  · simp only [pow_zero, powHalf_zero, mul_one]
+  · rw [← hn, ← double_powHalf_succ_eq_powHalf n, ← mul_assoc (2 ^ n) 2 (powHalf (n + 1)),
+      pow_succ', mul_comm 2 (2 ^ n)]
 #align surreal.nsmul_pow_two_pow_half Surreal.nsmul_pow_two_powHalf
 
 @[simp]
-theorem nsmul_pow_two_powHalf' (n k : ℕ) : 2 ^ n • powHalf (n + k) = powHalf k := by
+theorem nsmul_pow_two_powHalf' (n k : ℕ) : 2 ^ n * powHalf (n + k) = powHalf k := by
   induction' k with k hk
   · simp only [add_zero, Surreal.nsmul_pow_two_powHalf, Nat.zero_eq, eq_self_iff_true,
       Surreal.powHalf_zero]
   · rw [← double_powHalf_succ_eq_powHalf (n + k), ← double_powHalf_succ_eq_powHalf k,
-      smul_algebra_smul_comm] at hk
-    rwa [← zsmul_eq_zsmul_iff' two_ne_zero]
+      ← mul_assoc, mul_comm (2 ^ n) 2, mul_assoc] at hk
+    rw [← zsmul_eq_zsmul_iff' two_ne_zero]
+    simpa only [zsmul_eq_mul, Int.cast_ofNat]
 #align surreal.nsmul_pow_two_pow_half' Surreal.nsmul_pow_two_powHalf'
 
 theorem zsmul_pow_two_powHalf (m : ℤ) (n k : ℕ) :
-    (m * 2 ^ n) • powHalf (n + k) = m • powHalf k := by
-  rw [mul_zsmul]
+    (m * 2 ^ n) * powHalf (n + k) = m * powHalf k := by
+  rw [mul_assoc]
   congr
-  norm_cast
   exact nsmul_pow_two_powHalf' n k
 #align surreal.zsmul_pow_two_pow_half Surreal.zsmul_pow_two_powHalf
 
 theorem dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) :
-    m₁ • powHalf y₂ = m₂ • powHalf y₁ := by
+    m₁ * powHalf y₂ = m₂ * powHalf y₁ := by
   revert m₁ m₂
   wlog h : y₁ ≤ y₂
   · intro m₁ m₂ aux; exact (this (le_of_not_le h) aux.symm).symm
   intro m₁ m₂ h₂
   obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h
   rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂
   cases' h₂ with h₂ h₂
-  · rw [h₂, add_comm, zsmul_pow_two_powHalf m₂ c y₁]
+  · rw [h₂, add_comm]
+    simp_rw [Int.cast_mul, Int.cast_pow, Int.cast_ofNat, zsmul_pow_two_powHalf m₂ c y₁]
   · have := Nat.one_le_pow y₁ 2 Nat.succ_pos'
     norm_cast at h₂; omega
 #align surreal.dyadic_aux Surreal.dyadic_aux
 
 /-- The additive monoid morphism `dyadicMap` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/
-def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where
+noncomputable def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where
   toFun x :=
-    (Localization.liftOn x fun x y => x • powHalf (Submonoid.log y)) <| by
+    (Localization.liftOn x fun x y => x * powHalf (Submonoid.log y)) <| by
       intro m₁ m₂ n₁ n₂ h₁
       obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := Localization.r_iff_exists.mp h₁
       simp only [Subtype.coe_mk, mul_eq_mul_left_iff] at h₂
@@ -242,7 +243,7 @@ def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where
         rwa [ha₁, ha₂, mul_comm, mul_comm m₂]
       · have : (1 : ℤ) ≤ 2 ^ y₃ := mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
         linarith
-  map_zero' := Localization.liftOn_zero _ _
+  map_zero' := by simp_rw [Localization.liftOn_zero _ _, Int.cast_zero, zero_mul]
   map_add' x y :=
     Localization.induction_on₂ x y <| by
       rintro ⟨a, ⟨b, ⟨b', rfl⟩⟩⟩ ⟨c, ⟨d, ⟨d', rfl⟩⟩⟩
@@ -251,18 +252,19 @@ def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where
       simp_rw [Submonoid.pow_apply] at hpow₂
       simp_rw [Localization.add_mk, Localization.liftOn_mk,
         Submonoid.log_mul (Int.pow_right_injective h₂), hpow₂]
+      simp only [Int.cast_add, Int.cast_mul, Int.cast_pow, Int.cast_ofNat]
       calc
-        (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') =
-            (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b') := by
-          simp only [add_smul, mul_comm, add_comm]
-        _ = c • powHalf d' + a • powHalf b' := by simp only [zsmul_pow_two_powHalf]
-        _ = a • powHalf b' + c • powHalf d' := add_comm _ _
+        (2 ^ b' * c + 2 ^ d' * a) * powHalf (b' + d') =
+            (c * 2 ^ b') * powHalf (b' + d') + (a * 2 ^ d') * powHalf (d' + b') := by
+          simp only [right_distrib, mul_comm, add_comm]
+        _ = c * powHalf d' + a * powHalf b' := by simp only [zsmul_pow_two_powHalf]
+        _ = a * powHalf b' + c * powHalf d' := add_comm _ _
 #align surreal.dyadic_map Surreal.dyadicMap
 
 @[simp]
 theorem dyadicMap_apply (m : ℤ) (p : Submonoid.powers (2 : ℤ)) :
     dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) =
-      m • powHalf (Submonoid.log p) := by
+      m * powHalf (Submonoid.log p) := by
   rw [← Localization.mk_eq_mk']; rfl
 #align surreal.dyadic_map_apply Surreal.dyadicMap_apply
 
@@ -271,11 +273,12 @@ theorem dyadicMap_apply_pow (m : ℤ) (n : ℕ) :
     dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) =
       m • powHalf n := by
   rw [dyadicMap_apply, @Submonoid.log_pow_int_eq_self 2 one_lt_two]
+  simp only [zsmul_eq_mul]
 #align surreal.dyadic_map_apply_pow Surreal.dyadicMap_apply_pow
 
 @[simp]
 theorem dyadicMap_apply_pow' (m : ℤ) (n : ℕ) :
-    m • Surreal.powHalf (Submonoid.log (Submonoid.pow (2 : ℤ) n)) = m • powHalf n := by
+    m * Surreal.powHalf (Submonoid.log (Submonoid.pow (2 : ℤ) n)) = m * powHalf n := by
   rw [@Submonoid.log_pow_int_eq_self 2 one_lt_two]
 
 /-- We define dyadic surreals as the range of the map `dyadicMap`. -/