feat(set_theory/game/pgame): make lt_iff_le_and_lf true by def-eq (#…

…14983)

src/set_theory/game/basic.lean

@@ -57,10 +57,12 @@ instance : add_comm_group_with_one game :=
 instance : inhabited game := ⟨0⟩
 
 instance : partial_order game :=
-{ le := quotient.lift₂ (λ x y, x ≤ y) (λ x₁ y₁ x₂ y₂ hx hy, propext (le_congr hx hy)),
+{ le := quotient.lift₂ (≤) (λ x₁ y₁ x₂ y₂ hx hy, propext (le_congr hx hy)),
   le_refl := by { rintro ⟨x⟩, exact le_refl x },
   le_trans := by { rintro ⟨x⟩ ⟨y⟩ ⟨z⟩, exact @le_trans _ _ x y z },
-  le_antisymm := by { rintro ⟨x⟩ ⟨y⟩ h₁ h₂, apply quot.sound, exact ⟨h₁, h₂⟩ } }
+  le_antisymm := by { rintro ⟨x⟩ ⟨y⟩ h₁ h₂, apply quot.sound, exact ⟨h₁, h₂⟩ },
+  lt := quotient.lift₂ (<) (λ x₁ y₁ x₂ y₂ hx hy, propext (lt_congr hx hy)),
+  lt_iff_le_not_le := by { rintro ⟨x⟩ ⟨y⟩, exact @lt_iff_le_not_le _ _ x y }, }
 
 /-- The less or fuzzy relation on games.
 

src/set_theory/game/ordinal.lean

@@ -83,7 +83,7 @@ begin
 end
 
 theorem to_pgame_lt {a b : ordinal} (h : a < b) : a.to_pgame < b.to_pgame :=
-lt_of_le_of_lf (to_pgame_le h.le) (to_pgame_lf h)
+⟨to_pgame_le h.le, to_pgame_lf h⟩ 
 
 @[simp] theorem to_pgame_lf_iff {a b : ordinal} : a.to_pgame ⧏ b.to_pgame ↔ a < b :=
 ⟨by { contrapose, rw [not_lt, not_lf], exact to_pgame_le }, to_pgame_lf⟩

src/set_theory/game/pgame.lean

@@ -358,6 +358,8 @@ by simp only [mk_le_mk] at *; exact
   λ 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 _))⟩
 
+instance : has_lt pgame := ⟨λ x y, x ≤ y ∧ x ⧏ y⟩
+
 instance : preorder pgame :=
 { le_refl := λ x, begin
     induction x with _ _ _ _ IHl IHr,
@@ -375,7 +377,14 @@ instance : preorder pgame :=
       le_trans_aux (λ i, (IHyl _).2.2) (λ i, (IHxr _).1),
       le_trans_aux (λ i, (IHzl _).1) (λ i, (IHyr _).2.1)⟩,
   end,
-  ..pgame.has_le }
+  lt_iff_le_not_le := λ x y, by { rw pgame.not_le, refl },
+  ..pgame.has_le, ..pgame.has_lt }
+
+theorem lt_iff_le_and_lf {x y : pgame} : x < y ↔ x ≤ y ∧ x ⧏ y := iff.rfl
+theorem lt_of_le_of_lf {x y : pgame} (h₁ : x ≤ y) (h₂ : x ⧏ y) : x < y := ⟨h₁, h₂⟩
+
+theorem lf_of_lt {x y : pgame} (h : x < y) : x ⧏ y := h.2
+alias lf_of_lt ← has_lt.lt.lf
 
 theorem lf_irrefl (x : pgame) : ¬ x ⧏ x := le_rfl.not_gf
 instance : is_irrefl _ (⧏) := ⟨lf_irrefl⟩
@@ -409,15 +418,6 @@ theorem lf_mk {xl xr} (xL : xl → pgame) (xR : xr → pgame) (i) : xL i ⧏ mk
 theorem mk_lf {xl xr} (xL : xl → pgame) (xR : xr → pgame) (j) : mk xl xr xL xR ⧏ xR j :=
 @lf_move_right (mk _ _ _ _) j
 
