Misere combinatorial games.

def MisereGames.Moves.IsOption' {G : Type v} (moves : Player → G → Set G) (x y : G) : Prop

The immediate-option relation determined by a raw move function.

Equations

• MisereGames.Moves.IsOption' moves x y = (x ∈ ⋃ (p : MisereGames.Player), moves p y)

class MisereGames.Moves (G : Type v) : Type v

A type with Left and Right moves and a well-founded option relation.

• moves (p : Player) (x : G) : Set G

  The positions reachable by a move for a player.

• isOption'_wf : WellFounded (IsOption' moves)

  The option relation generated by moves is well-founded.

class MisereGames.Form (G : Type (v + 1)) extends MisereGames.Moves G, MisereGames.OfSets G fun (x : MisereGames.Player → Set G) => True, InvolutiveNeg G, AddCommSemigroup G : Type (v + 1)

A type of combinatorial game forms with negation, addition, and set construction.

• moves (p : Player) (x : G) : Set G
• isOption'_wf : WellFounded (IsOption' moves)
• ofSets (st : Player → Set G) (h : True) [Small.{v, v + 1} ↑(st Player.left)] [Small.{v, v + 1} ↑(st Player.right)] : G
• neg : G → G
• neg_neg (x : G) : - -x = x
• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• add_comm (a b : G) : a + b = b + a
• moves_neg' (p : Player) (x : G) : moves p (-x) = -moves (-p) x
• moves_add' (p : Player) (x y : G) : moves p (x + y) = (fun (x : G) => x + y) '' moves p x ∪ (fun (x_1 : G) => x + x_1) '' moves p y
• moves_small' (p : Player) (x : G) : Small.{v, v + 1} ↑(moves p x)
• moves_ofSets' (p : Player) (st : Player → Set G) [Small.{v, v + 1} ↑(st Player.left)] [Small.{v, v + 1} ↑(st Player.right)] : moves p !{st} = st p
• add_zero' (x : G) : x + !{fun (x : Player) => ∅} = x
• add_eq_zero_iff' (x y : G) : x + y = !{fun (x : Player) => ∅} ↔ x = !{fun (x : Player) => ∅} ∧ y = !{fun (x : Player) => ∅}
• ofSets_inj'' {st₁ st₂ : Player → Set G} [Small.{v, v + 1} ↑(st₁ Player.left)] [Small.{v, v + 1} ↑(st₁ Player.right)] [Small.{v, v + 1} ↑(st₂ Player.left)] [Small.{v, v + 1} ↑(st₂ Player.right)] : !{st₁} = !{st₂} ↔ st₁ = st₂
• neg_ofSets'' (s t : Set G) [Small.{v, v + 1} ↑s] [Small.{v, v + 1} ↑t] : -!{s | t} = !{-t | -s}
• neg_add' (x y : G) : -(x + y) = -x + -y
• smallElemMoves' (p : Player) (x : G) : Small.{v, v + 1} ↑(moves p x)
• IsEndLike (p : Player) (x : G) : Prop

  Positions that behave like ends for a player in the ambient form type.

• ofSets_isEndLike_iff' (p : Player) (s t : Set G) [Small.{v, v + 1} ↑s] [Small.{v, v + 1} ↑t] : IsEndLike p !{s | t} ↔ moves p !{s | t} = ∅
• ofSets_add_ofSets'' (s₁ t₁ s₂ t₂ : Set G) [Small.{v, v + 1} ↑s₁] [Small.{v, v + 1} ↑t₁] [Small.{v, v + 1} ↑s₂] [Small.{v, v + 1} ↑t₂] : !{s₁ | t₁} + !{s₂ | t₂} = !{(fun (x : G) => x + !{s₂ | t₂}) '' s₁ ∪ (fun (x : G) => !{s₁ | t₁} + x) '' s₂ | (fun (x : G) => x + !{s₂ | t₂}) '' t₁ ∪ (fun (x : G) => !{s₁ | t₁} + x) '' t₂}
• isEndLike_ofEnd' (p : Player) (x : G) (h1 : moves p x = ∅) : IsEndLike p x
• isEndLike_add_iff' (p : Player) (x y : G) : IsEndLike p (x + y) ↔ IsEndLike p x ∧ IsEndLike p y
• isEndLike_neg_iff_neg' (p : Player) (g : G) : IsEndLike p (-g) ↔ IsEndLike (-p) g
• ofSets_moves_of_not_isEndLike' (g : G) [Small.{v, v + 1} ↑(moves Player.left g)] [Small.{v, v + 1} ↑(moves Player.right g)] (h : ∀ (p : Player), ¬IsEndLike p g) : !{fun (p : Player) => moves p g} = g

