feat(set_theory/game/pgame): golf le_trans (#14956)

This also adds `has_le.le.move_left_lf` and `has_le.le.lf_move_right` to enable dot notation. Note that we already have other pgame lemmas in the `has_le.le` namespace like `has_le.le.not_gf`.

To make this dot notation work even when these lemmas are partially-applied, we swap the arguments of `move_left_lf_of_le` and `lf_move_right_of_le`.

src/set_theory/game/impartial.lean

@@ -170,7 +170,7 @@ begin
   { rw [equiv_zero_iff_le G, le_zero_lf],
     exact λ i, (hb i).1 },
   { rw fuzzy_zero_iff_lf,
-    exact move_left_lf_of_le i hp.1 }
+    exact hp.1.move_left_lf i }
 end
 
 lemma forall_right_moves_fuzzy_iff_equiv_zero : (∀ j, G.move_right j ∥ 0) ↔ G ≈ 0 :=
@@ -179,7 +179,7 @@ begin
   { rw [equiv_zero_iff_ge G, zero_le_lf],
     exact λ i, (hb i).2 },
   { rw fuzzy_zero_iff_gf,
-    exact lf_move_right_of_le i hp.2 }
+    exact hp.2.lf_move_right i }
 end
 
 lemma exists_left_move_equiv_iff_fuzzy_zero : (∃ i, G.move_left i ≈ 0) ↔ G ∥ 0 :=

src/set_theory/game/pgame.lean

@@ -320,43 +320,43 @@ theorem lf.not_ge {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 }
 
-theorem move_left_lf_of_le {x y : pgame} (i) (h : x ≤ y) : x.move_left i ⧏ y :=
+theorem move_left_lf_of_le {x y : pgame} (h : x ≤ y) (i) : x.move_left i ⧏ y :=
 (le_iff_forall_lf.1 h).1 i
 
-theorem lf_move_right_of_le {x y : pgame} (j) (h : x ≤ y) : x ⧏ y.move_right j :=
+alias move_left_lf_of_le ← _root_.has_le.le.move_left_lf
+
+theorem lf_move_right_of_le {x y : pgame} (h : x ≤ y) (j) : x ⧏ y.move_right j :=
 (le_iff_forall_lf.1 h).2 j
 
+alias lf_move_right_of_le ← _root_.has_le.le.lf_move_right
+
 theorem lf_of_move_right_le {x y : pgame} {j} (h : x.move_right j ≤ y) : x ⧏ y :=
 lf_iff_exists_le.2 $ or.inr ⟨j, h⟩
 
 theorem lf_of_le_move_left {x y : pgame} {i} (h : x ≤ y.move_left i) : x ⧏ y :=
 lf_iff_exists_le.2 $ or.inl ⟨i, h⟩
 
-theorem lf_of_le_mk {xl xr xL xR y} : ∀ i, mk xl xr xL xR ≤ y → xL i ⧏ y :=
-@move_left_lf_of_le (mk _ _ _ _) y
+theorem lf_of_le_mk {xl xr xL xR y} : mk xl xr xL xR ≤ y → ∀ i, xL i ⧏ y :=
+move_left_lf_of_le
 
-theorem lf_of_mk_le {x yl yr yL yR} : ∀ j, x ≤ mk yl yr yL yR → x ⧏ yR j :=
-@lf_move_right_of_le x (mk _ _ _ _)
+theorem lf_of_mk_le {x yl yr yL yR} : x ≤ mk yl yr yL yR → ∀ j, x ⧏ yR j :=
+lf_move_right_of_le
 
 theorem mk_lf_of_le {xl xr y j} (xL) {xR : xr → pgame} : xR j ≤ y → mk xl xr xL xR ⧏ y :=
 @lf_of_move_right_le (mk _ _ _ _) y j
 
 theorem lf_mk_of_le {x yl yr} {yL : yl → pgame} (yR) {i} : x ≤ yL i → x ⧏ mk yl yr yL yR :=
 @lf_of_le_move_left x (mk _ _ _ _) i
 
