refactor(set_theory/game/pgame): rename and add theorems like -y ≤ -x ↔ x ≤ y (#14653)

For `*` in `le`, `lf`, `lt`, we rename `neg_*_iff : -y * -x ↔ x * y` to `neg_*_neg_iff`, and add the theorems `neg_*_iff : -y * x ↔ x * -y`.

We further add many missing corresponding theorems for equivalence and fuzziness.

Author: vihdzp

src/set_theory/game/basic.lean

@@ -44,7 +44,7 @@ namespace game
 
 instance : add_comm_group game :=
 { zero := ⟦0⟧,
-  neg := quot.lift (λ x, ⟦-x⟧) (λ x y h, quot.sound (@neg_congr x y h)),
+  neg := quot.lift (λ x, ⟦-x⟧) (λ x y h, quot.sound ((@neg_equiv_neg_iff x y).2 h)),
   add := quotient.lift₂ (λ x y : pgame, ⟦x + y⟧)
     (λ x₁ y₁ x₂ y₂ hx hy, quot.sound (pgame.add_congr hx hy)),
   add_zero := by { rintro ⟨x⟩, exact quot.sound (add_zero_equiv x) },

src/set_theory/game/birthday.lean

@@ -135,6 +135,6 @@ le_def.2 ⟨λ i, or.inl ⟨to_left_moves_to_pgame ⟨_, birthday_move_left_lt i
   by simp [le_birthday (xL i)]⟩, is_empty_elim⟩
 
 theorem neg_birthday_le (x : pgame) : -x.birthday.to_pgame ≤ x :=
-let h := le_birthday (-x) in by rwa [neg_birthday, ←neg_le_iff, neg_neg] at h
+let h := le_birthday (-x) in by rwa [neg_birthday, neg_le_iff] at h
 
 end pgame

src/set_theory/game/impartial.lean

@@ -63,7 +63,7 @@ theorem impartial_congr : ∀ {G H : pgame} (e : relabelling G H) [G.impartial],
 | G H e := begin
   introI h,
   rw impartial_def,
-  refine ⟨e.symm.equiv.trans ((neg_equiv_self G).trans (neg_congr e.equiv)),
+  refine ⟨e.symm.equiv.trans ((neg_equiv_self G).trans (neg_equiv_neg_iff.2 e.equiv)),
     λ i, _, λ j, _⟩;
   cases e with _ _ L R hL hR,
   { convert impartial_congr (hL (L.symm i)),
@@ -107,14 +107,14 @@ using_well_founded { dec_tac := pgame_wf_tac }
 
 lemma nonpos (G : pgame) [G.impartial] : ¬ 0 < G :=
 λ h, begin
-  have h' := neg_lt_iff.2 h,
+  have h' := neg_lt_neg_iff.2 h,
   rw [pgame.neg_zero, lt_congr_left (neg_equiv_self G).symm] at h',
   exact (h.trans h').false
 end
 
 lemma nonneg (G : pgame) [G.impartial] : ¬ G < 0 :=
 λ h, begin
-  have h' := neg_lt_iff.2 h,
+  have h' := neg_lt_neg_iff.2 h,
   rw [pgame.neg_zero, lt_congr_right (neg_equiv_self G).symm] at h',
   exact (h.trans h').false
 end

src/set_theory/game/pgame.lean

@@ -899,58 +899,97 @@ def relabelling.neg_congr : ∀ {x y : pgame}, x.relabelling y → (-x).relabell
     λ i, relabelling.neg_congr (by simpa using R_relabelling (R_equiv i)),
     λ i, relabelling.neg_congr (by simpa using L_relabelling (L_equiv.symm i))⟩
 
-@[simp] theorem neg_le_iff : Π {x y : pgame}, -y ≤ -x ↔ x ≤ y
+@[simp] theorem neg_le_neg_iff : Π {x y : pgame}, -y ≤ -x ↔ x ≤ y
 | (mk xl xr xL xR) (mk yl yr yL yR) :=
 begin
   rw [le_def, le_def], dsimp,
   refine ⟨λ h, ⟨λ i, _, λ j, _⟩, λ h, ⟨λ i, _, λ j, _⟩⟩,
   { rcases h.right i with ⟨w, h⟩ | ⟨w, h⟩,
-    { refine or.inr ⟨to_left_moves_neg.symm w, neg_le_iff.1 _⟩,
+    { refine or.inr ⟨to_left_moves_neg.symm w, neg_le_neg_iff.1 _⟩,
       rwa [move_right_neg_symm, neg_neg] },
-    { exact or.inl ⟨w, neg_le_iff.1 h⟩ } },
+    { exact or.inl ⟨w, neg_le_neg_iff.1 h⟩ } },
   { rcases h.left j with ⟨w, h⟩ | ⟨w, h⟩,
-    { exact or.inr ⟨w, neg_le_iff.1 h⟩ },
-    { refine or.inl ⟨to_right_moves_neg.symm w, neg_le_iff.1 _⟩,
+    { exact or.inr ⟨w, neg_le_neg_iff.1 h⟩ },
+    { refine or.inl ⟨to_right_moves_neg.symm w, neg_le_neg_iff.1 _⟩,
       rwa [move_left_neg_symm, neg_neg] } },
   { rcases h.right i with ⟨w, h⟩ | ⟨w, h⟩,
     { refine or.inr ⟨to_right_moves_neg w, _⟩,
-      convert neg_le_iff.2 h,
+      convert neg_le_neg_iff.2 h,
       rw move_right_neg },
-    { exact or.inl ⟨w, neg_le_iff.2 h⟩ } },
+    { exact or.inl ⟨w, neg_le_neg_iff.2 h⟩ } },
   { rcases h.left j with ⟨w, h⟩ | ⟨w, h⟩,
-    { exact or.inr ⟨w, neg_le_iff.2 h⟩ },
+    { exact or.inr ⟨w, neg_le_neg_iff.2 h⟩ },
     { refine or.inl ⟨to_left_moves_neg w, _⟩,
-      convert neg_le_iff.2 h,
+      convert neg_le_neg_iff.2 h,
       rw move_left_neg } }
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-theorem neg_congr {x y : pgame} (h : x ≈ y) : -x ≈ -y :=
-⟨neg_le_iff.2 h.2, neg_le_iff.2 h.1⟩
+@[simp] theorem neg_lf_neg_iff {x y : pgame} : -y ⧏ -x ↔ x ⧏ y :=
+by rw [←pgame.not_le, ←pgame.not_le, not_iff_not, neg_le_neg_iff]
 
-@[simp] theorem neg_lf_iff {x y : pgame} : -y ⧏ -x ↔ x ⧏ y :=
-by rw [←pgame.not_le, ←pgame.not_le, not_iff_not, neg_le_iff]
+@[simp] theorem neg_lt_neg_iff {x y : pgame} : -y < -x ↔ x < y :=
+by rw [lt_iff_le_and_lf, lt_iff_le_and_lf, neg_le_neg_iff, neg_lf_neg_iff]
 
-@[simp] theorem neg_lt_iff {x y : pgame} : -y < -x ↔ x < y :=
-by rw [lt_iff_le_and_lf, lt_iff_le_and_lf, neg_le_iff, neg_lf_iff]
+@[simp] theorem neg_equiv_neg_iff {x y : pgame} : -x ≈ -y ↔ x ≈ y :=
+by rw [equiv, equiv, neg_le_neg_iff, neg_le_neg_iff, and.comm]
+
+@[simp] theorem neg_fuzzy_neg_iff {x y : pgame} : -x ∥ -y ↔ x ∥ y :=
+by rw [fuzzy, fuzzy, neg_lf_neg_iff, neg_lf_neg_iff, and.comm]
+
+theorem neg_le_iff {x y : pgame} : -y ≤ x ↔ -x ≤ y :=
+by rw [←neg_neg x, neg_le_neg_iff, neg_neg]
+
+theorem neg_lf_iff {x y : pgame} : -y ⧏ x ↔ -x ⧏ y :=
+by rw [←neg_neg x, neg_lf_neg_iff, neg_neg]
+
+theorem neg_lt_iff {x y : pgame} : -y < x ↔ -x < y :=
+by rw [←neg_neg x, neg_lt_neg_iff, neg_neg]
+
+theorem neg_equiv_iff {x y : pgame} : -x ≈ y ↔ x ≈ -y :=
+by rw [←neg_neg y, neg_equiv_neg_iff, neg_neg]
+
+theorem neg_fuzzy_iff {x y : pgame} : -x ∥ y ↔ x ∥ -y :=
+by rw [←neg_neg y, neg_fuzzy_neg_iff, neg_neg]
+
+theorem le_neg_iff {x y : pgame} : y ≤ -x ↔ x ≤ -y :=
+by rw [←neg_neg x, neg_le_neg_iff, neg_neg]
+
+theorem lf_neg_iff {x y : pgame} : y ⧏ -x ↔ x ⧏ -y :=
+by rw [←neg_neg x, neg_lf_neg_iff, neg_neg]
+
+theorem lt_neg_iff {x y : pgame} : y < -x ↔ x < -y :=
+by rw [←neg_neg x, neg_lt_neg_iff, neg_neg]
 
 @[simp] theorem neg_le_zero_iff {x : pgame} : -x ≤ 0 ↔ 0 ≤ x :=
-by { convert neg_le_iff, rw pgame.neg_zero }
+by rw [neg_le_iff, pgame.neg_zero]
 
 @[simp] theorem zero_le_neg_iff {x : pgame} : 0 ≤ -x ↔ x ≤ 0 :=
-by { convert neg_le_iff, rw pgame.neg_zero }
+by rw [le_neg_iff, pgame.neg_zero]
 
 @[simp] theorem neg_lf_zero_iff {x : pgame} : -x ⧏ 0 ↔ 0 ⧏ x :=
-by { convert neg_lf_iff, rw pgame.neg_zero }
+by rw [neg_lf_iff, pgame.neg_zero]
 
 @[simp] theorem zero_lf_neg_iff {x : pgame} : 0 ⧏ -x ↔ x ⧏ 0 :=
-by { convert neg_lf_iff, rw pgame.neg_zero }
+by rw [lf_neg_iff, pgame.neg_zero]
 
 @[simp] theorem neg_lt_zero_iff {x : pgame} : -x < 0 ↔ 0 < x :=
-by { convert neg_lt_iff, rw pgame.neg_zero }
+by rw [neg_lt_iff, pgame.neg_zero]
 
 @[simp] theorem zero_lt_neg_iff {x : pgame} : 0 < -x ↔ x < 0 :=
-by { convert neg_lt_iff, rw pgame.neg_zero }
+by rw [lt_neg_iff, pgame.neg_zero]
+
+@[simp] theorem neg_equiv_zero_iff {x : pgame} : -x ≈ 0 ↔ x ≈ 0 :=
+by rw [neg_equiv_iff, pgame.neg_zero]
+
+@[simp] theorem neg_fuzzy_zero_iff {x : pgame} : -x ∥ 0 ↔ x ∥ 0 :=
+by rw [neg_fuzzy_iff, pgame.neg_zero]
+
+@[simp] theorem zero_equiv_neg_iff {x : pgame} : 0 ≈ -x ↔ 0 ≈ x :=
+by rw [←neg_equiv_iff, pgame.neg_zero]
+
+@[simp] theorem zero_fuzzy_neg_iff {x : pgame} : 0 ∥ -x ↔ 0 ∥ x :=
+by rw [←neg_fuzzy_iff, pgame.neg_zero]
 
 /-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
 instance : has_add pgame.{u} := ⟨λ x y, begin
@@ -1208,7 +1247,7 @@ end
 
 theorem zero_le_add_left_neg (x : pgame) : 0 ≤ -x + x :=
 begin
-  rw [←neg_le_iff, pgame.neg_zero],
+  rw [←neg_le_neg_iff, pgame.neg_zero],
   exact neg_add_le.trans (add_left_neg_le_zero _)
 end
 
@@ -1299,7 +1338,7 @@ theorem add_congr_right {x y z : pgame} : y ≈ z → x + y ≈ x + z :=
 add_congr equiv_rfl
 
 theorem sub_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w - y ≈ x - z :=
-add_congr h₁ (neg_congr h₂)
+add_congr h₁ (neg_equiv_neg_iff.2 h₂)
 
 theorem sub_congr_left {x y z : pgame} (h : x ≈ y) : x - z ≈ y - z :=
 sub_congr h equiv_rfl

src/set_theory/surreal/basic.lean

@@ -164,7 +164,7 @@ theorem numeric_zero : numeric 0 := numeric_of_is_empty 0
 theorem numeric_one : numeric 1 := numeric_of_is_empty_right_moves 1 $ λ _, numeric_zero
 
 theorem numeric.neg : Π {x : pgame} (o : numeric x), numeric (-x)
-| ⟨l, r, L, R⟩ o := ⟨λ j i, neg_lt_iff.2 (o.1 i j), λ j, (o.2.2 j).neg, λ i, (o.2.1 i).neg⟩
+| ⟨l, r, L, R⟩ o := ⟨λ j i, neg_lt_neg_iff.2 (o.1 i j), λ j, (o.2.2 j).neg, λ i, (o.2.1 i).neg⟩
 
 theorem numeric.move_left_lt {x : pgame} (o : numeric x) (i) : x.move_left i < x :=
 (pgame.move_left_lf i).lt (o.move_left i) o
@@ -274,7 +274,7 @@ the negation of `{L | R}` is `{-R | -L}`. -/
 instance : has_neg surreal  :=
 ⟨surreal.lift
   (λ x ox, ⟦⟨-x, ox.neg⟩⟧)
-  (λ _ _ _ _ a, quotient.sound (pgame.neg_congr a))⟩
+  (λ _ _ _ _ a, quotient.sound (pgame.neg_equiv_neg_iff.2 a))⟩
 
 instance : ordered_add_comm_group surreal :=
 { add               := (+),