feat(set_theory/game/pgame): x.move_left i < x and variants (#13654)

Author: vihdzp

src/set_theory/game/pgame.lean

@@ -386,12 +386,35 @@ end
 | ⟨l, r, L, R⟩ := by rw mk_le_mk; exact
 ⟨λ i, lt_mk_of_le (le_refl _), λ i, mk_lt_of_le (le_refl _)⟩
 
+protected theorem le_rfl {x : pgame} : x ≤ x :=
+pgame.le_refl x
+
 protected theorem lt_irrefl (x : pgame) : ¬ x < x :=
 not_lt.2 (pgame.le_refl _)
 
 protected theorem ne_of_lt : ∀ {x y : pgame}, x < y → x ≠ y
 | x _ h rfl := pgame.lt_irrefl x h
 
+/-- In general, `xL i ≤ x` isn't true. It is true however for `numeric` games, see
+`numeric.move_left_le`. -/
+theorem lt_mk {xl xr : Type u} {xL : xl → pgame} {xR : xr → pgame} (i) : xL i < mk xl xr xL xR :=
+lt_mk_of_le pgame.le_rfl
+
+/-- In general, `x ≤ xR i` isn't true. It is true however for `numeric` games, see
+`numeric.move_right_le`. -/
+theorem mk_lt {xl xr : Type u} {xL : xl → pgame} {xR : xr → pgame} (i) : mk xl xr xL xR < xR i :=
+mk_lt_of_le pgame.le_rfl
+
+/-- In general, `x.move_left i ≤ x` isn't true. It is true however for `numeric` games, see
+`numeric.move_left_le`. -/
+theorem move_left_lt {x : pgame} (i) : x.move_left i < x :=
+move_left_lt_of_le pgame.le_rfl
+
+/-- In general, `x ≤ x.move_right i` isn't true. It is true however for `numeric` games, see
+`numeric.move_right_le`. -/
+theorem lt_move_right {x : pgame} (i) : x < x.move_right i :=
+lt_move_right_of_le pgame.le_rfl
+
 theorem le_trans_aux
   {xl xr} {xL : xl → pgame} {xR : xr → pgame}
   {yl yr} {yL : yl → pgame} {yR : yr → pgame}

src/set_theory/surreal/basic.lean

@@ -108,35 +108,15 @@ theorem numeric_neg : Π {x : pgame} (o : numeric x), numeric (-x)
 ⟨λ j i, lt_iff_neg_gt.1 (o.1 i j),
   ⟨λ j, numeric_neg (o.2.2 j), λ i, numeric_neg (o.2.1 i)⟩⟩
 
--- We provide this as an analogue for `numeric.move_left_le`,
--- even though it does not need the `numeric` hypothesis.
-@[nolint unused_arguments]
-theorem numeric.move_left_lt {x : pgame.{u}} (o : numeric x) (i : x.left_moves) :
-  x.move_left i < x :=
-begin
-  rw lt_def_le,
-  left,
-  use i,
-end
-
+/-- For the `<` version, see `pgame.move_left_lt`. -/
 theorem numeric.move_left_le {x : pgame} (o : numeric x) (i : x.left_moves) :
   x.move_left i ≤ x :=
-le_of_lt (o.move_left i) o (o.move_left_lt i)
-
--- We provide this as an analogue for `numeric.le_move_right`,
--- even though it does not need the `numeric` hypothesis.
-@[nolint unused_arguments]
-theorem numeric.lt_move_right {x : pgame} (o : numeric x) (j : x.right_moves) :
-  x < x.move_right j :=
-begin
-  rw lt_def_le,
-  right,
-  use j,
-end
+le_of_lt (o.move_left i) o (pgame.move_left_lt i)
 
+/-- For the `<` version, see `pgame.lt_move_right`. -/
 theorem numeric.le_move_right {x : pgame} (o : numeric x) (j : x.right_moves) :
   x ≤ x.move_right j :=
-le_of_lt o (o.move_right j) (o.lt_move_right j)
+le_of_lt o (o.move_right j) (pgame.lt_move_right j)
 
 theorem add_lt_add
   {w x y z : pgame.{u}} (oy : numeric y) (oz : numeric z)
@@ -178,10 +158,10 @@ theorem numeric_add : Π {x y : pgame} (ox : numeric x) (oy : numeric y), numeri
    { show xL ix + ⟨yl, yr, yL, yR⟩ < xR jx + ⟨yl, yr, yL, yR⟩,
      exact add_lt_add_right (ox.1 ix jx) _ },
    { show xL ix + ⟨yl, yr, yL, yR⟩ < ⟨xl, xr, xL, xR⟩ + yR jy,
-     exact add_lt_add oy (oy.move_right jy) (ox.move_left_lt _) (oy.lt_move_right _), },
-   { --  show ⟨xl, xr, xL, xR⟩ + yL iy < xR jx + ⟨yl, yr, yL, yR⟩, -- fails?
-     exact add_lt_add (oy.move_left iy) oy (ox.lt_move_right _) (oy.move_left_lt _), },
-   { --  show ⟨xl, xr, xL, xR⟩ + yL iy < ⟨xl, xr, xL, xR⟩ + yR jy, -- fails?
+     exact add_lt_add oy (oy.move_right jy) (pgame.lt_mk ix) (pgame.mk_lt jy), },
+   { -- show ⟨xl, xr, xL, xR⟩ + yL iy < xR jx + ⟨yl, yr, yL, yR⟩, -- fails?
+     exact add_lt_add (oy.move_left iy) oy (pgame.mk_lt jx) (pgame.lt_mk iy), },
+   { -- show ⟨xl, xr, xL, xR⟩ + yL iy < ⟨xl, xr, xL, xR⟩ + yR jy, -- fails?
      exact @add_lt_add_left pgame _ _ _ _ _ (oy.1 iy jy) ⟨xl, xr, xL, xR⟩ }
  end,
  begin

src/set_theory/surreal/dyadic.lean

@@ -66,12 +66,12 @@ begin
     { rintro ⟨ ⟩ ⟨ ⟩,
       dsimp only [pi.zero_apply],
       rw ← pow_half_move_left' n,
-      apply hn.move_left_lt },
+      apply pgame.move_left_lt },
     { exact ⟨λ _, numeric_zero, λ _, hn⟩ } }
 end
 
 theorem pow_half_succ_lt_pow_half {n : ℕ} : pow_half (n + 1) < pow_half n :=
-(@numeric_pow_half (n + 1)).lt_move_right punit.star
+pgame.lt_move_right punit.star
 
 theorem pow_half_succ_le_pow_half {n : ℕ} : pow_half (n + 1) ≤ pow_half n :=
 le_of_lt numeric_pow_half numeric_pow_half pow_half_succ_lt_pow_half