def MisereGames.Moves.IsOption {G : Type (u + 1)} [g_moves : Moves G] (x y : G) : Prop

IsOption x y means that x is either a Left or a Right option for y.

Equations

• MisereGames.Moves.IsOption x y = MisereGames.Moves.IsOption' MisereGames.Moves.moves x y

theorem MisereGames.Moves.IsOption.iff_mem_union {G : Type (u + 1)} [g_moves : Moves G] {x y : G} : IsOption x y ↔ x ∈ moves Player.left y ∪ moves Player.right y

theorem MisereGames.Moves.IsOption.of_mem_moves {G : Type (u + 1)} [g_moves : Moves G] {x y : G} {p : Player} (h : x ∈ moves p y) : IsOption x y

instance MisereGames.Moves.instSmallSubtypeIsOption {G : Type (u + 1)} [g_moves : Moves G] (x : G) : Small.{u + 1, u + 1} { y : G // IsOption y x }

theorem MisereGames.Moves.isOption_wf {G : Type (u + 1)} [g_moves : Moves G] : WellFounded IsOption

instance MisereGames.Moves.instIsWellFoundedIsOption {G : Type (u + 1)} [g_moves : Moves G] : IsWellFounded G IsOption

theorem MisereGames.Moves.IsOption.irrefl {G : Type (u + 1)} [g_moves : Moves G] (x : G) : ¬IsOption x x

theorem MisereGames.Moves.self_notMem_moves {G : Type (u + 1)} [g_moves : Moves G] (p : Player) (x : G) : x ∉ moves p x

def MisereGames.Moves.Subposition {G : Type (u + 1)} [g_moves : Moves G] : G → G → Prop

A proper subposition is an element of the transitive closure of IsOption. Note that this is not the reflexive-transitive closure! While it is common to say that $G$ is a subposition of $G$ in the literature, here Subposition refers to a proper subposition.

Equations

• MisereGames.Moves.Subposition = Relation.TransGen MisereGames.Moves.IsOption

theorem MisereGames.Moves.Subposition.of_isOption {G : Type (u + 1)} [g_moves : Moves G] {x y : G} (h : IsOption x y) : Subposition x y

theorem MisereGames.Moves.Subposition.of_mem_moves {G : Type (u + 1)} [g_moves : Moves G] {p : Player} {x y : G} (h : x ∈ moves p y) : Subposition x y

theorem MisereGames.Moves.Subposition.trans {G : Type (u + 1)} [g_moves : Moves G] {x y z : G} (h₁ : Subposition x y) (h₂ : Subposition y z) : Subposition x z

instance MisereGames.Moves.instSmallSubtypeSubposition {G : Type (u + 1)} [g_moves : Moves G] (x : G) : Small.{u + 1, u + 1} { y : G // Subposition y x }

instance MisereGames.Moves.instIsTransSubposition {G : Type (u + 1)} [g_moves : Moves G] : IsTrans G Subposition

instance MisereGames.Moves.instIsWellFoundedSubposition {G : Type (u + 1)} [g_moves : Moves G] : IsWellFounded G Subposition

@[implicit_reducible]

instance MisereGames.Moves.instWellFoundedRelation {G : Type (u + 1)} [g_moves : Moves G] : WellFoundedRelation G

Equations

• MisereGames.Moves.instWellFoundedRelation = { rel := MisereGames.Moves.Subposition, wf := ⋯ }

def MisereGames.Moves.formWf : Lean.ParserDescr

Solve routine well-foundedness goals generated by recursive form definitions.

Equations

• MisereGames.Moves.formWf = Lean.ParserDescr.node `MisereGames.Moves.formWf 1024 (Lean.ParserDescr.nonReservedSymbol "form_wf" false)

def MisereGames.Form.IsEnd {G : Type (u + 1)} [Moves G] (p : Player) (g : G) : Prop

A position is an end for p when p has no legal move.

Equations

• MisereGames.Form.IsEnd p g = (MisereGames.Moves.moves p g = ∅)

theorem MisereGames.Form.isEnd_def {G : Type (u + 1)} [Moves G] (p : Player) (g : G) : IsEnd p g = (moves p g = ∅)

theorem MisereGames.Form.not_isEnd_def {G : Type (u + 1)} [Moves G] (p : Player) (g : G) : ¬IsEnd p g ↔ moves p g ≠ ∅

theorem MisereGames.Form.isEndLike_of_isEnd {G : Type (u + 1)} [g_form : Form G] {p : Player} {x : G} (h1 : IsEnd p x) : IsEndLike p x

@[simp]

theorem MisereGames.Form.IsEndLike.add_iff {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} : IsEndLike p (x + y) ↔ IsEndLike p x ∧ IsEndLike p y

@[simp]

theorem MisereGames.Form.IsEndLike.neg_iff_neg {G : Type (u + 1)} [g_form : Form G] {g : G} {p : Player} : IsEndLike p (-g) ↔ IsEndLike (-p) g

@[simp]

theorem MisereGames.Form.moves_neg {G : Type (u + 1)} [g_form : Form G] (p : Player) (x : G) : moves p (-x) = -moves (-p) x

@[simp]

theorem MisereGames.Form.moves_add {G : Type (u + 1)} [g_form : Form G] (p : Player) (x y : G) : moves p (x + y) = (fun (x : G) => x + y) '' moves p x ∪ (fun (x_1 : G) => x + x_1) '' moves p y

instance MisereGames.Form.instSmallElemMoves {G : Type (u + 1)} [g_form : Form G] (p : Player) (x : G) : Small.{u, u + 1} ↑(moves p x)

@[simp]

theorem MisereGames.Form.moves_ofSets {G : Type (u + 1)} [g_form : Form G] (p : Player) (st : Player → Set G) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] : moves p !{st} = st p

theorem MisereGames.Form.ofSets_moves_of_not_isEndLike {G : Type (u + 1)} [g_form : Form G] {g : G} (h : ∀ (p : Player), ¬IsEndLike p g) : !{fun (p : Player) => moves p g} = g

Away from end-like positions, a form is determined by its sets of moves.

@[simp]

theorem MisereGames.Form.leftMoves_ofSets {G : Type (u + 1)} [g_form : Form G] (s t : Set G) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : moves Player.left !{s | t} = s

@[simp]

theorem MisereGames.Form.rightMoves_ofSets {G : Type (u + 1)} [g_form : Form G] (s t : Set G) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : moves Player.right !{s | t} = t

@[simp]

theorem MisereGames.Form.ofSets_inj' {G : Type (u + 1)} [g_form : Form G] {st₁ st₂ : Player → Set G} [Small.{u, u + 1} ↑(st₁ Player.left)] [Small.{u, u + 1} ↑(st₁ Player.right)] [Small.{u, u + 1} ↑(st₂ Player.left)] [Small.{u, u + 1} ↑(st₂ Player.right)] : !{st₁} = !{st₂} ↔ st₁ = st₂

theorem MisereGames.Form.ofSets_inj {G : Type (u + 1)} [g_form : Form G] {s₁ s₂ t₁ t₂ : Set G} [Small.{u, u + 1} ↑s₁] [Small.{u, u + 1} ↑s₂] [Small.{u, u + 1} ↑t₁] [Small.{u, u + 1} ↑t₂] : !{s₁ | t₁} = !{s₂ | t₂} ↔ s₁ = s₂ ∧ t₁ = t₂

@[implicit_reducible]

instance MisereGames.Form.instZero {G : Type (u + 1)} [g_form : Form G] : Zero G

Equations

• MisereGames.Form.instZero = { zero := !{fun (x : MisereGames.Player) => ∅} }

theorem MisereGames.Form.zero_def {G : Type (u + 1)} [g_form : Form G] : 0 = !{fun (x : Player) => ∅}

@[simp]

theorem MisereGames.Form.moves_zero {G : Type (u + 1)} [g_form : Form G] (p : Player) : moves p 0 = ∅

@[simp]

theorem MisereGames.Form.isEnd_zero {G : Type (u + 1)} [g_form : Form G] {p : Player} : IsEnd p 0

def MisereGames.Form.IsZeroLike {G : Type (u + 1)} [g_form : Form G] (g : G) : Prop

A form is zero-like if it is both a Left and a Right end, just like 0.

Equations

• MisereGames.Form.IsZeroLike g = ∀ (p : MisereGames.Player), MisereGames.Form.IsEnd p g

@[simp]

theorem MisereGames.Form.isZeroLike_zero {G : Type (u + 1)} [g_form : Form G] : IsZeroLike 0

@[simp]

theorem MisereGames.Form.neg_ofSets {G : Type (u + 1)} [g_form : Form G] (s t : Set G) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : -!{s | t} = !{-t | -s}

@[simp]

theorem MisereGames.Form.neg_ofSets_const {G : Type (u + 1)} [g_form : Form G] (s : Set G) [Small.{u, u + 1} ↑s] : -!{fun (x : Player) => s} = !{fun (x : Player) => -s}

@[implicit_reducible]

instance MisereGames.Form.instNegZeroClass {G : Type (u + 1)} [g_form : Form G] : NegZeroClass G

Equations

• MisereGames.Form.instNegZeroClass = { toZero := MisereGames.Form.instZero, toNeg := g_form.toNeg, neg_zero := ⋯ }

@[implicit_reducible]

instance MisereGames.Form.instInhabited {G : Type (u + 1)} [g_form : Form G] : Inhabited G

Equations

• MisereGames.Form.instInhabited = { default := 0 }

@[implicit_reducible]

instance MisereGames.Form.instOne {G : Type (u + 1)} [g_form : Form G] : One G

Equations

• MisereGames.Form.instOne = { one := !{{0} | ∅} }

theorem MisereGames.Form.one_def {G : Type (u + 1)} [g_form : Form G] : 1 = !{{0} | ∅}

@[simp]

theorem MisereGames.Form.leftMoves_one {G : Type (u + 1)} [g_form : Form G] : moves Player.left 1 = {0}

@[simp]

theorem MisereGames.Form.rightMoves_one {G : Type (u + 1)} [g_form : Form G] : moves Player.right 1 = ∅

@[simp]

theorem MisereGames.Form.moves_small {G : Type (u + 1)} [g_form : Form G] (p : Player) (x : G) : Small.{u, u + 1} ↑(moves p x)

theorem MisereGames.Form.exists_moves_neg {G : Type (u + 1)} [g_form : Form G] {P : G → Prop} {p : Player} {x : G} : (∃ y ∈ moves p (-x), P y) ↔ ∃ y ∈ moves (-p) x, P (-y)

@[simp]

theorem MisereGames.Form.IsEnd.add_iff {G : Type (u + 1)} [g_form : Form G] {g h : G} {p : Player} : IsEnd p (g + h) ↔ IsEnd p g ∧ IsEnd p h

theorem MisereGames.Form.IsEnd.neg_iff_neg {G : Type (u + 1)} [g_form : Form G] {g : G} {p : Player} : IsEnd p (-g) ↔ IsEnd (-p) g

theorem MisereGames.Form.mem_moves_ne_zero {G : Type (u + 1)} [g_form : Form G] {g gl : G} {p : Player} (h1 : gl ∈ moves p g) : g ≠ 0

theorem MisereGames.Form.not_isEnd_ne_zero {G : Type (u + 1)} [g_form : Form G] {g : G} {p : Player} (h1 : ¬IsEnd p g) : g ≠ 0

theorem MisereGames.Form.not_isEnd_exists_move {G : Type (u + 1)} [g_form : Form G] {g : G} {p : Player} (h1 : ¬IsEnd p g) : ∃ (gp : G), gp ∈ moves p g

@[simp]

theorem MisereGames.Form.not_mem_moves_of_isEnd {G : Type (u + 1)} [g_form : Form G] {p : Player} {g gp : G} (h1 : IsEnd p g) : gp ∉ moves p g

theorem MisereGames.Form.not_isEnd_of_mem_moves {G : Type (u + 1)} [g_form : Form G] {p : Player} {g g' : G} (h1 : g' ∈ moves p g) : ¬IsEnd p g

theorem MisereGames.Form.not_isEnd_add_left {G : Type (u + 1)} [g_form : Form G] {p : Player} {g h : G} (h_not_isEnd : ¬IsEnd p g) : ¬IsEnd p (g + h)

theorem MisereGames.Form.not_isEnd_add_right {G : Type (u + 1)} [g_form : Form G] {p : Player} {g h : G} (h_not_isEnd : ¬IsEnd p h) : ¬IsEnd p (g + h)

theorem MisereGames.Form.add_left_mem_moves_add {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (h : x ∈ moves p y) (z : G) : z + x ∈ moves p (z + y)

theorem MisereGames.Form.add_right_mem_moves_add {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (h : x ∈ moves p y) (z : G) : x + z ∈ moves p (y + z)

@[implicit_reducible]

instance MisereGames.Form.instAddCommMonoid {G : Type (u + 1)} [g_form : Form G] : AddCommMonoid G

Equations

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

@[implicit_reducible]

instance MisereGames.Form.instSubNegMonoid {G : Type (u + 1)} [g_form : Form G] : SubNegMonoid G

Equations

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

@[implicit_reducible]

instance MisereGames.Form.instAddCommMonoidWithOne {G : Type (u + 1)} [g_form : Form G] : AddCommMonoidWithOne G

Equations

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

theorem MisereGames.Form.sub_left_mem_moves_sub {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (h : x ∈ moves p y) (z : G) : z - x ∈ moves (-p) (z - y)

theorem MisereGames.Form.sub_left_mem_moves_sub_neg {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (h : x ∈ moves (-p) y) (z : G) : z - x ∈ moves p (z - y)

theorem MisereGames.Form.sub_right_mem_moves_sub {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (h : x ∈ moves p y) (z : G) : x - z ∈ moves p (y - z)

theorem MisereGames.Form.exists_moves_add {G : Type (u + 1)} [g_form : Form G] {p : Player} {P : G → Prop} {x y : G} : (∃ a ∈ moves p (x + y), P a) ↔ (∃ a ∈ moves p x, P (a + y)) ∨ ∃ b ∈ moves p y, P (x + b)

theorem MisereGames.Form.isOption_iff_mem_union {G : Type (u + 1)} [g_form : Form G] {x y : G} : IsOption x y ↔ x ∈ moves Player.left y ∪ moves Player.right y

theorem MisereGames.Form.isOption_iff_mem_moves {G : Type (u + 1)} [g_form : Form G] {x y : G} : IsOption x y ↔ ∃ (p : Player), x ∈ moves p y

@[simp]

theorem MisereGames.Form.not_isOption_zero {G : Type (u + 1)} [g_form : Form G] (g : G) : ¬IsOption g 0

@[simp]

theorem MisereGames.Form.isOption_zero_neg_iff {G : Type (u + 1)} [g_form : Form G] {g : G} : IsOption 0 (-g) ↔ IsOption 0 g

theorem MisereGames.Form.isOption_not_mem {G : Type (u + 1)} [g_form : Form G] {p : Player} {g g' : G} (h_isOption : IsOption g' g) (h_mem : g' ∉ moves p g) : g' ∈ moves (-p) g

theorem MisereGames.Form.isOption_not_mem_neg {G : Type (u + 1)} [g_form : Form G] {p : Player} {g g' : G} (h_isOption : IsOption g' g) (h_mem : g' ∉ moves (-p) g) : g' ∈ moves p g

theorem MisereGames.Form.leftMoves_natCast_succ' {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : moves Player.left ↑n.succ = {↑n}

@[simp]

theorem MisereGames.Form.leftMoves_natCast_succ {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : moves Player.left (↑n + 1) = {↑n}

@[simp]

theorem MisereGames.Form.rightMoves_natCast {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : moves Player.right ↑n = ∅

@[simp]

theorem MisereGames.Form.leftMoves_ofNat {G : Type (u + 1)} [g_form : Form G] (n : ℕ) [n.AtLeastTwo] : moves Player.left (OfNat.ofNat n) = {↑(n - 1)}

@[simp]

theorem MisereGames.Form.rightMoves_ofNat {G : Type (u + 1)} [g_form : Form G] (n : ℕ) [n.AtLeastTwo] : moves Player.right (OfNat.ofNat n) = ∅

@[implicit_reducible]

instance MisereGames.Form.instIntCast {G : Type (u + 1)} [g_form : Form G] : IntCast G

Equations

• MisereGames.Form.instIntCast = { intCast := fun (x : ℤ) => match x with | Int.ofNat n => ↑n | Int.negSucc n => -(↑n + 1) }

@[simp]

theorem MisereGames.Form.intCast_nat {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem MisereGames.Form.intCast_ofNat {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : ↑(OfNat.ofNat n) = ↑n

@[simp]

theorem MisereGames.Form.intCast_negSucc {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : ↑(Int.negSucc n) = -(↑n + 1)

theorem MisereGames.Form.intCast_zero {G : Type (u + 1)} [g_form : Form G] : ↑0 = 0

theorem MisereGames.Form.intCast_one {G : Type (u + 1)} [g_form : Form G] : ↑1 = 1

theorem MisereGames.Form.natCast_zero {G : Type (u + 1)} [g_form : Form G] : ↑0 = 0

theorem MisereGames.Form.natCast_one {G : Type (u + 1)} [g_form : Form G] : ↑1 = 1

@[simp]

theorem MisereGames.Form.intCast_neg {G : Type (u + 1)} [g_form : Form G] (n : ℤ) : ↑(-n) = -↑n

@[simp]

theorem MisereGames.Form.leftMoves_eq_natCast_zero_lt {G : Type (u + 1)} [g_form : Form G] {a : ℕ} (h1 : 0 < a) : moves Player.left ↑a = {↑(a - 1)}

theorem MisereGames.Form.leftMoves_natCast_zero_lt {G : Type (u + 1)} [g_form : Form G] {a : ℕ} (h1 : 0 < a) : ↑(a - 1) ∈ moves Player.left ↑a

@[simp]

theorem MisereGames.Form.leftMoves_intCast_succ {G : Type (u + 1)} [g_form : Form G] {n : ℤ} (h1 : 0 ≤ n) : moves Player.left (↑n + 1) = {↑n}

@[simp]

theorem MisereGames.Form.leftMoves_intCast {G : Type (u + 1)} [g_form : Form G] {a : ℤ} (h1 : 0 < a) : moves Player.left ↑a = {↑(a - 1)}

theorem MisereGames.Form.leftMoves_intCast_zero_lt {G : Type (u + 1)} [g_form : Form G] {a : ℤ} (h1 : 0 < a) : ↑(a - 1) ∈ moves Player.left ↑a

theorem MisereGames.Form.leftMoves_intCast_zero_le_succ {G : Type (u + 1)} [g_form : Form G] {a : ℤ} (h1 : 0 ≤ a) : ↑a ∈ moves Player.left ↑(a + 1)

theorem MisereGames.Form.leftMoves_intCast_le_zero_of_empty {G : Type (u + 1)} [g_form : Form G] {k : ℤ} (h1 : 0 ≤ k) (h2 : moves Player.left ↑k = ∅) : k = 0

theorem MisereGames.Form.leftMoves_intCast_le_one_eq {G : Type (u + 1)} [g_form : Form G] {a : ℤ} (h1 : 1 ≤ a) : moves Player.left ↑a = {↑(a - 1)}

@[simp]

theorem MisereGames.Form.leftMoves_intCast_le_one_ne_empty {G : Type (u + 1)} [g_form : Form G] {a : ℤ} (h1 : 1 ≤ a) : moves Player.left ↑a ≠ ∅

@[simp]

theorem MisereGames.Form.rightMoves_intCast {G : Type (u + 1)} [g_form : Form G] {a : ℤ} (h1 : 0 ≤ a) : moves Player.right ↑a = ∅

theorem MisereGames.Form.mem_moves_add_one_iff_mem_moves {G : Type (u + 1)} [g_form : Form G] {g : G} {p : Player} {n : ℕ} : g + 1 ∈ moves p (↑n + 1) ↔ g ∈ moves p ↑n

@[simp]

theorem MisereGames.Form.one_isEnd_right {G : Type (u + 1)} [g_form : Form G] : IsEnd Player.right 1

@[simp]

theorem MisereGames.Form.not_isEnd_left_one {G : Type (u + 1)} [g_form : Form G] : ¬IsEnd Player.left 1

theorem MisereGames.Form.natCast_isEnd_right {G : Type (u + 1)} [g_form : Form G] (n : ℕ) : IsEnd Player.right ↑n

@[simp]

theorem MisereGames.Form.ofSets_isEndLike_iff {G : Type (u + 1)} [g_form : Form G] {p : Player} {s t : Set G} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] : IsEndLike p !{s | t} ↔ IsEnd p !{s | t}

theorem MisereGames.Form.ofSets_add_ofSets {G : Type (u + 1)} [g_form : Form G] (s₁ t₁ s₂ t₂ : Set G) [Small.{u, u + 1} ↑s₁] [Small.{u, u + 1} ↑t₁] [Small.{u, u + 1} ↑s₂] [Small.{u, u + 1} ↑t₂] : !{s₁ | t₁} + !{s₂ | t₂} = !{(fun (x : G) => x + !{s₂ | t₂}) '' s₁ ∪ (fun (x : G) => !{s₁ | t₁} + x) '' s₂ | (fun (x : G) => x + !{s₂ | t₂}) '' t₁ ∪ (fun (x : G) => !{s₁ | t₁} + x) '' t₂}

theorem MisereGames.Form.ofSets_add_ofSets' {G : Type (u + 1)} [g_form : Form G] (st₁ st₂ : Player → Set G) [Small.{u, u + 1} ↑(st₁ Player.left)] [Small.{u, u + 1} ↑(st₂ Player.left)] [Small.{u, u + 1} ↑(st₁ Player.right)] [Small.{u, u + 1} ↑(st₂ Player.right)] : !{st₁} + !{st₂} = !{fun (p : Player) => (fun (x : G) => x + !{st₂}) '' st₁ p ∪ (fun (x : G) => !{st₁} + x) '' st₂ p}

theorem MisereGames.Form.natCast_add_one_ofSets {G : Type (u + 1)} [g_form : Form G] {n : ℕ} : ↑(n + 1) = !{{↑n} | ∅}

@[simp]

theorem MisereGames.Form.natCast_isEndLike_iff {G : Type (u + 1)} [g_form : Form G] {p : Player} {n : ℕ} : IsEndLike p ↑n ↔ IsEnd p ↑n

@[simp]

theorem MisereGames.Form.one_isEndLike_right {G : Type (u + 1)} [g_form : Form G] : IsEndLike Player.right 1

@[simp]

theorem MisereGames.Form.not_isEndLike_left_one {G : Type (u + 1)} [g_form : Form G] : ¬IsEndLike Player.left 1

theorem MisereGames.Form.natCast_ext {G : Type (u + 1)} [g_form : Form G] {k m : ℕ} (h_moves : ∀ (p : Player) (gp : G), gp ∈ moves p ↑k ↔ gp ∈ moves p ↑m) : ↑k = ↑m

@[simp]

theorem MisereGames.Form.isEnd_left_natCast_iff {G : Type (u + 1)} [g_form : Form G] {n : ℕ} : IsEnd Player.left ↑n ↔ n = 0

@[simp]

theorem MisereGames.Form.isEnd_left_intCast_iff {G : Type (u + 1)} [g_form : Form G] {n : ℤ} : IsEnd Player.left ↑n ↔ n ≤ 0

@[simp]

theorem MisereGames.Form.isEnd_right_intCast_iff {G : Type (u + 1)} [g_form : Form G] {n : ℤ} : IsEnd Player.right ↑n ↔ 0 ≤ n

@[simp]

theorem MisereGames.Form.isEnd_right_natCast {G : Type (u + 1)} [g_form : Form G] {n : ℕ} : IsEnd Player.right ↑n

theorem MisereGames.Form.isEnd_of_not_mem {G : Type (u + 1)} [g_form : Form G] {p : Player} {g : G} (h1 : ∀ (gr : G), gr ∉ moves p g) : IsEnd p g

theorem MisereGames.Form.natCast_injective {G : Type (u + 1)} [g_form : Form G] : Function.Injective Nat.cast

instance MisereGames.Form.instCharZero {G : Type (u + 1)} [g_form : Form G] : CharZero G

theorem MisereGames.Form.eq_sub_one_of_mem_leftMoves_intCast {G : Type (u + 1)} [g_form : Form G] {n : ℤ} {x : G} (hx : x ∈ moves Player.left ↑n) : x = ↑(n - 1)

theorem MisereGames.Form.eq_add_one_of_mem_rightMoves_intCast {G : Type (u + 1)} [g_form : Form G] {n : ℤ} {x : G} (hx : x ∈ moves Player.right ↑n) : x = ↑(n + 1)

theorem MisereGames.Form.eq_intCast_of_mem_leftMoves_intCast {G : Type (u + 1)} [g_form : Form G] {n : ℤ} {x : G} (hx : x ∈ moves Player.left ↑n) : ∃ m < n, ↑m = x

Every Left option of an integer is equal to a smaller integer.

theorem MisereGames.Form.eq_intCast_of_mem_rightMoves_intCast {G : Type (u + 1)} [g_form : Form G] {n : ℤ} {x : G} (hx : x ∈ moves Player.right ↑n) : ∃ (m : ℤ), n < m ∧ ↑m = x

theorem MisereGames.Form.succ_nat_end_right {G : Type (u + 1)} [g_form : Form G] {p : Player} {n : ℕ} : IsEnd p ↑n.succ ↔ p = Player.right

theorem MisereGames.Form.nat_forall_moves {G : Type (u + 1)} [g_form : Form G] {n : ℕ} {P : G → Prop} (h1 : P ↑n) (p : Player) (gp : G) : gp ∈ moves p ↑n.succ → P gp

If P holds at n, then P holds at every option of n+1 (since n is the only such option).

@[simp]

theorem MisereGames.Form.add_eq_zero_iff {G : Type (u + 1)} [g_form : Form G] {x y : G} : x + y = 0 ↔ x = 0 ∧ y = 0

@[implicit_reducible]

instance MisereGames.Form.instSubtractionCommMonoid {G : Type (u + 1)} [g_form : Form G] : SubtractionCommMonoid G

Equations

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

@[simp]

theorem MisereGames.Form.IsEnd.sub_iff {G : Type (u + 1)} [g_form : Form G] {g h : G} {p : Player} : IsEnd p (g - h) ↔ IsEnd p g ∧ IsEnd (-p) h

theorem MisereGames.Form.mem_leftMoves_natSub_add_isEnd {G : Type (u + 1)} [g_form : Form G] {a b : ℕ} {y g' : G} (hye : IsEnd Player.left y) : g' ∈ moves Player.left (↑a - ↑b + y) ↔ ∃ (a' : ℕ), a = a' + 1 ∧ g' = ↑a' - ↑b + y

theorem MisereGames.Form.mem_rightMoves_natSub_add {G : Type (u + 1)} [g_form : Form G] {a b : ℕ} {y g' : G} : g' ∈ moves Player.right (↑a - ↑b + y) ↔ (∃ (b' : ℕ), b = b' + 1 ∧ g' = ↑a - ↑b' + y) ∨ ∃ yr ∈ moves Player.right y, g' = ↑a - ↑b + yr