@[irreducible]

def Form.Misere.Outcome.WinsGoingFirst {G : Type (u + 1)} [Form G] (p : Player) (g : G) : Prop

Equations

• Form.Misere.Outcome.WinsGoingFirst p g = (Form.IsEndLike p g ∨ ∃ (g' : G) (_ : g' ∈ Moves.moves p g), ¬Form.Misere.Outcome.WinsGoingFirst (-p) g')

theorem Form.Misere.Outcome.winsGoingFirst_iff {G : Type (u + 1)} [Form G] (g : G) (p : Player) : WinsGoingFirst p g ↔ IsEndLike p g ∨ ∃ g' ∈ moves p g, ¬WinsGoingFirst (-p) g'

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_of_isEndLike {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsEndLike p g) : WinsGoingFirst p g

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_of_isEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsEnd p g) : WinsGoingFirst p g

theorem Form.Misere.Outcome.winsGoingFirst_of_moves {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : ∃ g' ∈ moves p g, ¬WinsGoingFirst (-p) g') : WinsGoingFirst p g

@[irreducible]

theorem Form.Misere.Outcome.winsGoingFirst_neg_iff {G : Type (u + 1)} [Form G] (g : G) (p : Player) : WinsGoingFirst p (-g) ↔ WinsGoingFirst (-p) g

theorem Form.Misere.Outcome.not_winsGoingFirst_iff {G : Type (u + 1)} [Form G] {g : G} {p : Player} : ¬WinsGoingFirst p g ↔ ¬IsEndLike p g ∧ ∀ g' ∈ moves p g, WinsGoingFirst (-p) g'

theorem Form.Misere.Outcome.winsGoingFirst_zero {G : Type (u + 1)} [Form G] (p : Player) : WinsGoingFirst p 0

noncomputable def Form.Misere.Outcome.MiserePlayerOutcome {G : Type (u + 1)} [Form G] : G → Player → Player

Equations

• Form.Misere.Outcome.MiserePlayerOutcome g p = if Form.Misere.Outcome.WinsGoingFirst p g then p else -p

noncomputable def Form.Misere.Outcome.MisereOutcome {G : Type (u + 1)} [Form G] : G → Outcome

Equations

• Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayers (Form.Misere.Outcome.MiserePlayerOutcome g Player.left) (Form.Misere.Outcome.MiserePlayerOutcome g Player.right)

@[simp]

theorem Form.Misere.Outcome.miserePlayerOutcome_eq_iff_winsGoingFirst {G : Type (u + 1)} [Form G] {g : G} {p : Player} : MiserePlayerOutcome g p = p ↔ WinsGoingFirst p g

theorem Form.Misere.Outcome.misereOutcome_L_iff_miserePlayerOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.L ↔ MiserePlayerOutcome g Player.left = Player.left ∧ MiserePlayerOutcome g Player.right = Player.left

theorem Form.Misere.Outcome.misereOutcome_N_iff_miserePlayerOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.N ↔ MiserePlayerOutcome g Player.left = Player.left ∧ MiserePlayerOutcome g Player.right = Player.right

theorem Form.Misere.Outcome.misereOutcome_P_iff_miserePlayerOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.P ↔ MiserePlayerOutcome g Player.left = Player.right ∧ MiserePlayerOutcome g Player.right = Player.left

theorem Form.Misere.Outcome.misereOutcome_R_iff_miserePlayerOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.R ↔ MiserePlayerOutcome g Player.left = Player.right ∧ MiserePlayerOutcome g Player.right = Player.right

@[simp]

theorem Form.Misere.Outcome.minsGoingFirst_left_of_misereOutcome_L {G : Type (u + 1)} [Form G] {g : G} (h1 : MisereOutcome g = Outcome.L) : WinsGoingFirst Player.left g

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_right_of_misereOutcome_R {G : Type (u + 1)} [Form G] {g : G} (h1 : MisereOutcome g = Outcome.R) : WinsGoingFirst Player.right g

@[simp]

theorem Form.Misere.Outcome.miserePlayerOutcome_neg_player_neg {G : Type (u + 1)} [Form G] (g : G) (p : Player) : MiserePlayerOutcome (-g) p = -MiserePlayerOutcome g (-p)

@[simp]

theorem Form.Misere.Outcome.misereOutcome_conjugate_neg {G : Type (u + 1)} [Form G] (g : G) : (MisereOutcome g).Conjugate = MisereOutcome (-g)

theorem Form.Misere.Outcome.misereOutcome_ge_P_of_not_winsGoingFirst_right {G : Type (u + 1)} [Form G] {g : G} (h1 : ¬WinsGoingFirst Player.right g) : MisereOutcome g ≥ Outcome.P

