feat(SetTheory/Surreal/Basic): add some lemmas for Surreal.mk (#14600)

add some lemmas for Surreal.mk

Author: hwatheod

Mathlib/SetTheory/Surreal/Basic.lean

@@ -321,6 +321,10 @@ instance : One Surreal :=
 instance : Inhabited Surreal :=
   ⟨0⟩
 
+lemma mk_eq_mk {x y : PGame.{u}} {hx hy} : mk x hx = mk y hy ↔ x ≈ y := Quotient.eq
+
+lemma mk_eq_zero {x : PGame.{u}} {hx} : mk x hx = 0 ↔ x ≈ 0 := Quotient.eq
+
 /-- Lift an equivalence-respecting function on pre-games to surreals. -/
 def lift {α} (f : ∀ x, Numeric x → α)
     (H : ∀ {x y} (hx : Numeric x) (hy : Numeric y), x.Equiv y → f x hx = f y hy) : Surreal → α :=
@@ -344,10 +348,24 @@ instance instLE : LE Surreal :=
 @[simp]
 lemma mk_le_mk {x y : PGame.{u}} {hx hy} : mk x hx ≤ mk y hy ↔ x ≤ y := Iff.rfl
 
+lemma zero_le_mk {x : PGame.{u}} {hx} : 0 ≤ mk x hx ↔ 0 ≤ x := Iff.rfl
+
 instance instLT : LT Surreal :=
   ⟨lift₂ (fun x y _ _ => x < y) fun _ _ _ _ hx hy => propext (lt_congr hx hy)⟩
 #align surreal.has_lt Surreal.instLT
 
+lemma mk_lt_mk {x y : PGame.{u}} {hx hy} : mk x hx < mk y hy ↔ x < y := Iff.rfl
+
+lemma zero_lt_mk {x : PGame.{u}} {hx} : 0 < mk x hx ↔ 0 < x := Iff.rfl
+
+/-- Same as `moveLeft_lt`, but for `Surreal` instead of `PGame` -/
+theorem mk_moveLeft_lt_mk {x : PGame} (o : Numeric x) (i) :
+    Surreal.mk (x.moveLeft i) (Numeric.moveLeft o i) < Surreal.mk x o := Numeric.moveLeft_lt o i
+
+/-- Same as `lt_moveRight`, but for `Surreal` instead of `PGame` -/
+theorem mk_lt_mk_moveRight {x : PGame} (o : Numeric x) (j) :
+    Surreal.mk x o < Surreal.mk (x.moveRight j) (Numeric.moveRight o j) := Numeric.lt_moveRight o j
+
 /-- Addition on surreals is inherited from pre-game addition:
 the sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
 instance : Add Surreal :=
@@ -378,6 +396,14 @@ instance orderedAddCommGroup : OrderedAddCommGroup Surreal where
   nsmul := nsmulRec
   zsmul := zsmulRec
 
+lemma mk_add {x y : PGame} (hx : x.Numeric) (hy : y.Numeric) :
+    Surreal.mk (x + y) (hx.add hy) = Surreal.mk x hx + Surreal.mk y hy := by rfl
+
+lemma mk_sub {x y : PGame} (hx : x.Numeric) (hy : y.Numeric) :
+    Surreal.mk (x - y) (hx.sub hy) = Surreal.mk x hx - Surreal.mk y hy := by rfl
+
+lemma zero_def : 0 = mk 0 numeric_zero := by rfl
+
 noncomputable instance : LinearOrderedAddCommGroup Surreal :=
   { Surreal.orderedAddCommGroup with
     le_total := by