refactor(set_theory/game/pgame): Rename le_def_lf → `le_iff_forall_…

…lf` (#14206)

One-sided variants of these have also been introduced.

src/set_theory/game/impartial.lean

@@ -180,10 +180,10 @@ lemma no_good_left_moves_iff_first_loses (G : pgame) [G.impartial] :
   (∀ (i : G.left_moves), (G.move_left i).first_wins) ↔ G.first_loses :=
 begin
   refine ⟨λ hb, _, λ hp i, _⟩,
-  { rw [first_loses_symm G, le_def_lf],
+  { rw [first_loses_symm G, le_iff_forall_lf],
     exact ⟨λ i, (hb i).1, is_empty_elim⟩ },
   { rw first_wins_symm,
-    exact (le_def_lf.1 $ (first_loses_symm G).1 hp).1 i }
+    exact (le_iff_forall_lf.1 $ (first_loses_symm G).1 hp).1 i }
 end
 
 lemma no_good_right_moves_iff_first_loses (G : pgame) [G.impartial] :
@@ -202,8 +202,8 @@ end
 lemma good_left_move_iff_first_wins (G : pgame) [G.impartial] :
   (∃ (i : G.left_moves), (G.move_left i).first_loses) ↔ G.first_wins :=
 begin
-  refine ⟨λ ⟨i, hi⟩, (first_wins_symm' G).2 (lf_def_le.2 $ or.inl ⟨i, hi.2⟩), λ hn, _⟩,
-  rw [first_wins_symm' G, lf_def_le] at hn,
+  refine ⟨λ ⟨i, hi⟩, (first_wins_symm' G).2 (lf_of_forall_le $ or.inl ⟨i, hi.2⟩), λ hn, _⟩,
+  rw [first_wins_symm' G, lf_iff_forall_le] at hn,
   rcases hn with ⟨i, hi⟩ | ⟨j, _⟩,
   { exact ⟨i, (first_loses_symm' _).2 hi⟩ },
   { exact pempty.elim j }
@@ -212,8 +212,8 @@ end
 lemma good_right_move_iff_first_wins (G : pgame) [G.impartial] :
   (∃ j : G.right_moves, (G.move_right j).first_loses) ↔ G.first_wins :=
 begin
-  refine ⟨λ ⟨j, hj⟩, (first_wins_symm G).2 (lf_def_le.2 $ or.inr ⟨j, hj.1⟩), λ hn, _⟩,
-  rw [first_wins_symm G, lf_def_le] at hn,
+  refine ⟨λ ⟨j, hj⟩, (first_wins_symm G).2 (lf_of_forall_le $ or.inr ⟨j, hj.1⟩), λ hn, _⟩,
+  rw [first_wins_symm G, lf_iff_forall_le] at hn,
   rcases hn with ⟨i, _⟩ | ⟨j, hj⟩,
   { exact pempty.elim i },
   { exact ⟨j, (first_loses_symm _).2 hj⟩ }

src/set_theory/game/nim.lean

@@ -165,7 +165,7 @@ equiv.is_empty _
 
 lemma non_zero_first_wins {O : ordinal} (hO : O ≠ 0) : (nim O).first_wins :=
 begin
-  rw [impartial.first_wins_symm, nim_def, lf_def_le],
+  rw [impartial.first_wins_symm, nim_def, lf_iff_forall_le],
   rw ←ordinal.pos_iff_ne_zero at hO,
   exact or.inr ⟨(ordinal.principal_seg_out hO).top, by simp⟩
 end
@@ -179,7 +179,7 @@ begin
     wlog h' : O₁ ≤ O₂ using [O₁ O₂, O₂ O₁],
     { exact le_total O₁ O₂ },
     { have h : O₁ < O₂ := lt_of_le_of_ne h' h,
-      rw [impartial.first_wins_symm', lf_def_le, nim_def O₂],
+      rw [impartial.first_wins_symm', lf_iff_forall_le, nim_def O₂],
       refine or.inl ⟨(left_moves_add (nim O₁) _).symm (sum.inr _), _⟩,
       { exact (ordinal.principal_seg_out h).top },
       { simpa using (impartial.add_self (nim O₁)).2 } },

src/set_theory/game/pgame.lean

@@ -284,19 +284,29 @@ local infix ` ⧏ `:50 := lf
 show (le_lf _ _).1 ↔ _, by { rw le_lf, refl }
 
 /-- Definition of `x ≤ y` on pre-games, in terms of `⧏` -/
-theorem le_def_lf {x y : pgame} : x ≤ y ↔ (∀ i, x.move_left i ⧏ y) ∧ ∀ j, x ⧏ y.move_right j :=
+theorem le_iff_forall_lf {x y : pgame} :
+  x ≤ y ↔ (∀ i, x.move_left i ⧏ y) ∧ ∀ j, x ⧏ y.move_right j :=
 by { cases x, cases y, exact mk_le_mk }
 
+theorem le_of_forall_lf {x y : pgame} :
+  ((∀ i, x.move_left i ⧏ y) ∧ ∀ j, x ⧏ y.move_right j) → x ≤ y :=
+le_iff_forall_lf.2
+
 /-- Definition of `x ⧏ y` on pre-games built using the constructor. -/
 @[simp] theorem mk_lf_mk {xl xr xL xR yl yr yL yR} :
   mk xl xr xL xR ⧏ mk yl yr yL yR ↔
   (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR :=
 show (le_lf _ _).2 ↔ _, by { rw le_lf, refl }
 
 /-- Definition of `x ⧏ y` on pre-games, in terms of `≤` -/
-theorem lf_def_le {x y : pgame} : x ⧏ y ↔ (∃ i, x ≤ y.move_left i) ∨ ∃ j, x.move_right j ≤ y :=
+theorem lf_iff_forall_le {x y : pgame} :
+  x ⧏ y ↔ (∃ i, x ≤ y.move_left i) ∨ ∃ j, x.move_right j ≤ y :=
 by { cases x, cases y, exact mk_lf_mk }
 
+theorem lf_of_forall_le {x y : pgame} :
+  ((∃ i, x ≤ y.move_left i) ∨ ∃ j, x.move_right j ≤ y) → x ⧏ y :=
+lf_iff_forall_le.2
+
 private theorem not_le_lf {x y : pgame} :
   (¬ x ≤ y ↔ y ⧏ x) ∧ (¬ x ⧏ y ↔ y ≤ x) :=
 begin
@@ -354,7 +364,7 @@ by simp only [mk_le_mk] at *; exact
 instance : preorder pgame :=
 { le_refl := λ x, begin
     induction x with _ _ _ _ IHl IHr,
-    exact le_def_lf.2 ⟨λ i, lf_of_le_move_left (IHl i), λ i, lf_of_move_right_le (IHr i)⟩
+    exact le_of_forall_lf ⟨λ i, lf_of_le_move_left (IHl i), λ i, lf_of_move_right_le (IHr i)⟩
   end,
   le_trans := λ x y z, suffices ∀ {x y z : pgame},
     (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y),
@@ -410,29 +420,29 @@ theorem lf_of_lt {x y : pgame} (h : x < y) : x ⧏ y :=
 theorem le_def {x y : pgame} : x ≤ y ↔
   (∀ i, (∃ i', x.move_left i ≤ y.move_left i')  ∨ ∃ j, (x.move_left i).move_right j ≤ y) ∧
    ∀ j, (∃ i, x ≤ (y.move_right j).move_left i) ∨ ∃ j', x.move_right j' ≤ y.move_right j :=
-by { rw le_def_lf, conv { to_lhs, simp only [lf_def_le] } }
+by { rw le_iff_forall_lf, conv { to_lhs, simp only [lf_iff_forall_le] } }
 
 /-- The definition of `x ⧏ y` on pre-games, in terms of `⧏` two moves later. -/
 theorem lf_def {x y : pgame} : x ⧏ y ↔
   (∃ i, (∀ i', x.move_left i' ⧏ y.move_left i)  ∧ ∀ j, x ⧏ (y.move_left i).move_right j) ∨
    ∃ j, (∀ i, (x.move_right j).move_left i ⧏ y) ∧ ∀ j', x.move_right j ⧏ y.move_right j' :=
-by { rw lf_def_le, conv { to_lhs, simp only [le_def_lf] } }
+by { rw lf_iff_forall_le, conv { to_lhs, simp only [le_iff_forall_lf] } }
 
 /-- The definition of `0 ≤ x` on pre-games, in terms of `0 ⧏`. -/
 theorem zero_le_lf {x : pgame} : 0 ≤ x ↔ ∀ j, 0 ⧏ x.move_right j :=
-by { rw le_def_lf, dsimp, simp }
+by { rw le_iff_forall_lf, dsimp, simp }
 
 /-- The definition of `x ≤ 0` on pre-games, in terms of `⧏ 0`. -/
 theorem le_zero_lf {x : pgame} : x ≤ 0 ↔ ∀ i, x.move_left i ⧏ 0 :=
-by { rw le_def_lf, dsimp, simp }
+by { rw le_iff_forall_lf, dsimp, simp }
 
 /-- The definition of `0 ⧏ x` on pre-games, in terms of `0 ≤`. -/
 theorem zero_lf_le {x : pgame} : 0 ⧏ x ↔ ∃ i, 0 ≤ x.move_left i :=
-by { rw lf_def_le, dsimp, simp }
+by { rw lf_iff_forall_le, dsimp, simp }
 
 /-- The definition of `x ⧏ 0` on pre-games, in terms of `≤ 0`. -/
 theorem lf_zero_le {x : pgame} : x ⧏ 0 ↔ ∃ j, x.move_right j ≤ 0 :=
-by { rw lf_def_le, dsimp, simp }
+by { rw lf_iff_forall_le, dsimp, simp }
 
 /-- The definition of `0 ≤ x` on pre-games, in terms of `0 ≤` two moves later. -/
 theorem zero_le {x : pgame} : 0 ≤ x ↔ ∀ j, ∃ i, 0 ≤ (x.move_right j).move_left i :=
@@ -1320,7 +1330,8 @@ lt_of_le_of_lf (zero_le.2 (λ j, ⟨punit.star, le_rfl⟩))
   (zero_lf.2 ⟨default, is_empty.elim pempty.is_empty⟩)
 
 theorem half_lt_one : half < 1 :=
-lt_of_le_of_lf (le_def_lf.2 ⟨by simp, is_empty_elim⟩) (lf_def_le.2 (or.inr ⟨default, le_rfl⟩))
+lt_of_le_of_lf
+  (le_of_forall_lf ⟨by simp, is_empty_elim⟩) (lf_of_forall_le (or.inr ⟨default, le_rfl⟩))
 
 theorem half_add_half_equiv_one : half + half ≈ 1 :=
 begin

src/set_theory/surreal/basic.lean

@@ -129,7 +129,7 @@ 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_def_le at *,
+  rw lf_iff_forall_le at *,
   rcases hwx with ⟨ix, hix⟩|⟨jw, hjw⟩;
   rcases hyz with ⟨iz, hiz⟩|⟨jy, hjy⟩,
   { left,

src/set_theory/surreal/dyadic.lean

@@ -86,14 +86,14 @@ theorem add_pow_half_succ_self_eq_pow_half {n} : pow_half (n + 1) + pow_half (n
 begin
   induction n with n hn,
   { exact half_add_half_equiv_one },
-  { split; rw le_def_lf; split,
+  { split; rw le_iff_forall_lf; split,
     { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩); apply lf_of_lt,
       { calc 0 + pow_half (n.succ + 1) ≈ pow_half (n.succ + 1) : zero_add_equiv _
                                    ... < pow_half n.succ       : pow_half_succ_lt_pow_half },
       { calc pow_half (n.succ + 1) + 0 ≈ pow_half (n.succ + 1) : add_zero_equiv _
                                    ... < pow_half n.succ       : pow_half_succ_lt_pow_half } },
     { rintro ⟨ ⟩,
-      rw lf_def_le,
+      rw lf_iff_forall_le,
       right,
       use sum.inl punit.star,
       calc pow_half (n.succ) + pow_half (n.succ + 1)