-private theorem le_trans_aux
-  {xl xr} {xL : xl → pgame} {xR : xr → pgame}
-  {yl yr} {yL : yl → pgame} {yR : yr → pgame}
-  {zl zr} {zL : zl → pgame} {zR : zr → pgame}
-  (h₁ : ∀ i, mk yl yr yL yR ≤ mk zl zr zL zR → mk zl zr zL zR ≤ xL i → mk yl yr yL yR ≤ xL i)
-  (h₂ : ∀ i, zR i ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → zR i ≤ mk yl yr yL yR) :
-  mk xl xr xL xR ≤ mk yl yr yL yR →
-  mk yl yr yL yR ≤ mk zl zr zL zR →
-  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, (h₁ _ ⟨yLz, yzR⟩ h).not_gf (xLy _)),
-  λ i, pgame.not_le.1 (λ h, (h₂ _ h ⟨xLy, xyR⟩).not_gf (yzR _))⟩
+/- We prove that `x ≤ y → y ≤ z ← x ≤ z` inductively, by also simultaneously proving its cyclic
+reorderings. This auxiliary lemma is used during said induction. -/
+private theorem le_trans_aux {x y z : pgame}
+  (h₁ : ∀ {i}, y ≤ z → z ≤ x.move_left i → y ≤ x.move_left i)
+  (h₂ : ∀ {j}, z.move_right j ≤ x → x ≤ y → z.move_right j ≤ y)
+  (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z :=
+le_of_forall_lf
+  (λ i, pgame.not_le.1 $ λ h, (h₁ hyz h).not_gf $ hxy.move_left_lf i)
+  (λ j, pgame.not_le.1 $ λ h, (h₂ h hxy).not_gf $ hyz.lf_move_right j)
 
 instance : has_lt pgame := ⟨λ x y, x ≤ y ∧ x ⧏ y⟩
 
@@ -365,17 +365,17 @@ instance : preorder pgame :=
     induction x with _ _ _ _ IHl IHr,
     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),
-  from this.1, begin
-    clear x y z, intros,
+  le_trans := begin
+    suffices : ∀ {x y z : pgame},
+      (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y),
+      from λ x y z, this.1,
+    intros x y z,
     induction x with xl xr xL xR IHxl IHxr generalizing y z,
     induction y with yl yr yL yR IHyl IHyr generalizing z,
     induction z with zl zr zL zR IHzl IHzr,
-    exact ⟨
-      le_trans_aux (λ i, (IHxl _).2.1) (λ i, (IHzr _).2.2),
-      le_trans_aux (λ i, (IHyl _).2.2) (λ i, (IHxr _).1),
-      le_trans_aux (λ i, (IHzl _).1) (λ i, (IHyr _).2.1)⟩,
+    exact ⟨le_trans_aux (λ i, (IHxl i).2.1) (λ j, (IHzr j).2.2),
+      le_trans_aux (λ i, (IHyl i).2.2) (λ j, (IHxr j).1),
+      le_trans_aux (λ i, (IHzl i).1) (λ j, (IHyr j).2.1)⟩
   end,
   lt_iff_le_not_le := λ x y, by { rw pgame.not_le, refl },
   ..pgame.has_le, ..pgame.has_lt }
@@ -406,11 +406,11 @@ h₁.trans_le h₂.le
 alias lf_of_lt_of_lf ← _root_.has_lt.lt.trans_lf
 alias lf_of_lf_of_lt ← lf.trans_lt
 
-theorem move_left_lf {x : pgame} (i) : x.move_left i ⧏ x :=
-move_left_lf_of_le i le_rfl
+theorem move_left_lf {x : pgame} : ∀ i, x.move_left i ⧏ x :=
+le_rfl.move_left_lf
 
-theorem lf_move_right {x : pgame} (j) : x ⧏ x.move_right j :=
-lf_move_right_of_le j le_rfl
+theorem lf_move_right {x : pgame} : ∀ j, x ⧏ x.move_right j :=
+le_rfl.lf_move_right
 
 theorem lf_mk {xl xr} (xL : xl → pgame) (xR : xr → pgame) (i) : xL i ⧏ mk xl xr xL xR :=
 @move_left_lf (mk _ _ _ _) i

src/set_theory/surreal/basic.lean

@@ -101,10 +101,10 @@ begin
   refine numeric_rec (λ xl xr xL xR hx oxl oxr IHxl IHxr, _) x ox y oy,
   refine numeric_rec (λ yl yr yL yR hy oyl oyr IHyl IHyr, _),
   rw [mk_lf_mk, mk_lf_mk], rintro (⟨i, h₁⟩ | ⟨j, h₁⟩) (⟨i, h₂⟩ | ⟨j, h₂⟩),
-  { exact IHxl _ _ (oyl _) (move_left_lf_of_le _ h₁) (move_left_lf_of_le _ h₂) },
+  { exact IHxl _ _ (oyl _) (h₁.move_left_lf _) (h₂.move_left_lf _) },
   { exact (le_trans h₂ h₁).not_gf (lf_of_lt (hy _ _)) },
   { exact (le_trans h₁ h₂).not_gf (lf_of_lt (hx _ _)) },
-  { exact IHxr _ _ (oyr _) (lf_move_right_of_le _ h₁) (lf_move_right_of_le _ h₂) },
+  { exact IHxr _ _ (oyr _) (h₁.lf_move_right _) (h₂.lf_move_right _) },
 end
 
 theorem le_of_lf {x y : pgame} (h : x ⧏ y) (ox : numeric x) (oy : numeric y) : x ≤ y :=