-theorem lt_iff_le_and_lf {x y : pgame} : x < y ↔ x ≤ y ∧ x ⧏ y :=
-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
-alias lf_of_lt ← has_lt.lt.lf
-
 /-- This special case of `pgame.le_of_forall_lf` is useful when dealing with surreals, where `<` is
 preferred over `⧏`. -/
 theorem le_of_forall_lt {x y : pgame} (h₁ : ∀ i, x.move_left i < y) (h₂ : ∀ j, x < y.move_right j) :
@@ -664,8 +664,8 @@ begin
   cases le_or_gf x y with h₁ h₁;
   cases le_or_gf y x with h₂ h₂,
   { right, left, exact ⟨h₁, h₂⟩ },
-  { left, exact lt_of_le_of_lf h₁ h₂ },
-  { right, right, left, exact lt_of_le_of_lf h₂ h₁ },
+  { left, exact ⟨h₁, h₂⟩ },
+  { right, right, left, exact ⟨h₂, h₁⟩ },
   { right, right, right, exact ⟨h₂, h₁⟩ }
 end
 
@@ -1258,16 +1258,10 @@ theorem add_lf_add_left {y z : pgame} (h : y ⧏ z) (x) : x + y ⧏ x + z :=
 by { rw lf_congr add_comm_equiv add_comm_equiv, apply add_lf_add_right h }
 
 instance covariant_class_swap_add_lt : covariant_class pgame pgame (swap (+)) (<) :=
-⟨λ x y z h, begin
-  rw lt_iff_le_and_lf at h ⊢,
-  exact ⟨add_le_add_right h.1 x, add_lf_add_right h.2 x⟩
-end⟩
+⟨λ x y z h, ⟨add_le_add_right h.1 x, add_lf_add_right h.2 x⟩⟩
 
 instance covariant_class_add_lt : covariant_class pgame pgame (+) (<) :=
-⟨λ x y z h, begin
-  rw lt_iff_le_and_lf at h ⊢,
-  exact ⟨add_le_add_left h.1 x, add_lf_add_left h.2 x⟩
-end⟩
+⟨λ x y z h, ⟨add_le_add_left h.1 x, add_lf_add_left h.2 x⟩⟩
 
 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)

src/set_theory/game/short.lean

@@ -215,7 +215,7 @@ instance lf_decidable (x y : pgame.{u}) [short x] [short y] : decidable (x ⧏ y
 (le_lf_decidable x y).2
 
 instance lt_decidable (x y : pgame.{u}) [short x] [short y] : decidable (x < y) :=
-by { rw lt_iff_le_and_lf, exact and.decidable }
+and.decidable 
 
 instance equiv_decidable (x y : pgame.{u}) [short x] [short y] : decidable (x ≈ y) :=
 and.decidable

src/set_theory/surreal/basic.lean

@@ -298,7 +298,7 @@ instance : ordered_add_comm_group surreal :=
   lt                := (<),
   le_refl           := by { rintros ⟨_⟩, apply @le_rfl pgame },
   le_trans          := by { rintros ⟨_⟩ ⟨_⟩ ⟨_⟩, apply @le_trans pgame },
-  lt_iff_le_not_le  := by { rintros ⟨_, ox⟩ ⟨_, oy⟩, exact lt_iff_le_not_le },
+  lt_iff_le_not_le  := by { rintros ⟨_, ox⟩ ⟨_, oy⟩, apply @lt_iff_le_not_le pgame },
   le_antisymm       := by { rintros ⟨_⟩ ⟨_⟩ h₁ h₂, exact quotient.sound ⟨h₁, h₂⟩ },
   add_le_add_left   := by { rintros ⟨_⟩ ⟨_⟩ hx ⟨_⟩, exact @add_le_add_left pgame _ _ _ _ _ hx _ } }