theorem Form.Misere.Outcome.misereOutcome_le_N_of_winsGoingFirst_right {G : Type (u + 1)} [Form G] {g : G} (h1 : WinsGoingFirst Player.right g) : MisereOutcome g ≤ Outcome.N

theorem Form.Misere.Outcome.not_winsGoingFirst_of_misereOutcome_P {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : MisereOutcome g = Outcome.P) : ¬WinsGoingFirst p g

theorem Form.Misere.Outcome.misereOutcome_P_of_miserePlayerOutcome_neg {G : Type (u + 1)} [Form G] {g : G} (h1 : ∀ (p : Player), MiserePlayerOutcome g p = -p) : MisereOutcome g = Outcome.P

@[simp]

theorem Form.Misere.Outcome.misereOutcome_eq_player_iff {G : Type (u + 1)} [Form G] (g : G) (p : Player) : MisereOutcome g = Outcome.ofPlayer p ↔ WinsGoingFirst p g ∧ ¬WinsGoingFirst (-p) g

theorem Form.Misere.Outcome.misereOutcome_L_iff_winsGoingFirst {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.L ↔ WinsGoingFirst Player.left g ∧ ¬WinsGoingFirst Player.right g

theorem Form.Misere.Outcome.misereOutcome_R_iff_winsGoingFirst {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.R ↔ WinsGoingFirst Player.right g ∧ ¬WinsGoingFirst Player.left g

theorem Form.Misere.Outcome.misereOutcome_P_iff_winsGoingFirst' {G : Type (u + 1)} [Form G] {g : G} {p : Player} : MisereOutcome g = Outcome.P ↔ ¬WinsGoingFirst p g ∧ ¬WinsGoingFirst (-p) g

theorem Form.Misere.Outcome.misereOutcome_P_iff_winsGoingFirst {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.P ↔ ¬WinsGoingFirst Player.right g ∧ ¬WinsGoingFirst Player.left g

theorem Form.Misere.Outcome.misereOutcome_N_iff_winsGoingFirst {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g = Outcome.N ↔ WinsGoingFirst Player.left g ∧ WinsGoingFirst Player.right g

theorem Form.Misere.Outcome.misereOutcome_N_iff_winsGoingFirst' {G : Type (u + 1)} [Form G] {g : G} {p : Player} : MisereOutcome g = Outcome.N ↔ WinsGoingFirst p g ∧ WinsGoingFirst (-p) g

theorem Form.Misere.Outcome.misereOutcome_ne_P_iff_winsGoingFirst {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome g ≠ Outcome.P ↔ WinsGoingFirst Player.right g ∨ WinsGoingFirst Player.left g

theorem Form.Misere.Outcome.winsGoingFirst_left_of_ge_N {G : Type (u + 1)} [Form G] {x : G} (h : MisereOutcome x ≥ Outcome.N) : WinsGoingFirst Player.left x

If o(x) ≥ N then Left wins going first on x.

@[simp]

theorem Form.Misere.Outcome.miserePlayerOutcome_zero {G : Type (u + 1)} [Form G] (p : Player) : MiserePlayerOutcome 0 p = p

@[simp]

theorem Form.Misere.Outcome.misereOutcome_zero_N {G : Type (u + 1)} [Form G] : MisereOutcome 0 = Outcome.N

@[simp]

theorem Form.Misere.Outcome.misereOutcome_neg_R_iff_misereOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome (-g) = Outcome.R ↔ MisereOutcome g = Outcome.L

@[simp]

theorem Form.Misere.Outcome.misereOutcome_neg_L_iff_misereOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome (-g) = Outcome.L ↔ MisereOutcome g = Outcome.R

@[simp]

theorem Form.Misere.Outcome.misereOutcome_neg_N_iff_misereOutcome {G : Type (u + 1)} [Form G] {g : G} : MisereOutcome (-g) = Outcome.N ↔ MisereOutcome g = Outcome.N

theorem Form.Misere.Outcome.winsGoingFirst_left_of_move_misereOutcome_P {G : Type (u + 1)} [Form G] {g gl : G} (h1 : gl ∈ moves Player.left g) (h2 : MisereOutcome gl = Outcome.P) : WinsGoingFirst Player.left g

theorem Form.Misere.Outcome.winsGoingFirst_add_of_isEndLike {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsEndLike p g) (h2 : IsEndLike p h) : WinsGoingFirst p (g + h)

theorem Form.Misere.Outcome.winsGoingFirst_add_of_isEnd {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsEnd p g) (h2 : IsEnd p h) : WinsGoingFirst p (g + h)

theorem Form.Misere.Outcome.miserePlayerOutcome_of_leftMoves {G : Type (u + 1)} [Form G] {g gl : G} (h1 : gl ∈ moves Player.left g) (h2 : MiserePlayerOutcome gl Player.right = Player.left) : MiserePlayerOutcome g Player.left = Player.left

theorem Form.Misere.Outcome.miserePlayerOutcome_of_rightMoves {G : Type (u + 1)} [Form G] {g gr : G} (h1 : gr ∈ moves Player.right g) (h2 : MiserePlayerOutcome gr Player.left = Player.right) : MiserePlayerOutcome g Player.right = Player.right

theorem Form.Misere.Outcome.misereOutcome_ge_iff_miserePlayerOutcome_ge {G : Type (u + 1)} [Form G] {g h : G} : MisereOutcome g ≥ MisereOutcome h ↔ ∀ (p : Player), MiserePlayerOutcome g p ≥ MiserePlayerOutcome h p

def Form.Misere.Outcome.MisereEQ {G : Type (u + 1)} [Form G] (A : G → Prop) (g h : G) : Prop

Restricted misère equivalence, working modulo a set A.

Conventions for notations in identifiers:

• The recommended spelling of =m in identifiers is misereEQ.

Equations

• g =m A h = ∀ (x : G), A x → Form.Misere.Outcome.MisereOutcome (g + x) = Form.Misere.Outcome.MisereOutcome (h + x)

def Form.Misere.Outcome.misereEQ : Lean.TrailingParserDescr

Restricted misère equivalence, working modulo a set A.

Conventions for notations in identifiers:

• The recommended spelling of =m in identifiers is misereEQ.

Equations

• One or more equations did not get rendered due to their size.

def Form.Misere.Outcome.delab_misereEQ : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

theorem Form.Misere.Outcome.MisereEQ.symm {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (h1 : g =m A h) : h =m A g

theorem Form.Misere.Outcome.MisereEQ.trans {G : Type (u + 1)} [Form G] {A : G → Prop} {g h k : G} (h1 : g =m A h) (h2 : h =m A k) : g =m A k

def Form.Misere.Outcome.MisereGE {G : Type (u + 1)} [Form G] (A : G → Prop) (g h : G) : Prop

The restricted misère preorder, working modulo a set A.

Conventions for notations in identifiers:

• The recommended spelling of ≥m in identifiers is misereGE.

Equations

• g ≥m A h = ∀ (x : G), A x → Form.Misere.Outcome.MisereOutcome (g + x) ≥ Form.Misere.Outcome.MisereOutcome (h + x)

def Form.Misere.Outcome.misereGE : Lean.TrailingParserDescr

The restricted misère preorder, working modulo a set A.

Conventions for notations in identifiers:

• The recommended spelling of ≥m in identifiers is misereGE.

Equations

• One or more equations did not get rendered due to their size.

def Form.Misere.Outcome.delab_misereGE : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

theorem Form.Misere.Outcome.MisereEq.of_antisymm {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (h1 : g ≥m A h) (h2 : h ≥m A g) : g =m A h

theorem Form.Misere.Outcome.MisereGE.trans {G : Type (u + 1)} [Form G] {A : G → Prop} {g h k : G} (h1 : g ≥m A h) (h2 : h ≥m A k) : g ≥m A k

theorem Form.Misere.Outcome.misereGE_rw_left_iff {G : Type (u + 1)} [Form G] {A : G → Prop} {a b c : G} (h_eq : b =m A c) : b ≥m A a ↔ c ≥m A a

theorem Form.Misere.Outcome.misereGE_rw_right_iff {G : Type (u + 1)} [Form G] {A : G → Prop} {a b c : G} (h_eq : b =m A c) : a ≥m A b ↔ a ≥m A c

theorem Form.Misere.Outcome.misereGE_of_misereEQ {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (h1 : g =m A h) : g ≥m A h

theorem Form.Misere.Outcome.misereGE_of_subset {G : Type (u + 1)} [Form G] (U : G → Prop) {V : G → Prop} (h_v_subset_u : ∀ (g : G), V g → U g) (g h : G) (h2 : g ≥m U h) : g ≥m V h

theorem Form.Misere.Outcome.misereGE_add_right {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] {g h c : G} (hc : A c) (h1 : g ≥m A h) : (g + c) ≥m A h + c

Adding a fixed element c ∈ A on the right preserves the restricted misère inequality.

theorem Form.Misere.Outcome.misereEQ_add_right {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] {g h c : G} (hc : A c) (h1 : g =m A h) : (g + c) =m A h + c

Adding a fixed element c ∈ A on the right preserves the restricted misère equivalence.

theorem Form.Misere.Outcome.misereEQ_add_left {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderAdd A] {g h c : G} (hc : A c) (h1 : g =m A h) : (c + g) =m A c + h

Adding a fixed element c ∈ A on the left preserves the restricted misère equivalence.

@[simp]

theorem Form.Misere.Outcome.MisereGE.refl {G : Type (u + 1)} [Form G] {A : G → Prop} (g : G) : g ≥m A g

theorem Form.Misere.Outcome.not_misereEQ_of_not_misereGE {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (h1 : ¬g ≥m A h) : ¬g =m A h

@[simp]

theorem Form.Misere.Outcome.ClosedUnderNeg.neg_ge_neg_iff {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] (g h : G) : (-h) ≥m A-g ↔ g ≥m A h

theorem Form.Misere.Outcome.misereEQ_neg_iff {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] {g h : G} : (-g) =m A-h ↔ g =m A h

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_left_intCast_iff {G : Type (u + 1)} [Form G] (n : ℤ) : WinsGoingFirst Player.left ↑n ↔ n ≤ 0

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_left_natCast_iff {G : Type (u + 1)} [Form G] (n : ℕ) : WinsGoingFirst Player.left ↑n ↔ n = 0

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_right_intCast_iff {G : Type (u + 1)} [Form G] (n : ℤ) : WinsGoingFirst Player.right ↑n ↔ 0 ≤ n

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_right_natCast {G : Type (u + 1)} [Form G] (n : ℕ) : WinsGoingFirst Player.right ↑n

@[simp]

theorem Form.Misere.Outcome.not_winsGoingFirst_left_one {G : Type (u + 1)} [Form G] : ¬WinsGoingFirst Player.left 1

@[simp]

theorem Form.Misere.Outcome.winsGoingFirst_right_one {G : Type (u + 1)} [Form G] : WinsGoingFirst Player.right 1

@[simp]

theorem Form.Misere.Outcome.one_misereOutcome_R {G : Type (u + 1)} [Form G] : MisereOutcome 1 = Outcome.R

@[simp]

theorem Form.Misere.Outcome.misereOutcome_R_intCast_iff {G : Type (u + 1)} [Form G] (n : ℤ) : MisereOutcome ↑n = Outcome.R ↔ 0 < n

@[simp]

theorem Form.Misere.Outcome.misereOutcome_R_natCast_iff {G : Type (u + 1)} [Form G] (n : ℕ) : MisereOutcome ↑n = Outcome.R ↔ 0 < n

@[simp]

theorem Form.Misere.Outcome.misereOutcome_L_intCast_iff {G : Type (u + 1)} [Form G] (n : ℤ) : MisereOutcome ↑n = Outcome.L ↔ n < 0

@[simp]

theorem Form.Misere.Outcome.misereOutcome_L_natCast {G : Type (u + 1)} [Form G] (n : ℕ) : ¬MisereOutcome ↑n = Outcome.L

@[simp]

theorem Form.Misere.Outcome.misereOutcome_N_intCast_iff {G : Type (u + 1)} [Form G] (n : ℤ) : MisereOutcome ↑n = Outcome.N ↔ n = 0

@[simp]

theorem Form.Misere.Outcome.misereOutcome_N_natCast_iff {G : Type (u + 1)} [Form G] (n : ℕ) : MisereOutcome ↑n = Outcome.N ↔ n = 0

@[simp]

theorem Form.Misere.Outcome.misereOutcome_P_intCast {G : Type (u + 1)} [Form G] (n : ℤ) : ¬MisereOutcome ↑n = Outcome.P

@[simp]

theorem Form.Misere.Outcome.misereOutcome_P_natCast {G : Type (u + 1)} [Form G] (n : ℕ) : ¬MisereOutcome ↑n = Outcome.P

theorem Form.Misere.Outcome.misereOutcome_eq_winsGoingFirst_iff {G : Type (u + 1)} [Form G] {p : Player} {g h : G} (h_eq : MisereOutcome g = MisereOutcome h) : WinsGoingFirst p g ↔ WinsGoingFirst p h

theorem Form.Misere.Outcome.winsGoingFirst_left_add_of_misereGE_zero {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (h_h : A h) (h_g_ge_zero : g ≥m A↑0) (h_h_left_win : WinsGoingFirst Player.left h) : WinsGoingFirst Player.left (g + h)

theorem Form.Misere.Outcome.add_neg_self_misereOutcome {G : Type (u + 1)} [Form G] (g : G) : MisereOutcome (g + -g) = Outcome.N ∨ MisereOutcome (g + -g) = Outcome.P