feat(set_theory/game/pgame): add_lf_add_of_lf_of_le (#14150)

This generalizes the previously existing `add_lf_add` on `numeric` games.
leanprover-community · May 22, 2022 · 684587b · 684587b
1 parent b7952ee
commit 684587b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 33 deletions.
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
@@ -1257,6 +1257,12 @@ instance covariant_class_add_lt : covariant_class pgame pgame (+) (<) :=
   exact ⟨add_le_add_left h.1 x, add_lf_add_left h.2 x⟩
 end⟩
 
+theorem add_lf_add_of_lf_of_le {w x y z : pgame} (hwx : w ⧏ x) (hyz : y ≤ z) : w + y ⧏ x + z :=
+lf_of_lf_of_le (add_lf_add_right hwx y) (add_le_add_left hyz x)
+
+theorem add_lf_add_of_le_of_lf {w x y z : pgame} (hwx : w ≤ x) (hyz : y ⧏ z) : w + y ⧏ x + z :=
+lf_of_le_of_lf (add_le_add_right hwx y) (add_lf_add_left hyz x)
+
 theorem add_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y ≈ x + z :=
 ⟨(add_le_add_left h₂.1 w).trans (add_le_add_right h₁.1 z),
   (add_le_add_left h₂.2 x).trans (add_le_add_right h₁.2 y)⟩

diff --git a/src/set_theory/surreal/basic.lean b/src/set_theory/surreal/basic.lean
@@ -159,46 +159,15 @@ lt_of_lf o (o.move_right j) (pgame.lf_move_right j)
 theorem numeric.le_move_right {x : pgame} (o : numeric x) (j) : x ≤ x.move_right j :=
 (o.lt_move_right j).le
 
--- TODO: this can be generalized to `add_lf_add_of_lf_of_lt`, which doesn't depend on any `numeric`
--- hypotheses.
-theorem add_lf_add
-  {w x y z : pgame.{u}} (oy : numeric y) (oz : numeric z)
-  (hwx : w ⧏ x) (hyz : y ⧏ z) : w + y ⧏ x + z :=
-begin
-  rw lf_iff_forall_le at *,
-  rcases hwx with ⟨ix, hix⟩|⟨jw, hjw⟩;
-  rcases hyz with ⟨iz, hiz⟩|⟨jy, hjy⟩,
-  { refine or.inl ⟨to_left_moves_add (sum.inl ix), _⟩,
-    rw add_move_left_inl,
-    calc w + y ≤ move_left x ix + y : add_le_add_right hix _
-            ... ≤ move_left x ix + move_left z iz : add_le_add_left hiz _
-            ... ≤ move_left x ix + z : add_le_add_left (oz.move_left_le iz) _ },
-  { refine or.inl ⟨to_left_moves_add (sum.inl ix), _⟩,
-    rw add_move_left_inl,
-    calc w + y ≤ move_left x ix + y : add_le_add_right hix _
-            ... ≤ move_left x ix + move_right y jy : add_le_add_left (oy.le_move_right jy) _
-            ... ≤ move_left x ix + z : add_le_add_left hjy _ },
-  { refine or.inr ⟨to_right_moves_add (sum.inl jw), _⟩,
-    rw add_move_right_inl,
-    calc move_right w jw + y ≤ x + y : add_le_add_right hjw _
-            ... ≤ x + move_left z iz : add_le_add_left hiz _
-            ... ≤ x + z : add_le_add_left (oz.move_left_le iz) _ },
-  { refine or.inr ⟨to_right_moves_add (sum.inl jw), _⟩,
-    rw add_move_right_inl,
-    calc move_right w jw + y ≤ x + y : add_le_add_right hjw _
-            ... ≤ x + move_right y jy : add_le_add_left (oy.le_move_right jy) _
-            ... ≤ x + z : add_le_add_left hjy _ },
-end
-
 theorem numeric.add : Π {x y : pgame} (ox : numeric x) (oy : numeric y), numeric (x + y)
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ ox oy :=
 ⟨begin
    rintros (ix|iy) (jx|jy),
    { exact add_lt_add_right (ox.1 ix jx) _ },
    { apply lt_of_lf ((ox.move_left ix).add oy) (ox.add (oy.move_right jy))
-      (add_lf_add oy (oy.move_right jy) (pgame.move_left_lf ix) (pgame.lf_move_right jy)) },
+      (add_lf_add_of_lf_of_le (pgame.move_left_lf ix) (oy.le_move_right jy)) },
    { apply lt_of_lf (ox.add (oy.move_left iy)) ((ox.move_right jx).add oy)
-      (add_lf_add (oy.move_left iy) oy (pgame.lf_move_right jx) (pgame.move_left_lf iy)) },
+      (add_lf_add_of_lf_of_le (pgame.lf_move_right jx) (oy.move_left_le iy)) },
    { exact add_lt_add_left (oy.1 iy jy) ⟨xl, xr, xL, xR⟩ }
  end,
  begin