feat(set_theory/game/pgame): Add dot notation on many lemmas (#14149)

src/set_theory/game/basic.lean

@@ -21,17 +21,14 @@ imply `x * z ≈ y * z`. Hence, multiplication is not a well-defined operation o
 the abelian group structure on games allows us to simplify many proofs for pre-games.
 -/
 
-open function
+open function pgame
 
 universes u
 
 local infix ` ≈ ` := pgame.equiv
 
 instance pgame.setoid : setoid pgame :=
-⟨λ x y, x ≈ y,
- λ x, pgame.equiv_refl _,
- λ x y, pgame.equiv_symm,
- λ x y z, pgame.equiv_trans⟩
+⟨(≈), equiv_refl, @pgame.equiv.symm, @pgame.equiv.trans⟩
 
 /-- The type of combinatorial games. In ZFC, a combinatorial game is constructed from
   two sets of combinatorial games that have been constructed at an earlier
@@ -43,8 +40,6 @@ instance pgame.setoid : setoid pgame :=
   `x ≈ y ↔ x ≤ y ∧ y ≤ x`. -/
 abbreviation game := quotient pgame.setoid
 
-open pgame
-
 namespace game
 
 instance : add_comm_group game :=

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 ⟨equiv_trans e.symm.equiv (equiv_trans (neg_equiv_self G) (neg_congr e.equiv)),
+  refine ⟨e.symm.equiv.trans ((neg_equiv_self G).trans (neg_congr e.equiv)),
     λ i, _, λ j, _⟩;
   cases e with _ _ L R hL hR,
   { convert impartial_congr (hL (L.symm i)),
@@ -77,7 +77,7 @@ instance impartial_add : ∀ (G H : pgame) [G.impartial] [H.impartial], (G + H).
 begin
   introsI hG hH,
   rw impartial_def,
-  refine ⟨equiv_trans (add_congr (neg_equiv_self _) (neg_equiv_self _))
+  refine ⟨(add_congr (neg_equiv_self _) (neg_equiv_self _)).trans
     (neg_add_relabelling _ _).equiv.symm, λ i, _, λ i, _⟩,
   { rcases left_moves_add_cases i with ⟨j, rfl⟩ | ⟨j, rfl⟩,
     all_goals
@@ -108,14 +108,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,
-  rw [pgame.neg_zero, lt_congr_left (equiv_symm (neg_equiv_self G))] at 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,
-  rw [pgame.neg_zero, lt_congr_right (equiv_symm (neg_equiv_self G))] at h',
+  rw [pgame.neg_zero, lt_congr_right (neg_equiv_self G).symm] at h',
   exact (h.trans h').false
 end
 
@@ -138,7 +138,7 @@ lemma not_first_loses (G : pgame) [G.impartial] : ¬G.first_loses ↔ G.first_wi
 iff.symm $ iff_not_comm.1 $ iff.symm $ not_first_wins G
 
 lemma add_self (G : pgame) [G.impartial] : (G + G).first_loses :=
-first_loses_is_zero.2 $ equiv_trans (add_congr_left (neg_equiv_self G)) (add_left_neg_equiv G)
+first_loses_is_zero.2 $ (add_congr_left (neg_equiv_self G)).trans (add_left_neg_equiv G)
 
 lemma equiv_iff_sum_first_loses (G H : pgame) [G.impartial] [H.impartial] :
   G ≈ H ↔ (G + H).first_loses :=

src/set_theory/game/nim.lean

@@ -249,7 +249,7 @@ using_well_founded { dec_tac := pgame_wf_tac }
 @[simp] lemma grundy_value_eq_iff_equiv_nim (G : pgame) [G.impartial] (O : ordinal) :
   grundy_value G = O ↔ G ≈ nim O :=
 ⟨by { rintro rfl, exact equiv_nim_grundy_value G },
-  by { intro h, rw ←nim.equiv_iff_eq, exact equiv_trans (equiv_symm (equiv_nim_grundy_value G)) h }⟩
+  by { intro h, rw ←nim.equiv_iff_eq, exact (equiv_nim_grundy_value G).symm.trans h }⟩
 
 lemma nim.grundy_value (O : ordinal.{u}) : grundy_value (nim O) = O :=
 by simp
@@ -258,12 +258,12 @@ by simp
   grundy_value G = grundy_value H ↔ G ≈ H :=
 (grundy_value_eq_iff_equiv_nim _ _).trans (equiv_congr_left.1 (equiv_nim_grundy_value H) _).symm
 
-@[simp] lemma grundy_value_zero : grundy_value 0 = 0 := by simp [equiv_symm nim.nim_zero_equiv]
+@[simp] lemma grundy_value_zero : grundy_value 0 = 0 := by simp [nim.nim_zero_equiv.symm]
 
 @[simp] lemma grundy_value_iff_equiv_zero (G : pgame) [G.impartial] : grundy_value G = 0 ↔ G ≈ 0 :=
 by rw [←grundy_value_eq_iff_equiv, grundy_value_zero]
 
-lemma grundy_value_star : grundy_value star = 1 := by simp [equiv_symm nim.nim_one_equiv]
+lemma grundy_value_star : grundy_value star = 1 := by simp [nim.nim_one_equiv.symm]
 
 @[simp] lemma grundy_value_nim_add_nim (n m : ℕ) :
   grundy_value (nim.{u} n + nim.{u} m) = nat.lxor n m :=
@@ -343,7 +343,7 @@ lemma grundy_value_add (G H : pgame) [G.impartial] [H.impartial] {n m : ℕ} (hG
   (hH : grundy_value H = m) : grundy_value (G + H) = nat.lxor n m :=
 begin
   rw [←nim.grundy_value (nat.lxor n m), grundy_value_eq_iff_equiv],
-  refine equiv_trans _ nim_add_nim_equiv,
+  refine equiv.trans _ nim_add_nim_equiv,
   convert add_congr (equiv_nim_grundy_value G) (equiv_nim_grundy_value H);
   simp only [hG, hH]
 end

src/set_theory/game/pgame.lean

@@ -319,6 +319,8 @@ end
 
 @[simp] protected theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y ⧏ x := not_le_lf.1
 @[simp] theorem not_lf {x y : pgame} : ¬ x ⧏ y ↔ y ≤ x := not_le_lf.2
+theorem _root_.has_le.le.not_lf {x y : pgame} : x ≤ y → ¬ y ⧏ x := not_lf.2
+theorem lf.not_le {x y : pgame} : x ⧏ y → ¬ y ≤ x := pgame.not_le.2
 
 theorem le_or_gf (x y : pgame) : x ≤ y ∨ y ⧏ x :=
 by { rw ←pgame.not_le, apply em }
@@ -358,8 +360,8 @@ private theorem le_trans_aux
   mk xl xr xL xR ≤ mk zl zr zL zR :=
 by simp only [mk_le_mk] at *; exact
 λ ⟨xLy, xyR⟩ ⟨yLz, yzR⟩, ⟨
-  λ i, pgame.not_le.1 (λ h, not_lf.2 (h₁ _ ⟨yLz, yzR⟩ h) (xLy _)),
-  λ i, pgame.not_le.1 (λ h, not_lf.2 (h₂ _ h ⟨xLy, xyR⟩) (yzR _))⟩
+  λ i, pgame.not_le.1 (λ h, (h₁ _ ⟨yLz, yzR⟩ h).not_lf (xLy _)),
+  λ i, pgame.not_le.1 (λ h, (h₂ _ h ⟨xLy, xyR⟩).not_lf (yzR _))⟩
 
 instance : preorder pgame :=
 { le_refl := λ x, begin
@@ -380,20 +382,25 @@ instance : preorder pgame :=
   end,
   ..pgame.has_le }
 
-theorem lf_irrefl (x : pgame) : ¬ x ⧏ x := pgame.not_lf.2 le_rfl
+theorem lf_irrefl (x : pgame) : ¬ x ⧏ x := le_rfl.not_lf
 instance : is_irrefl _ (⧏) := ⟨lf_irrefl⟩
 
 @[trans] theorem lf_of_le_of_lf {x y z : pgame} (h₁ : x ≤ y) (h₂ : y ⧏ z) : x ⧏ z :=
 by { rw ←pgame.not_le at h₂ ⊢, exact λ h₃, h₂ (h₃.trans h₁) }
-
 @[trans] theorem lf_of_lf_of_le {x y z : pgame} (h₁ : x ⧏ y) (h₂ : y ≤ z) : x ⧏ z :=
 by { rw ←pgame.not_le at h₁ ⊢, exact λ h₃, h₁ (h₂.trans h₃) }
 
+alias lf_of_le_of_lf ← has_le.le.trans_lf
+alias lf_of_lf_of_le ← pgame.lf.trans_le
+
 @[trans] theorem lf_of_lt_of_lf {x y z : pgame} (h₁ : x < y) (h₂ : y ⧏ z) : x ⧏ z :=
-lf_of_le_of_lf h₁.le h₂
+h₁.le.trans_lf h₂
 
 @[trans] theorem lf_of_lf_of_lt {x y z : pgame} (h₁ : x ⧏ y) (h₂ : y < z) : x ⧏ z :=
-lf_of_lf_of_le h₁ h₂.le
+h₁.trans_le h₂.le
+
+alias lf_of_lt_of_lf ← has_lt.lt.trans_lf
+alias lf_of_lf_of_lt ← pgame.lf.trans_lt
 
 theorem move_left_lf {x : pgame} (i) : x.move_left i ⧏ x :=
 move_left_lf_of_le i le_rfl
@@ -413,8 +420,8 @@ by rw [lt_iff_le_not_le, pgame.not_le]
 theorem lt_of_le_of_lf {x y : pgame} (h₁ : x ≤ y) (h₂ : x ⧏ y) : x < y :=
 lt_iff_le_and_lf.2 ⟨h₁, h₂⟩
 
-theorem lf_of_lt {x y : pgame} (h : x < y) : x ⧏ y :=
-(lt_iff_le_and_lf.1 h).2
+theorem lf_of_lt {x y : pgame} (h : x < y) : x ⧏ y := (lt_iff_le_and_lf.1 h).2
+alias lf_of_lt ← has_lt.lt.lf
 
 /-- The definition of `x ≤ y` on pre-games, in terms of `≤` two moves later. -/
 theorem le_def {x y : pgame} : x ≤ y ↔
@@ -500,21 +507,31 @@ def equiv (x y : pgame) : Prop := x ≤ y ∧ y ≤ x
 
 local infix ` ≈ ` := pgame.equiv
 
-@[refl, simp] theorem equiv_rfl {x} : x ≈ x := ⟨le_rfl, le_rfl⟩
-theorem equiv_refl (x) : x ≈ x := equiv_rfl
+instance : is_equiv _ (≈) :=
+{ refl := λ x, ⟨le_rfl, le_rfl⟩,
+  trans := λ x y z ⟨xy, yx⟩ ⟨yz, zy⟩, ⟨xy.trans yz, zy.trans yx⟩,
+  symm := λ x y, and.symm }
+
+theorem equiv.le {x y : pgame} (h : x ≈ y) : x ≤ y := h.1
+theorem equiv.ge {x y : pgame} (h : x ≈ y) : y ≤ x := h.2
 
--- TODO: use dot notation on these.
-@[symm] theorem equiv_symm {x y} : x ≈ y → y ≈ x | ⟨xy, yx⟩ := ⟨yx, xy⟩
-@[trans] theorem equiv_trans {x y z} : x ≈ y → y ≈ z → x ≈ z
-| ⟨xy, yx⟩ ⟨yz, zy⟩ := ⟨le_trans xy yz, le_trans zy yx⟩
+@[refl, simp] theorem equiv_rfl {x} : x ≈ x := refl x
+theorem equiv_refl (x) : x ≈ x := refl x
+@[symm] protected theorem equiv.symm {x y} : x ≈ y → y ≈ x := symm
+@[trans] protected theorem equiv.trans {x y z} : x ≈ y → y ≈ z → x ≈ z := trans
 
 @[trans] theorem le_of_le_of_equiv {x y z} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := h₁.trans h₂.1
 @[trans] theorem le_of_equiv_of_le {x y z} (h₁ : x ≈ y) : y ≤ z → x ≤ z := h₁.1.trans
 
+theorem lf.not_equiv {x y} (h : x ⧏ y) : ¬ x ≈ y := λ h', h.not_le h'.2
+theorem lf.not_equiv' {x y} (h : x ⧏ y) : ¬ y ≈ x := λ h', h.not_le h'.1
+
+theorem lf.not_lt {x y} (h : x ⧏ y) : ¬ y < x := λ h', h.not_le h'.le
+
 theorem le_congr_imp {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ ≤ y₁) : x₂ ≤ y₂ :=
 hx.2.trans (h.trans hy.1)
 theorem le_congr {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ ≤ y₁ ↔ x₂ ≤ y₂ :=
-⟨le_congr_imp hx hy, le_congr_imp (equiv_symm hx) (equiv_symm hy)⟩
+⟨le_congr_imp hx hy, le_congr_imp hx.symm hy.symm⟩
 theorem le_congr_left {x₁ x₂ y} (hx : x₁ ≈ x₂) : x₁ ≤ y ↔ x₂ ≤ y :=
 le_congr hx equiv_rfl
 theorem le_congr_right {x y₁ y₂} (hy : y₁ ≈ y₂) : x ≤ y₁ ↔ x ≤ y₂ :=
@@ -532,15 +549,15 @@ lf_congr equiv_rfl hy
 @[trans] theorem lf_of_lf_of_equiv {x y z} (h₁ : x ⧏ y) (h₂ : y ≈ z) : x ⧏ z :=
 lf_congr_imp equiv_rfl h₂ h₁
 @[trans] theorem lf_of_equiv_of_lf {x y z} (h₁ : x ≈ y) : y ⧏ z → x ⧏ z :=
-lf_congr_imp (equiv_symm h₁) equiv_rfl
+lf_congr_imp h₁.symm equiv_rfl
 
 @[trans] theorem lt_of_lt_of_equiv {x y z} (h₁ : x < y) (h₂ : y ≈ z) : x < z := h₁.trans_le h₂.1
 @[trans] theorem lt_of_equiv_of_lt {x y z} (h₁ : x ≈ y) : y < z → x < z := h₁.1.trans_lt
 
 theorem lt_congr_imp {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ < y₁) : x₂ < y₂ :=
 hx.2.trans_lt (h.trans_le hy.1)
 theorem lt_congr {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ < y₁ ↔ x₂ < y₂ :=
-⟨lt_congr_imp hx hy, lt_congr_imp (equiv_symm hx) (equiv_symm hy)⟩
+⟨lt_congr_imp hx hy, lt_congr_imp hx.symm hy.symm⟩
 theorem lt_congr_left {x₁ x₂ y} (hx : x₁ ≈ x₂) : x₁ < y ↔ x₂ < y :=
 lt_congr hx equiv_rfl
 theorem lt_congr_right {x y₁ y₂} (hy : y₁ ≈ y₂) : x < y₁ ↔ x < y₂ :=
@@ -556,16 +573,16 @@ begin
   { right,
     cases (lf_or_equiv_of_le (pgame.not_lf.1 h)) with h' h',
     { exact or.inr h' },
-    { exact or.inl (equiv_symm h') } }
+    { exact or.inl h'.symm } }
 end
 
 theorem equiv_congr_left {y₁ y₂} : y₁ ≈ y₂ ↔ ∀ x₁, x₁ ≈ y₁ ↔ x₁ ≈ y₂ :=
-⟨λ h x₁, ⟨λ h', equiv_trans h' h, λ h', equiv_trans h' (equiv_symm h)⟩,
+⟨λ h x₁, ⟨λ h', h'.trans h, λ h', h'.trans h.symm⟩,
  λ h, (h y₁).1 $ equiv_rfl⟩
 
 theorem equiv_congr_right {x₁ x₂} : x₁ ≈ x₂ ↔ ∀ y₁, x₁ ≈ y₁ ↔ x₂ ≈ y₁ :=
-⟨λ h y₁, ⟨λ h', equiv_trans (equiv_symm h) h', λ h', equiv_trans h h'⟩,
- λ h, (h x₂).2 $ equiv_refl _⟩
+⟨λ h y₁, ⟨λ h', h.symm.trans h', λ h', h.trans h'⟩,
+ λ h, (h x₂).2 $ equiv_rfl⟩
 
 theorem equiv_of_mk_equiv {x y : pgame}
   (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves)
@@ -605,21 +622,21 @@ instance : is_irrefl _ (∥) := ⟨fuzzy_irrefl⟩
 theorem lf_iff_lt_or_fuzzy {x y : pgame} : x ⧏ y ↔ x < y ∨ x ∥ y :=
 by { simp only [lt_iff_le_and_lf, fuzzy, ←pgame.not_le], tauto! }
 
-theorem lf_of_fuzzy {x y : pgame} (h : x ∥ y) : x ⧏ y :=
-lf_iff_lt_or_fuzzy.2 (or.inr h)
+theorem lf_of_fuzzy {x y : pgame} (h : x ∥ y) : x ⧏ y := lf_iff_lt_or_fuzzy.2 (or.inr h)
+alias lf_of_fuzzy ← pgame.fuzzy.lf
 
 theorem lt_or_fuzzy_of_lf {x y : pgame} : x ⧏ y → x < y ∨ x ∥ y :=
 lf_iff_lt_or_fuzzy.1
 
 theorem fuzzy.not_equiv {x y : pgame} (h : x ∥ y) : ¬ x ≈ y :=
-λ h', not_lf.2 h'.1 h.2
+λ h', h'.1.not_lf h.2
 theorem fuzzy.not_equiv' {x y : pgame} (h : x ∥ y) : ¬ y ≈ x :=
-λ h', not_lf.2 h'.2 h.2
+λ h', h'.2.not_lf h.2
 
 theorem not_fuzzy_of_le {x y : pgame} (h : x ≤ y) : ¬ x ∥ y :=
-λ h', pgame.not_le.2 h'.2 h
+λ h', h'.2.not_le h
 theorem not_fuzzy_of_ge {x y : pgame} (h : y ≤ x) : ¬ x ∥ y :=
-λ h', pgame.not_le.2 h'.1 h
+λ h', h'.1.not_le h
 
 theorem equiv.not_fuzzy {x y : pgame} (h : x ≈ y) : ¬ x ∥ y :=
 not_fuzzy_of_le h.1
@@ -1298,7 +1315,7 @@ theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x :=
      ... ≤ y : (add_zero_relabelling y).le⟩
 
 theorem lf_iff_sub_zero_lf {x y : pgame} : x ⧏ y ↔ 0 ⧏ y - x :=
-⟨λ h, lf_of_le_of_lf (zero_le_add_right_neg x) (add_lf_add_right h _),
+⟨λ h, (zero_le_add_right_neg x).trans_lf (add_lf_add_right h _),
  λ h,
   calc x ≤ 0 + x : (zero_add_relabelling x).symm.le
      ... ⧏ y - x + x : add_lf_add_right h _
@@ -1337,10 +1354,10 @@ by simp [star]
 lt_of_le_of_lf (zero_le_of_is_empty_right_moves 1) (zero_lf_le.2 ⟨default, le_rfl⟩)
 
 @[simp] theorem zero_le_one : (0 : pgame) ≤ 1 :=
-le_of_lt zero_lt_one
+zero_lt_one.le
 
 @[simp] theorem zero_lf_one : (0 : pgame) ⧏ 1 :=
-lf_of_lt zero_lt_one
+zero_lt_one.lf
 
 /-- The pre-game `half` is defined as `{0 | 1}`. -/
 def half : pgame := ⟨punit, punit, 0, 1⟩
@@ -1357,6 +1374,9 @@ protected theorem zero_lt_half : 0 < half :=
 lt_of_le_of_lf (zero_le.2 (λ j, ⟨punit.star, le_rfl⟩))
   (zero_lf.2 ⟨default, is_empty.elim pempty.is_empty⟩)
 
+protected theorem zero_le_half : 0 ≤ half :=
+pgame.zero_lt_half.le
+
 theorem half_lt_one : half < 1 :=
 lt_of_le_of_lf
   (le_of_forall_lf ⟨by simp, is_empty_elim⟩) (lf_of_forall_le (or.inr ⟨default, le_rfl⟩))
@@ -1365,27 +1385,11 @@ theorem half_add_half_equiv_one : half + half ≈ 1 :=
 begin
   split; rw le_def; split,
   { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩),
-    { right,
-      use (sum.inr punit.star),
-      calc ((half + half).move_left (sum.inl punit.star)).move_right (sum.inr punit.star)
-          = (half.move_left punit.star + half).move_right (sum.inr punit.star) : by fsplit
-      ... = (0 + half).move_right (sum.inr punit.star) : by fsplit
-      ... ≈ 1 : zero_add_equiv 1
-      ... ≤ 1 : le_rfl },
-    { right,
-      use (sum.inl punit.star),
-      calc ((half + half).move_left (sum.inr punit.star)).move_right (sum.inl punit.star)
-          = (half + half.move_left punit.star).move_right (sum.inl punit.star) : by fsplit
-      ... = (half + 0).move_right (sum.inl punit.star) : by fsplit
-      ... ≈ 1 : add_zero_equiv 1
-      ... ≤ 1 : le_rfl } },
+    { exact or.inr ⟨sum.inr punit.star, (le_congr_left (zero_add_equiv 1)).2 le_rfl⟩ },
+    { exact or.inr ⟨sum.inl punit.star, (le_congr_left (add_zero_equiv 1)).2 le_rfl⟩ } },
   { rintro ⟨ ⟩ },
   { rintro ⟨ ⟩,
-    left,
-    use (sum.inl punit.star),
-    calc 0 ≤ half : pgame.zero_lt_half.le
-    ... ≈ 0 + half : equiv_symm (zero_add_equiv half)
-    ... = (half + half).move_left (sum.inl punit.star) : by fsplit },
+    exact or.inl ⟨sum.inl punit.star, (le_congr_right (zero_add_equiv _)).2 pgame.zero_le_half⟩ },
   { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩); left,
     { exact ⟨sum.inr punit.star, (add_zero_equiv _).2⟩ },
     { exact ⟨sum.inl punit.star, (zero_add_equiv _).2⟩ } }

src/set_theory/game/winner.lean

@@ -42,7 +42,7 @@ lt_or_equiv_or_gt_or_fuzzy G 0
 lemma first_loses_is_zero {G : pgame} : G.first_loses ↔ G ≈ 0 := by refl
 
 lemma first_loses_of_equiv {G H : pgame} (h : G ≈ H) : G.first_loses → H.first_loses :=
-equiv_trans $ equiv_symm h
+h.symm.trans
 lemma first_wins_of_equiv {G H : pgame} (h : G ≈ H) : G.first_wins → H.first_wins :=
 (fuzzy_congr_left h).1
 lemma left_wins_of_equiv {G H : pgame} (h : G ≈ H) : G.left_wins → H.left_wins :=
@@ -51,7 +51,7 @@ lemma right_wins_of_equiv {G H : pgame} (h : G ≈ H) : G.right_wins → H.right
 (lt_congr_left h).1
 
 lemma first_loses_of_equiv_iff {G H : pgame} (h : G ≈ H) : G.first_loses ↔ H.first_loses :=
-⟨first_loses_of_equiv h, equiv_trans h⟩
+⟨first_loses_of_equiv h, h.trans⟩
 lemma first_wins_of_equiv_iff {G H : pgame} : G ≈ H → (G.first_wins ↔ H.first_wins) :=
 fuzzy_congr_left
 lemma left_wins_of_equiv_iff {G H : pgame} : G ≈ H → (G.left_wins ↔ H.left_wins) :=