From 424d2cc41a0d37bab5550275213067762c3f06d5 Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Wed, 25 Sep 2024 10:59:28 +0800 Subject: [PATCH 1/7] =?UTF-8?q?feat:=20define=20`PGame.identical`=20`PGame?= =?UTF-8?q?.mem=E2=82=97`=20`PGame.mem=E1=B5=A3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/SetTheory/Game/PGame.lean | 164 +++++++++++++++++++++++++++++- 1 file changed, 160 insertions(+), 4 deletions(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index 94f9ebf8cd866..232bf0ec746ee 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2019 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Kim Morrison +Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Kim Morrison, Yuyang Zhao -/ import Mathlib.Algebra.Order.ZeroLEOne import Mathlib.Data.List.InsertNth @@ -23,7 +23,8 @@ takes two types (thought of as indexing the possible moves for the players Left pair of functions out of these types to `SetTheory.PGame` (thought of as describing the resulting game after making a move). -Combinatorial games themselves, as a quotient of pregames, are constructed in `Game.lean`. +Combinatorial games themselves, as a quotient of pregames, are constructed in +`SetTheory.Game.Basic`. ## Conway induction @@ -344,6 +345,152 @@ instance uniqueOneLeftMoves : Unique (LeftMoves 1) := instance isEmpty_one_rightMoves : IsEmpty (RightMoves 1) := instIsEmptyPEmpty +/-! ### Identity -/ + +/-- Two pre-games are identical if their left and right sets are identical. +That is, `Identical x y` if every left move of `x` is identical to some left move of `y`, +every right move of `x` is identical to some right move of `y`, and vice versa. -/ +def Identical : ∀ (_ _ : PGame.{u}), Prop + | mk _ _ xL xR, mk _ _ yL yR => + Relator.BiTotal (fun i j ↦ Identical (xL i) (yL j)) ∧ + Relator.BiTotal (fun i j ↦ Identical (xR i) (yR j)) + +@[inherit_doc] scoped infix:50 " ≡ " => PGame.Identical + +/-- `x ∈ₗ y` if `x` is identical to some left move of `y`. -/ +def memₗ (x y : PGame.{u}) : Prop := ∃ b, x ≡ y.moveLeft b + +/-- `x ∈ᵣ y` if `x` is identical to some right move of `y`. -/ +def memᵣ (x y : PGame.{u}) : Prop := ∃ b, x ≡ y.moveRight b + +@[inherit_doc] scoped infix:50 " ∈ₗ " => PGame.memₗ +@[inherit_doc] scoped infix:50 " ∈ᵣ " => PGame.memᵣ +@[inherit_doc PGame.memₗ] binder_predicate x " ∈ₗ " y:term => `($x ∈ₗ $y) +@[inherit_doc PGame.memᵣ] binder_predicate x " ∈ᵣ " y:term => `($x ∈ᵣ $y) + +theorem identical_iff : ∀ {x y : PGame}, x ≡ y ↔ + Relator.BiTotal (x.moveLeft · ≡ y.moveLeft ·) ∧ Relator.BiTotal (x.moveRight · ≡ y.moveRight ·) + | mk _ _ _ _, mk _ _ _ _ => Iff.rfl + +@[refl, simp] protected theorem Identical.refl (x) : x ≡ x := + PGame.recOn x fun _ _ _ _ IHL IHR ↦ ⟨Relator.BiTotal.refl IHL, Relator.BiTotal.refl IHR⟩ + +protected theorem Identical.rfl {x} : x ≡ x := Identical.refl x + +@[symm] protected theorem Identical.symm : ∀ {x y}, x ≡ y → y ≡ x + | mk _ _ _ _, mk _ _ _ _, ⟨hL, hR⟩ => ⟨hL.symm fun _ _ h ↦ h.symm, hR.symm fun _ _ h ↦ h.symm⟩ + +theorem identical_comm {x y} : x ≡ y ↔ y ≡ x := + ⟨Identical.symm, Identical.symm⟩ + +@[trans] protected theorem Identical.trans : ∀ {x y z}, x ≡ y → y ≡ z → x ≡ z + | mk _ _ _ _, mk _ _ _ _, mk _ _ _ _, ⟨hL₁, hR₁⟩, ⟨hL₂, hR₂⟩ => + ⟨hL₁.trans (fun _ _ _ h₁ h₂ ↦ h₁.trans h₂) hL₂, hR₁.trans (fun _ _ _ h₁ h₂ ↦ h₁.trans h₂) hR₂⟩ + +theorem identical_of_is_empty (x y : PGame) + [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] + [IsEmpty y.LeftMoves] [IsEmpty y.RightMoves] : x ≡ y := + identical_iff.2 <| by simp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] + +/-- `Identical` as a `Setoid`. -/ +def identicalSetoid : Setoid PGame := + ⟨Identical, Identical.refl, Identical.symm, Identical.trans⟩ + +instance : IsRefl PGame (· ≡ ·) := ⟨Identical.refl⟩ +instance : IsSymm PGame (· ≡ ·) := ⟨fun _ _ ↦ Identical.symm⟩ +instance : IsTrans PGame (· ≡ ·) := ⟨fun _ _ _ ↦ Identical.trans⟩ +instance : IsEquiv PGame (· ≡ ·) := { } + +/-- If `x` and `y` are identical, then a left move of `x` is identical to some left move of `y`. -/ +lemma Identical.moveLeft : ∀ {x y}, x ≡ y → + ∀ i, ∃ j, x.moveLeft i ≡ y.moveLeft j + | mk _ _ _ _, mk _ _ _ _, ⟨hl, _⟩, i => hl.1 i + +/-- If `x` and `y` are identical, then a left move of `y` is identical to some left move of `x`. -/ +lemma Identical.moveLeft_symm : ∀ {x y}, x ≡ y → + ∀ i, ∃ j, x.moveLeft j ≡ y.moveLeft i + | mk _ _ _ _, mk _ _ _ _, ⟨hl, _⟩, i => hl.2 i + +/-- If `x` and `y` are identical, then a right move of `x` is identical to some right move of `y`. +-/ +lemma Identical.moveRight : ∀ {x y}, x ≡ y → + ∀ i, ∃ j, x.moveRight i ≡ y.moveRight j + | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.1 i + +/-- If `x` and `y` are identical, then a right move of `y` is identical to some right move of `x`. +-/ +lemma Identical.moveRight_symm : ∀ {x y}, x ≡ y → + ∀ i, ∃ j, x.moveRight j ≡ y.moveRight i + | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.2 i + +theorem identical_iff' : ∀ {x y : PGame}, x ≡ y ↔ + ((∀ i, x.moveLeft i ∈ₗ y) ∧ (∀ j, y.moveLeft j ∈ₗ x)) ∧ + ((∀ i, x.moveRight i ∈ᵣ y) ∧ (∀ j, y.moveRight j ∈ᵣ x)) + | mk xl xr xL xR, mk yl yr yL yR => by + convert identical_iff <;> + dsimp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] <;> + congr! <;> + exact exists_congr <| fun _ ↦ identical_comm + +theorem memₗ_def {x y : PGame} : x ∈ₗ y ↔ ∃ b, x ≡ y.moveLeft b := .rfl + +theorem memᵣ_def {x y : PGame} : x ∈ᵣ y ↔ ∃ b, x ≡ y.moveRight b := .rfl + +theorem moveLeft_memₗ (x : PGame) (b) : x.moveLeft b ∈ₗ x := ⟨_, .rfl⟩ + +theorem moveRight_memᵣ (x : PGame) (b) : x.moveRight b ∈ᵣ x := ⟨_, .rfl⟩ + +theorem memₗ.congr_right : ∀ {x y : PGame}, + x ≡ y → (∀ {w : PGame}, w ∈ₗ x ↔ w ∈ₗ y) + | mk _ _ _ _, mk _ _ _ _, ⟨⟨h₁, h₂⟩, _⟩, _w => + ⟨fun ⟨i, hi⟩ ↦ (h₁ i).imp (fun _ ↦ hi.trans), + fun ⟨j, hj⟩ ↦ (h₂ j).imp (fun _ hi ↦ hj.trans hi.symm)⟩ + +theorem memᵣ.congr_right : ∀ {x y : PGame}, + x ≡ y → (∀ {w : PGame}, w ∈ᵣ x ↔ w ∈ᵣ y) + | mk _ _ _ _, mk _ _ _ _, ⟨_, ⟨h₁, h₂⟩⟩, _w => + ⟨fun ⟨i, hi⟩ ↦ (h₁ i).imp (fun _ ↦ hi.trans), + fun ⟨j, hj⟩ ↦ (h₂ j).imp (fun _ hi ↦ hj.trans hi.symm)⟩ + +theorem memₗ.congr_left : ∀ {x y : PGame}, + x ≡ y → (∀ {w : PGame}, x ∈ₗ w ↔ y ∈ₗ w) + | _, _, h, mk _ _ _ _ => ⟨fun ⟨i, hi⟩ ↦ ⟨i, h.symm.trans hi⟩, fun ⟨i, hi⟩ ↦ ⟨i, h.trans hi⟩⟩ + +theorem memᵣ.congr_left : ∀ {x y : PGame}, + x ≡ y → (∀ {w : PGame}, x ∈ᵣ w ↔ y ∈ᵣ w) + | _, _, h, mk _ _ _ _ => ⟨fun ⟨i, hi⟩ ↦ ⟨i, h.symm.trans hi⟩, fun ⟨i, hi⟩ ↦ ⟨i, h.trans hi⟩⟩ + +lemma Identical.ext : ∀ {x y}, (∀ z, z ∈ₗ x ↔ z ∈ₗ y) → (∀ z, z ∈ᵣ x ↔ z ∈ᵣ y) → x ≡ y + | mk _ _ _ _, mk _ _ _ _, hl, hr => identical_iff'.mpr + ⟨⟨fun i ↦ (hl _).mp ⟨i, refl _⟩, fun j ↦ (hl _).mpr ⟨j, refl _⟩⟩, + ⟨fun i ↦ (hr _).mp ⟨i, refl _⟩, fun j ↦ (hr _).mpr ⟨j, refl _⟩⟩⟩ + +lemma Identical.ext_iff {x y} : x ≡ y ↔ (∀ z, z ∈ₗ x ↔ z ∈ₗ y) ∧ (∀ z, z ∈ᵣ x ↔ z ∈ᵣ y) := + ⟨fun h ↦ ⟨@memₗ.congr_right _ _ h, @memᵣ.congr_right _ _ h⟩, fun h ↦ h.elim Identical.ext⟩ + +lemma Identical.congr_right {x y z} (h : x ≡ y) : z ≡ x ↔ z ≡ y := + ⟨fun hz ↦ hz.trans h, fun hz ↦ hz.trans h.symm⟩ + +lemma Identical.congr_left {x y z} (h : x ≡ y) : x ≡ z ↔ y ≡ z := + ⟨fun hz ↦ h.symm.trans hz, fun hz ↦ h.trans hz⟩ + +/-- Show `x ≡ y` by giving an explicit correspondence between the moves of `x` and `y`. -/ +lemma Identical.of_fn {x y : PGame} + (l : x.LeftMoves → y.LeftMoves) (il : y.LeftMoves → x.LeftMoves) + (r : x.RightMoves → y.RightMoves) (ir : y.RightMoves → x.RightMoves) + (hl : ∀ i, x.moveLeft i ≡ y.moveLeft (l i)) + (hil : ∀ i, x.moveLeft (il i) ≡ y.moveLeft i) + (hr : ∀ i, x.moveRight i ≡ y.moveRight (r i)) + (hir : ∀ i, x.moveRight (ir i) ≡ y.moveRight i) : x ≡ y := + identical_iff.mpr + ⟨⟨fun i ↦ ⟨l i, hl i⟩, fun i ↦ ⟨il i, hil i⟩⟩, ⟨fun i ↦ ⟨r i, hr i⟩, fun i ↦ ⟨ir i, hir i⟩⟩⟩ + +lemma Identical.of_equiv {x y : PGame} + (l : x.LeftMoves ≃ y.LeftMoves) (r : x.RightMoves ≃ y.RightMoves) + (hl : ∀ i, x.moveLeft i ≡ y.moveLeft (l i)) (hr : ∀ i, x.moveRight i ≡ y.moveRight (r i)) : + x ≡ y := + .of_fn l l.symm r r.symm hl (by simpa using hl <| l.symm ·) hr (by simpa using hr <| r.symm ·) + /-! ### Pre-game order relations -/ @@ -373,7 +520,7 @@ theorem not_lf {x y : PGame} : ¬x ⧏ y ↔ y ≤ x := Classical.not_not theorem _root_.LE.le.not_gf {x y : PGame} : x ≤ y → ¬y ⧏ x := - not_lf.2 + absurd theorem LF.not_ge {x y : PGame} : x ⧏ y → ¬y ≤ x := id @@ -476,6 +623,13 @@ instance : Preorder PGame := le_trans_aux (fun {i} => (IHzl i).1) fun {j} => (IHyr j).2.1⟩ lt := fun x y => x ≤ y ∧ x ⧏ y } +lemma Identical.le : ∀ {x y}, x ≡ y → x ≤ y + | mk _ _ _ _, mk _ _ _ _, ⟨hL, hR⟩ => le_of_forall_lf + (fun i ↦ let ⟨_, hj⟩ := hL.1 i; lf_of_le_moveLeft hj.le) + (fun i ↦ let ⟨_, hj⟩ := hR.2 i; lf_of_moveRight_le hj.le) + +lemma Identical.ge {x y} (h : x ≡ y) : y ≤ x := h.symm.le + theorem lt_iff_le_and_lf {x y : PGame} : x < y ↔ x ≤ y ∧ x ⧏ y := Iff.rfl @@ -709,6 +863,8 @@ protected theorem equiv_comm {x y : PGame} : (x ≈ y) ↔ (y ≈ x) := theorem equiv_of_eq {x y : PGame} (h : x = y) : x ≈ y := by subst h; rfl +lemma Identical.equiv {x y} (h : x ≡ y) : x ≈ y := ⟨h.le, h.ge⟩ + @[trans] theorem le_of_le_of_equiv {x y z : PGame} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := h₁.trans h₂.1 @@ -1764,4 +1920,4 @@ end PGame end SetTheory -set_option linter.style.longFile 1900 +set_option linter.style.longFile 2300 From e4dc4dd5de2ac1857ec3a48781f90c0c5fbed0f1 Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Wed, 25 Sep 2024 11:01:26 +0800 Subject: [PATCH 2/7] Update PGame.lean --- Mathlib/SetTheory/Game/PGame.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index 232bf0ec746ee..f94cf200a1218 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -520,7 +520,7 @@ theorem not_lf {x y : PGame} : ¬x ⧏ y ↔ y ≤ x := Classical.not_not theorem _root_.LE.le.not_gf {x y : PGame} : x ≤ y → ¬y ⧏ x := - absurd + not_lf.2 theorem LF.not_ge {x y : PGame} : x ⧏ y → ¬y ≤ x := id From 4fde7201e400477db131b68d265380afb1b6c17c Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Thu, 26 Sep 2024 15:46:47 +0800 Subject: [PATCH 3/7] suggestions --- Mathlib/SetTheory/Game/PGame.lean | 38 +++++++++++++++---------------- 1 file changed, 18 insertions(+), 20 deletions(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index f94cf200a1218..83d154573a02f 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -350,24 +350,13 @@ instance isEmpty_one_rightMoves : IsEmpty (RightMoves 1) := /-- Two pre-games are identical if their left and right sets are identical. That is, `Identical x y` if every left move of `x` is identical to some left move of `y`, every right move of `x` is identical to some right move of `y`, and vice versa. -/ -def Identical : ∀ (_ _ : PGame.{u}), Prop +def Identical : ∀ _ _ : PGame.{u}, Prop | mk _ _ xL xR, mk _ _ yL yR => Relator.BiTotal (fun i j ↦ Identical (xL i) (yL j)) ∧ Relator.BiTotal (fun i j ↦ Identical (xR i) (yR j)) @[inherit_doc] scoped infix:50 " ≡ " => PGame.Identical -/-- `x ∈ₗ y` if `x` is identical to some left move of `y`. -/ -def memₗ (x y : PGame.{u}) : Prop := ∃ b, x ≡ y.moveLeft b - -/-- `x ∈ᵣ y` if `x` is identical to some right move of `y`. -/ -def memᵣ (x y : PGame.{u}) : Prop := ∃ b, x ≡ y.moveRight b - -@[inherit_doc] scoped infix:50 " ∈ₗ " => PGame.memₗ -@[inherit_doc] scoped infix:50 " ∈ᵣ " => PGame.memᵣ -@[inherit_doc PGame.memₗ] binder_predicate x " ∈ₗ " y:term => `($x ∈ₗ $y) -@[inherit_doc PGame.memᵣ] binder_predicate x " ∈ᵣ " y:term => `($x ∈ᵣ $y) - theorem identical_iff : ∀ {x y : PGame}, x ≡ y ↔ Relator.BiTotal (x.moveLeft · ≡ y.moveLeft ·) ∧ Relator.BiTotal (x.moveRight · ≡ y.moveRight ·) | mk _ _ _ _, mk _ _ _ _ => Iff.rfl @@ -387,6 +376,22 @@ theorem identical_comm {x y} : x ≡ y ↔ y ≡ x := | mk _ _ _ _, mk _ _ _ _, mk _ _ _ _, ⟨hL₁, hR₁⟩, ⟨hL₂, hR₂⟩ => ⟨hL₁.trans (fun _ _ _ h₁ h₂ ↦ h₁.trans h₂) hL₂, hR₁.trans (fun _ _ _ h₁ h₂ ↦ h₁.trans h₂) hR₂⟩ +/-- `x ∈ₗ y` if `x` is identical to some left move of `y`. -/ +def memₗ (x y : PGame.{u}) : Prop := ∃ b, x ≡ y.moveLeft b + +/-- `x ∈ᵣ y` if `x` is identical to some right move of `y`. -/ +def memᵣ (x y : PGame.{u}) : Prop := ∃ b, x ≡ y.moveRight b + +@[inherit_doc] scoped infix:50 " ∈ₗ " => PGame.memₗ +@[inherit_doc] scoped infix:50 " ∈ᵣ " => PGame.memᵣ +@[inherit_doc PGame.memₗ] binder_predicate x " ∈ₗ " y:term => `($x ∈ₗ $y) +@[inherit_doc PGame.memᵣ] binder_predicate x " ∈ᵣ " y:term => `($x ∈ᵣ $y) + +theorem memₗ_def {x y : PGame} : x ∈ₗ y ↔ ∃ b, x ≡ y.moveLeft b := .rfl +theorem memᵣ_def {x y : PGame} : x ∈ᵣ y ↔ ∃ b, x ≡ y.moveRight b := .rfl +theorem moveLeft_memₗ (x : PGame) (b) : x.moveLeft b ∈ₗ x := ⟨_, .rfl⟩ +theorem moveRight_memᵣ (x : PGame) (b) : x.moveRight b ∈ᵣ x := ⟨_, .rfl⟩ + theorem identical_of_is_empty (x y : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] [IsEmpty y.LeftMoves] [IsEmpty y.RightMoves] : x ≡ y := @@ -423,6 +428,7 @@ lemma Identical.moveRight_symm : ∀ {x y}, x ≡ y → ∀ i, ∃ j, x.moveRight j ≡ y.moveRight i | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.2 i +/-- Uses `∈ₗ` `∈ᵣ` instead of `≡`. -/ theorem identical_iff' : ∀ {x y : PGame}, x ≡ y ↔ ((∀ i, x.moveLeft i ∈ₗ y) ∧ (∀ j, y.moveLeft j ∈ₗ x)) ∧ ((∀ i, x.moveRight i ∈ᵣ y) ∧ (∀ j, y.moveRight j ∈ᵣ x)) @@ -432,14 +438,6 @@ theorem identical_iff' : ∀ {x y : PGame}, x ≡ y ↔ congr! <;> exact exists_congr <| fun _ ↦ identical_comm -theorem memₗ_def {x y : PGame} : x ∈ₗ y ↔ ∃ b, x ≡ y.moveLeft b := .rfl - -theorem memᵣ_def {x y : PGame} : x ∈ᵣ y ↔ ∃ b, x ≡ y.moveRight b := .rfl - -theorem moveLeft_memₗ (x : PGame) (b) : x.moveLeft b ∈ₗ x := ⟨_, .rfl⟩ - -theorem moveRight_memᵣ (x : PGame) (b) : x.moveRight b ∈ᵣ x := ⟨_, .rfl⟩ - theorem memₗ.congr_right : ∀ {x y : PGame}, x ≡ y → (∀ {w : PGame}, w ∈ₗ x ↔ w ∈ₗ y) | mk _ _ _ _, mk _ _ _ _, ⟨⟨h₁, h₂⟩, _⟩, _w => From b7674c7c7814c58f3dfb318ba0bbec4a14f1fe84 Mon Sep 17 00:00:00 2001 From: FR Date: Thu, 26 Sep 2024 20:01:27 +0800 Subject: [PATCH 4/7] suggestion MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández --- Mathlib/SetTheory/Game/PGame.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index 83d154573a02f..20796603c534d 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -428,7 +428,7 @@ lemma Identical.moveRight_symm : ∀ {x y}, x ≡ y → ∀ i, ∃ j, x.moveRight j ≡ y.moveRight i | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.2 i -/-- Uses `∈ₗ` `∈ᵣ` instead of `≡`. -/ +/-- Uses `∈ₗ` and `∈ᵣ` instead of `≡`. -/ theorem identical_iff' : ∀ {x y : PGame}, x ≡ y ↔ ((∀ i, x.moveLeft i ∈ₗ y) ∧ (∀ j, y.moveLeft j ∈ₗ x)) ∧ ((∀ i, x.moveRight i ∈ᵣ y) ∧ (∀ j, y.moveRight j ∈ᵣ x)) From 52f5a3309861b00cff11f623ca557570ab4f29b3 Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Tue, 22 Oct 2024 20:39:35 +0800 Subject: [PATCH 5/7] fix longfile linter --- Mathlib/SetTheory/Game/PGame.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index 2aaf032db4c80..eb396e0bad135 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -1926,4 +1926,4 @@ end PGame end SetTheory -set_option linter.style.longFile 2300 +set_option linter.style.longFile 2100 From a302520b7bf2f6b4db9a784468428da3dd33775d Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Fri, 15 Nov 2024 01:58:17 +0800 Subject: [PATCH 6/7] suggestions --- Mathlib/SetTheory/Game/PGame.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index 8088316bb172b..e8b7267d4ec16 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -348,7 +348,7 @@ instance isEmpty_one_rightMoves : IsEmpty (RightMoves 1) := /-- Two pre-games are identical if their left and right sets are identical. That is, `Identical x y` if every left move of `x` is identical to some left move of `y`, every right move of `x` is identical to some right move of `y`, and vice versa. -/ -def Identical : ∀ _ _ : PGame.{u}, Prop +def Identical : PGame.{u} → PGame.{u} → Prop | mk _ _ xL xR, mk _ _ yL yR => Relator.BiTotal (fun i j ↦ Identical (xL i) (yL j)) ∧ Relator.BiTotal (fun i j ↦ Identical (xR i) (yR j)) @@ -368,7 +368,7 @@ protected theorem Identical.rfl {x} : x ≡ x := Identical.refl x | mk _ _ _ _, mk _ _ _ _, ⟨hL, hR⟩ => ⟨hL.symm fun _ _ h ↦ h.symm, hR.symm fun _ _ h ↦ h.symm⟩ theorem identical_comm {x y} : x ≡ y ↔ y ≡ x := - ⟨Identical.symm, Identical.symm⟩ + ⟨.symm, .symm⟩ @[trans] protected theorem Identical.trans : ∀ {x y z}, x ≡ y → y ≡ z → x ≡ z | mk _ _ _ _, mk _ _ _ _, mk _ _ _ _, ⟨hL₁, hR₁⟩, ⟨hL₂, hR₂⟩ => @@ -390,7 +390,7 @@ theorem memᵣ_def {x y : PGame} : x ∈ᵣ y ↔ ∃ b, x ≡ y.moveRight b := theorem moveLeft_memₗ (x : PGame) (b) : x.moveLeft b ∈ₗ x := ⟨_, .rfl⟩ theorem moveRight_memᵣ (x : PGame) (b) : x.moveRight b ∈ᵣ x := ⟨_, .rfl⟩ -theorem identical_of_is_empty (x y : PGame) +theorem identical_of_isEmpty (x y : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] [IsEmpty y.LeftMoves] [IsEmpty y.RightMoves] : x ≡ y := identical_iff.2 <| by simp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] From 70db6730f93884e0b8e778ff2e551adca6d8a7d4 Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Fri, 15 Nov 2024 02:13:26 +0800 Subject: [PATCH 7/7] suggestion --- Mathlib/SetTheory/Game/PGame.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean index e8b7267d4ec16..b082ce43291c7 100644 --- a/Mathlib/SetTheory/Game/PGame.lean +++ b/Mathlib/SetTheory/Game/PGame.lean @@ -409,23 +409,12 @@ lemma Identical.moveLeft : ∀ {x y}, x ≡ y → ∀ i, ∃ j, x.moveLeft i ≡ y.moveLeft j | mk _ _ _ _, mk _ _ _ _, ⟨hl, _⟩, i => hl.1 i -/-- If `x` and `y` are identical, then a left move of `y` is identical to some left move of `x`. -/ -lemma Identical.moveLeft_symm : ∀ {x y}, x ≡ y → - ∀ i, ∃ j, x.moveLeft j ≡ y.moveLeft i - | mk _ _ _ _, mk _ _ _ _, ⟨hl, _⟩, i => hl.2 i - /-- If `x` and `y` are identical, then a right move of `x` is identical to some right move of `y`. -/ lemma Identical.moveRight : ∀ {x y}, x ≡ y → ∀ i, ∃ j, x.moveRight i ≡ y.moveRight j | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.1 i -/-- If `x` and `y` are identical, then a right move of `y` is identical to some right move of `x`. --/ -lemma Identical.moveRight_symm : ∀ {x y}, x ≡ y → - ∀ i, ∃ j, x.moveRight j ≡ y.moveRight i - | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.2 i - /-- Uses `∈ₗ` and `∈ᵣ` instead of `≡`. -/ theorem identical_iff' : ∀ {x y : PGame}, x ≡ y ↔ ((∀ i, x.moveLeft i ∈ₗ y) ∧ (∀ j, y.moveLeft j ∈ₗ x)) ∧