ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>NonAssocSemiring R<VAR>e : Sym2 α<VAR>Fintype α<VAR>Decidable (e ∈ G.edgeSet)<GOAL>((SimpleGraph.incMatrix R G)ᵀ * SimpleGraph.incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>Fintype (Sym2 α)<VAR>Semiring R<VAR>a b : α<VAR>h : G.Adj a b<GOAL>(SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G)ᵀ) a b = 1
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>Fintype (Sym2 α)<VAR>Semiring R<VAR>(a : α) → Fintype ↑(G.neighborSet a)<VAR>DecidableEq α<VAR>DecidableRel G.Adj<GOAL>SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G)ᵀ = fun a b => if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<GOAL>(SetTheory.PGame.mk xl xr xL xR).LeftMoves = xl
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<GOAL>(SetTheory.PGame.mk xl xr xL xR).moveLeft = xL
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<GOAL>(SetTheory.PGame.mk xl xr xL xR).RightMoves = xr
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<GOAL>(SetTheory.PGame.mk xl xr xL xR).moveRight = xR
<VAR>L R : List SetTheory.PGame<GOAL>(SetTheory.PGame.ofLists L R).LeftMoves = ULift.{u_1, 0} (Fin L.length)
<VAR>L R : List SetTheory.PGame<GOAL>(SetTheory.PGame.ofLists L R).RightMoves = ULift.{u_1, 0} (Fin R.length)
<VAR>L R : List SetTheory.PGame<VAR>i : Fin L.length<GOAL>(SetTheory.PGame.ofLists L R).moveLeft (SetTheory.PGame.toOfListsLeftMoves i) = L.get i
<VAR>L R : List SetTheory.PGame<VAR>i : (SetTheory.PGame.ofLists L R).LeftMoves<GOAL>(SetTheory.PGame.ofLists L R).moveLeft i = L.get (SetTheory.PGame.toOfListsLeftMoves.symm i)
<VAR>L R : List SetTheory.PGame<VAR>i : Fin R.length<GOAL>(SetTheory.PGame.ofLists L R).moveRight (SetTheory.PGame.toOfListsRightMoves i) = R.get i
<VAR>L R : List SetTheory.PGame<VAR>i : (SetTheory.PGame.ofLists L R).RightMoves<GOAL>(SetTheory.PGame.ofLists L R).moveRight i = R.get (SetTheory.PGame.toOfListsRightMoves.symm i)
<GOAL>∀ (a a_1 : SetTheory.PGame), a.IsOption a_1 ↔ (∃ i, a = a_1.moveLeft i) ∨ ∃ i, a = a_1.moveRight i
<VAR>xl xr : Type u<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>i : xl<GOAL>(xL i).IsOption (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>i : xr<GOAL>(xR i).IsOption (SetTheory.PGame.mk xl xr xL xR)
<VAR>x y z : SetTheory.PGame<GOAL>x.Subsequent y → y.Subsequent z → x.Subsequent z
<VAR>x : SetTheory.PGame<VAR>i : x.LeftMoves<GOAL>(x.moveLeft i).Subsequent x
<VAR>x : SetTheory.PGame<VAR>j : x.RightMoves<GOAL>(x.moveRight j).Subsequent x
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>i : xl<GOAL>(xL i).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>j : xr<GOAL>(xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>j : (SetTheory.PGame.mk xl xr xL xR).RightMoves<GOAL>(xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u<VAR>xR : xr → SetTheory.PGame<VAR>i : xl<VAR>xL : xl → SetTheory.PGame<VAR>j : (xL i).RightMoves<GOAL>((xL i).moveRight j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u<VAR>xL : xl → SetTheory.PGame<VAR>i : xr<VAR>xR : xr → SetTheory.PGame<VAR>j : (xR i).RightMoves<GOAL>((xR i).moveRight j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u<VAR>xR : xr → SetTheory.PGame<VAR>i : xl<VAR>xL : xl → SetTheory.PGame<VAR>j : (xL i).LeftMoves<GOAL>((xL i).moveLeft j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u<VAR>xL : xl → SetTheory.PGame<VAR>i : xr<VAR>xR : xr → SetTheory.PGame<VAR>j : (xR i).LeftMoves<GOAL>((xR i).moveLeft j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
<GOAL>SetTheory.PGame.LeftMoves 0 = PEmpty.{u_1 + 1}
<GOAL>SetTheory.PGame.RightMoves 0 = PEmpty.{u_1 + 1}
<GOAL>SetTheory.PGame.LeftMoves 1 = PUnit.{u_1 + 1}
<VAR>x : SetTheory.PGame.LeftMoves 1<GOAL>SetTheory.PGame.moveLeft 1 x = 0
<GOAL>SetTheory.PGame.RightMoves 1 = PEmpty.{u_1 + 1}
<VAR>x y : SetTheory.PGame<GOAL>¬x ≤ y ↔ y.LF x
<VAR>x y : SetTheory.PGame<GOAL>¬x.LF y ↔ y ≤ x
<VAR>x y : SetTheory.PGame<GOAL>x ≤ y → ¬y.LF x
<VAR>x y : SetTheory.PGame<GOAL>x.LF y → ¬y ≤ x
<VAR>x y : SetTheory.PGame<GOAL>x ≤ y ↔ (∀ (i : x.LeftMoves), (x.moveLeft i).LF y) ∧ ∀ (j : y.RightMoves), x.LF (y.moveRight j)
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yl yr : Type u_1<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<GOAL>SetTheory.PGame.mk xl xr xL xR ≤ SetTheory.PGame.mk yl yr yL yR ↔ (∀ (i : xl), (xL i).LF (SetTheory.PGame.mk yl yr yL yR)) ∧ ∀ (j : yr), (SetTheory.PGame.mk xl xr xL xR).LF (yR j)
<VAR>x y : SetTheory.PGame<VAR>h₁ : ∀ (i : x.LeftMoves), (x.moveLeft i).LF y<VAR>h₂ : ∀ (j : y.RightMoves), x.LF (y.moveRight j)<GOAL>x ≤ y
<VAR>x y : SetTheory.PGame<GOAL>x.LF y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yl yr : Type u_1<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<GOAL>(SetTheory.PGame.mk xl xr xL xR).LF (SetTheory.PGame.mk yl yr yL yR) ↔ (∃ i, SetTheory.PGame.mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ SetTheory.PGame.mk yl yr yL yR
<VAR>x y : SetTheory.PGame<GOAL>x ≤ y ∨ y.LF x
<VAR>x y : SetTheory.PGame<VAR>h : x ≤ y<VAR>i : x.LeftMoves<GOAL>(x.moveLeft i).LF y
<VAR>x y : SetTheory.PGame<VAR>h : x ≤ y<VAR>j : y.RightMoves<GOAL>x.LF (y.moveRight j)
<VAR>x y : SetTheory.PGame<VAR>j : x.RightMoves<VAR>h : x.moveRight j ≤ y<GOAL>x.LF y
<VAR>x y : SetTheory.PGame<VAR>i : y.LeftMoves<VAR>h : x ≤ y.moveLeft i<GOAL>x.LF y
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>y : SetTheory.PGame<GOAL>SetTheory.PGame.mk xl xr xL xR ≤ y → ∀ (i : xl), (xL i).LF y
<VAR>x : SetTheory.PGame<VAR>yl yr : Type u_1<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<GOAL>x ≤ SetTheory.PGame.mk yl yr yL yR → ∀ (j : yr), x.LF (yR j)
<VAR>xl xr : Type u_1<VAR>y : SetTheory.PGame<VAR>j : xr<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<GOAL>xR j ≤ y → (SetTheory.PGame.mk xl xr xL xR).LF y
<VAR>x : SetTheory.PGame<VAR>yl yr : Type u_1<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : yl<GOAL>x ≤ yL i → x.LF (SetTheory.PGame.mk yl yr yL yR)
<VAR>x y z : SetTheory.PGame<VAR>h₁ : ∀ {i : x.LeftMoves}, y ≤ z → z ≤ x.moveLeft i → y ≤ x.moveLeft i<VAR>h₂ : ∀ {j : z.RightMoves}, z.moveRight j ≤ x → x ≤ y → z.moveRight j ≤ y<VAR>hxy : x ≤ y<VAR>hyz : y ≤ z<GOAL>x ≤ z
<VAR>x y : SetTheory.PGame<GOAL>x < y ↔ x ≤ y ∧ x.LF y
<VAR>x y : SetTheory.PGame<VAR>h₁ : x ≤ y<VAR>h₂ : x.LF y<GOAL>x < y
<VAR>x y : SetTheory.PGame<VAR>h : x < y<GOAL>x.LF y
<VAR>x : SetTheory.PGame<GOAL>¬x.LF x
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x ≤ y<VAR>h₂ : y.LF z<GOAL>x.LF z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x.LF y<VAR>h₂ : y ≤ z<GOAL>x.LF z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x < y<VAR>h₂ : y.LF z<GOAL>x.LF z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x.LF y<VAR>h₂ : y < z<GOAL>x.LF z
<VAR>x : SetTheory.PGame<VAR>i : x.LeftMoves<GOAL>(x.moveLeft i).LF x
<VAR>x : SetTheory.PGame<VAR>j : x.RightMoves<GOAL>x.LF (x.moveRight j)
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>i : xl<GOAL>(xL i).LF (SetTheory.PGame.mk xl xr xL xR)
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>j : xr<GOAL>(SetTheory.PGame.mk xl xr xL xR).LF (xR j)
<VAR>x y : SetTheory.PGame<VAR>h₁ : ∀ (i : x.LeftMoves), x.moveLeft i < y<VAR>h₂ : ∀ (j : y.RightMoves), x < y.moveRight j<GOAL>x ≤ y
<VAR>x y : SetTheory.PGame<GOAL>x ≤ y ↔ (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧ ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j
<VAR>x y : SetTheory.PGame<GOAL>x.LF y ↔ (∃ i, (∀ (i' : x.LeftMoves), (x.moveLeft i').LF (y.moveLeft i)) ∧ ∀ (j : (y.moveLeft i).RightMoves), x.LF ((y.moveLeft i).moveRight j)) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF y) ∧ ∀ (j' : y.RightMoves), (x.moveRight j).LF (y.moveRight j')
<VAR>x : SetTheory.PGame<GOAL>0 ≤ x ↔ ∀ (j : x.RightMoves), SetTheory.PGame.LF 0 (x.moveRight j)
<VAR>x : SetTheory.PGame<GOAL>x ≤ 0 ↔ ∀ (i : x.LeftMoves), (x.moveLeft i).LF 0
<VAR>x : SetTheory.PGame<GOAL>SetTheory.PGame.LF 0 x ↔ ∃ i, 0 ≤ x.moveLeft i
<VAR>x : SetTheory.PGame<GOAL>x.LF 0 ↔ ∃ j, x.moveRight j ≤ 0
<VAR>x : SetTheory.PGame<GOAL>0 ≤ x ↔ ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i
<VAR>x : SetTheory.PGame<GOAL>x ≤ 0 ↔ ∀ (i : x.LeftMoves), ∃ j, (x.moveLeft i).moveRight j ≤ 0
<VAR>x : SetTheory.PGame<GOAL>SetTheory.PGame.LF 0 x ↔ ∃ i, ∀ (j : (x.moveLeft i).RightMoves), SetTheory.PGame.LF 0 ((x.moveLeft i).moveRight j)
<VAR>x : SetTheory.PGame<GOAL>x.LF 0 ↔ ∃ j, ∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF 0
<VAR>x : SetTheory.PGame<VAR>IsEmpty x.RightMoves<GOAL>0 ≤ x
<VAR>x : SetTheory.PGame<VAR>IsEmpty x.LeftMoves<GOAL>x ≤ 0
<VAR>x : SetTheory.PGame<VAR>h : x ≤ 0<VAR>i : x.LeftMoves<GOAL>(x.moveLeft i).moveRight (SetTheory.PGame.rightResponse h i) ≤ 0
<VAR>x : SetTheory.PGame<VAR>h : 0 ≤ x<VAR>j : x.RightMoves<GOAL>0 ≤ (x.moveRight j).moveLeft (SetTheory.PGame.leftResponse h j)
<VAR>ι : Type u_1<VAR>Small.{u, u_1} ι<VAR>f : ι → SetTheory.PGame<GOAL>BddAbove (Set.range f)
<VAR>s : Set SetTheory.PGame<VAR>Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>ι : Type u_1<VAR>Small.{u, u_1} ι<VAR>f : ι → SetTheory.PGame<GOAL>BddBelow (Set.range f)
<VAR>s : Set SetTheory.PGame<VAR>Small.{u, u + 1} ↑s<GOAL>BddBelow s
<VAR>x y : SetTheory.PGame<GOAL>x ≈ y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : SetTheory.PGame<VAR>h : x ≈ y<GOAL>x ≤ y
<VAR>x y : SetTheory.PGame<VAR>h : x ≈ y<GOAL>y ≤ x
<VAR>x : SetTheory.PGame<GOAL>x ≈ x
<VAR>x y : SetTheory.PGame<GOAL>x ≈ y → y ≈ x
<VAR>x y z : SetTheory.PGame<GOAL>x ≈ y → y ≈ z → x ≈ z
<VAR>x y : SetTheory.PGame<GOAL>x ≈ y ↔ y ≈ x
<VAR>x y : SetTheory.PGame<VAR>h : x = y<GOAL>x ≈ y
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x ≤ y<VAR>h₂ : y ≈ z<GOAL>x ≤ z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x ≈ y<GOAL>y ≤ z → x ≤ z
<VAR>x y : SetTheory.PGame<VAR>h : x.LF y<GOAL>¬x ≈ y
<VAR>x y : SetTheory.PGame<VAR>h : x.LF y<GOAL>¬y ≈ x
<VAR>x y : SetTheory.PGame<VAR>h : x.LF y<GOAL>¬y < x
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<VAR>h : x₁ ≤ y₁<GOAL>x₂ ≤ y₂
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁ ≤ y₁ ↔ x₂ ≤ y₂
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<GOAL>x₁ ≤ y ↔ x₂ ≤ y
<VAR>x y₁ y₂ : SetTheory.PGame<VAR>hy : y₁ ≈ y₂<GOAL>x ≤ y₁ ↔ x ≤ y₂
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁.LF y₁ ↔ x₂.LF y₂
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁.LF y₁ → x₂.LF y₂
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<GOAL>x₁.LF y ↔ x₂.LF y
<VAR>x y₁ y₂ : SetTheory.PGame<VAR>hy : y₁ ≈ y₂<GOAL>x.LF y₁ ↔ x.LF y₂
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x.LF y<VAR>h₂ : y ≈ z<GOAL>x.LF z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x ≈ y<GOAL>y.LF z → x.LF z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x < y<VAR>h₂ : y ≈ z<GOAL>x < z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x ≈ y<GOAL>y < z → x < z
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<VAR>h : x₁ < y₁<GOAL>x₂ < y₂
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁ < y₁ ↔ x₂ < y₂
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<GOAL>x₁ < y ↔ x₂ < y
<VAR>x y₁ y₂ : SetTheory.PGame<VAR>hy : y₁ ≈ y₂<GOAL>x < y₁ ↔ x < y₂
<VAR>x y : SetTheory.PGame<VAR>h : x ≤ y<GOAL>x < y ∨ x ≈ y
<VAR>x y : SetTheory.PGame<GOAL>x.LF y ∨ x ≈ y ∨ y.LF x
<VAR>y₁ y₂ : SetTheory.PGame<GOAL>y₁ ≈ y₂ ↔ ∀ (x₁ : SetTheory.PGame), x₁ ≈ y₁ ↔ x₁ ≈ y₂
<VAR>x₁ x₂ : SetTheory.PGame<GOAL>x₁ ≈ x₂ ↔ ∀ (y₁ : SetTheory.PGame), x₁ ≈ y₁ ↔ x₂ ≈ y₁
<VAR>x y : SetTheory.PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)<VAR>hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)<GOAL>x ≈ y
<VAR>x y : SetTheory.PGame<GOAL>x.Fuzzy y → y.Fuzzy x
<VAR>x y : SetTheory.PGame<GOAL>x.Fuzzy y ↔ y.Fuzzy x
<VAR>x : SetTheory.PGame<GOAL>¬x.Fuzzy x
<VAR>x y : SetTheory.PGame<GOAL>x.LF y ↔ x < y ∨ x.Fuzzy y
<VAR>x y : SetTheory.PGame<VAR>h : x.Fuzzy y<GOAL>x.LF y
<VAR>x y : SetTheory.PGame<GOAL>x.LF y → x < y ∨ x.Fuzzy y
<VAR>x y : SetTheory.PGame<VAR>h : x.Fuzzy y<GOAL>¬x ≈ y
<VAR>x y : SetTheory.PGame<VAR>h : x.Fuzzy y<GOAL>¬y ≈ x
<VAR>x y : SetTheory.PGame<VAR>h : x ≤ y<GOAL>¬x.Fuzzy y
<VAR>x y : SetTheory.PGame<VAR>h : y ≤ x<GOAL>¬x.Fuzzy y
<VAR>x y : SetTheory.PGame<VAR>h : x ≈ y<GOAL>¬x.Fuzzy y
<VAR>x y : SetTheory.PGame<VAR>h : x ≈ y<GOAL>¬y.Fuzzy x
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁.Fuzzy y₁ ↔ x₂.Fuzzy y₂
<VAR>x₁ y₁ x₂ y₂ : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁.Fuzzy y₁ → x₂.Fuzzy y₂
<VAR>x₁ x₂ y : SetTheory.PGame<VAR>hx : x₁ ≈ x₂<GOAL>x₁.Fuzzy y ↔ x₂.Fuzzy y
<VAR>x y₁ y₂ : SetTheory.PGame<VAR>hy : y₁ ≈ y₂<GOAL>x.Fuzzy y₁ ↔ x.Fuzzy y₂
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x.Fuzzy y<VAR>h₂ : y ≈ z<GOAL>x.Fuzzy z
<VAR>x y z : SetTheory.PGame<VAR>h₁ : x ≈ y<VAR>h₂ : y.Fuzzy z<GOAL>x.Fuzzy z
<VAR>x y : SetTheory.PGame<GOAL>x < y ∨ x ≈ y ∨ y < x ∨ x.Fuzzy y
<VAR>x y : SetTheory.PGame<GOAL>x < y ∨ x ≈ y ∨ y.LF x
<VAR>x y : SetTheory.PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))<VAR>hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))<GOAL>(SetTheory.PGame.Relabelling.mk L R hL hR).leftMovesEquiv = L
<VAR>x y : SetTheory.PGame<VAR>L : y.LeftMoves ≃ x.LeftMoves<VAR>R : y.RightMoves ≃ x.RightMoves<VAR>hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)<VAR>hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)<GOAL>(SetTheory.PGame.Relabelling.mk' L R hL hR).leftMovesEquiv = L.symm
<VAR>x y : SetTheory.PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))<VAR>hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))<GOAL>(SetTheory.PGame.Relabelling.mk L R hL hR).rightMovesEquiv = R
<VAR>x y : SetTheory.PGame<VAR>L : y.LeftMoves ≃ x.LeftMoves<VAR>R : y.RightMoves ≃ x.RightMoves<VAR>hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)<VAR>hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)<GOAL>(SetTheory.PGame.Relabelling.mk' L R hL hR).rightMovesEquiv = R.symm
<VAR>x y : SetTheory.PGame<VAR>r : x.Relabelling y<GOAL>x ≤ y
<VAR>x y : SetTheory.PGame<VAR>r : x.Relabelling y<GOAL>y ≤ x
<VAR>x y : SetTheory.PGame<VAR>r : x.Relabelling y<GOAL>x ≈ y
<VAR>x : SetTheory.PGame<VAR>IsEmpty x.LeftMoves<VAR>IsEmpty x.RightMoves<GOAL>x ≈ 0
<VAR>x : SetTheory.PGame<VAR>xl' xr' : Type u_1<VAR>el : xl' ≃ x.LeftMoves<VAR>er : xr' ≃ x.RightMoves<VAR>i : xl'<GOAL>(SetTheory.PGame.relabel el er).moveLeft i = x.moveLeft (el i)
<VAR>x : SetTheory.PGame<VAR>xl' xr' : Type u_1<VAR>el : xl' ≃ x.LeftMoves<VAR>er : xr' ≃ x.RightMoves<VAR>i : x.LeftMoves<GOAL>(SetTheory.PGame.relabel el er).moveLeft (el.symm i) = x.moveLeft i
<VAR>x : SetTheory.PGame<VAR>xl' xr' : Type u_1<VAR>el : xl' ≃ x.LeftMoves<VAR>er : xr' ≃ x.RightMoves<VAR>j : xr'<GOAL>(SetTheory.PGame.relabel el er).moveRight j = x.moveRight (er j)
<VAR>x : SetTheory.PGame<VAR>xl' xr' : Type u_1<VAR>el : xl' ≃ x.LeftMoves<VAR>er : xr' ≃ x.RightMoves<VAR>j : x.RightMoves<GOAL>(SetTheory.PGame.relabel el er).moveRight (er.symm j) = x.moveRight j
<VAR>xl xr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<GOAL>-SetTheory.PGame.mk xl xr xL xR = SetTheory.PGame.mk xr xl (fun j => -xR j) fun i => -xL i
<VAR>L R : List SetTheory.PGame<GOAL>-SetTheory.PGame.ofLists L R = SetTheory.PGame.ofLists (List.map (fun x => -x) R) (List.map (fun x => -x) L)
<VAR>x y : SetTheory.PGame<GOAL>x.IsOption (-y) ↔ (-x).IsOption y
<VAR>x y : SetTheory.PGame<GOAL>(-x).IsOption (-y) ↔ x.IsOption y
<VAR>x : SetTheory.PGame<GOAL>(-x).LeftMoves = x.RightMoves
<VAR>x : SetTheory.PGame<GOAL>(-x).RightMoves = x.LeftMoves
<VAR>x : SetTheory.PGame<VAR>i : x.RightMoves<GOAL>(-x).moveLeft (SetTheory.PGame.toLeftMovesNeg i) = -x.moveRight i
<VAR>x : SetTheory.PGame<VAR>i : (-x).LeftMoves<GOAL>(-x).moveLeft i = -x.moveRight (SetTheory.PGame.toLeftMovesNeg.symm i)
<VAR>x : SetTheory.PGame<VAR>i : x.LeftMoves<GOAL>(-x).moveRight (SetTheory.PGame.toRightMovesNeg i) = -x.moveLeft i
<VAR>x : SetTheory.PGame<VAR>i : (-x).RightMoves<GOAL>(-x).moveRight i = -x.moveLeft (SetTheory.PGame.toRightMovesNeg.symm i)
<VAR>x : SetTheory.PGame<VAR>i : (-x).RightMoves<GOAL>x.moveLeft (SetTheory.PGame.toRightMovesNeg.symm i) = -(-x).moveRight i
<VAR>x : SetTheory.PGame<VAR>i : x.LeftMoves<GOAL>x.moveLeft i = -(-x).moveRight (SetTheory.PGame.toRightMovesNeg i)
<VAR>x : SetTheory.PGame<VAR>i : (-x).LeftMoves<GOAL>x.moveRight (SetTheory.PGame.toLeftMovesNeg.symm i) = -(-x).moveLeft i
<VAR>x : SetTheory.PGame<VAR>i : x.RightMoves<GOAL>x.moveRight i = -(-x).moveLeft (SetTheory.PGame.toLeftMovesNeg i)
<VAR>x y : SetTheory.PGame<GOAL>(-y ≤ -x ↔ x ≤ y) ∧ ((-y).LF (-x) ↔ x.LF y)
<VAR>x y : SetTheory.PGame<GOAL>-y ≤ -x ↔ x ≤ y
<VAR>x y : SetTheory.PGame<GOAL>(-y).LF (-x) ↔ x.LF y
<VAR>x y : SetTheory.PGame<GOAL>-y < -x ↔ x < y
<VAR>x y : SetTheory.PGame<GOAL>-x ≈ -y ↔ x ≈ y
<VAR>x y : SetTheory.PGame<GOAL>(-x).Fuzzy (-y) ↔ x.Fuzzy y
<VAR>x y : SetTheory.PGame<GOAL>-y ≤ x ↔ -x ≤ y
<VAR>x y : SetTheory.PGame<GOAL>(-y).LF x ↔ (-x).LF y
<VAR>x y : SetTheory.PGame<GOAL>-y < x ↔ -x < y
<VAR>x y : SetTheory.PGame<GOAL>-x ≈ y ↔ x ≈ -y
<VAR>x y : SetTheory.PGame<GOAL>(-x).Fuzzy y ↔ x.Fuzzy (-y)
<VAR>x y : SetTheory.PGame<GOAL>y ≤ -x ↔ x ≤ -y
<VAR>x y : SetTheory.PGame<GOAL>y.LF (-x) ↔ x.LF (-y)
<VAR>x y : SetTheory.PGame<GOAL>y < -x ↔ x < -y
<VAR>x : SetTheory.PGame<GOAL>-x ≤ 0 ↔ 0 ≤ x
<VAR>x : SetTheory.PGame<GOAL>0 ≤ -x ↔ x ≤ 0
<VAR>x : SetTheory.PGame<GOAL>(-x).LF 0 ↔ SetTheory.PGame.LF 0 x
<VAR>x : SetTheory.PGame<GOAL>SetTheory.PGame.LF 0 (-x) ↔ x.LF 0
<VAR>x : SetTheory.PGame<GOAL>-x < 0 ↔ 0 < x
<VAR>x : SetTheory.PGame<GOAL>0 < -x ↔ x < 0
<VAR>x : SetTheory.PGame<GOAL>-x ≈ 0 ↔ x ≈ 0
<VAR>x : SetTheory.PGame<GOAL>(-x).Fuzzy 0 ↔ x.Fuzzy 0
<VAR>x : SetTheory.PGame<GOAL>0 ≈ -x ↔ 0 ≈ x
<VAR>x : SetTheory.PGame<GOAL>SetTheory.PGame.Fuzzy 0 (-x) ↔ SetTheory.PGame.Fuzzy 0 x
<VAR>x : SetTheory.PGame<GOAL>x + 0 ≈ x
<VAR>x : SetTheory.PGame<GOAL>0 + x ≈ x
<VAR>x y : SetTheory.PGame<GOAL>(x + y).LeftMoves = (x.LeftMoves ⊕ y.LeftMoves)
<VAR>x y : SetTheory.PGame<GOAL>(x + y).RightMoves = (x.RightMoves ⊕ y.RightMoves)
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xl<GOAL>(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveLeft (Sum.inl i) = (SetTheory.PGame.mk xl xr xL xR).moveLeft i + SetTheory.PGame.mk yl yr yL yR
<VAR>x : SetTheory.PGame<VAR>y : SetTheory.PGame<VAR>i : x.LeftMoves<GOAL>(x + y).moveLeft (SetTheory.PGame.toLeftMovesAdd (Sum.inl i)) = x.moveLeft i + y
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : xr<GOAL>(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveRight (Sum.inl i) = (SetTheory.PGame.mk xl xr xL xR).moveRight i + SetTheory.PGame.mk yl yr yL yR
<VAR>x : SetTheory.PGame<VAR>y : SetTheory.PGame<VAR>i : x.RightMoves<GOAL>(x + y).moveRight (SetTheory.PGame.toRightMovesAdd (Sum.inl i)) = x.moveRight i + y
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : yl<GOAL>(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveLeft (Sum.inr i) = SetTheory.PGame.mk xl xr xL xR + (SetTheory.PGame.mk yl yr yL yR).moveLeft i
<VAR>x : SetTheory.PGame<VAR>y : SetTheory.PGame<VAR>i : y.LeftMoves<GOAL>(x + y).moveLeft (SetTheory.PGame.toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i
<VAR>xl xr yl yr : Type u_1<VAR>xL : xl → SetTheory.PGame<VAR>xR : xr → SetTheory.PGame<VAR>yL : yl → SetTheory.PGame<VAR>yR : yr → SetTheory.PGame<VAR>i : yr<GOAL>(SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveRight (Sum.inr i) = SetTheory.PGame.mk xl xr xL xR + (SetTheory.PGame.mk yl yr yL yR).moveRight i
<VAR>x : SetTheory.PGame<VAR>y : SetTheory.PGame<VAR>i : y.RightMoves<GOAL>(x + y).moveRight (SetTheory.PGame.toRightMovesAdd (Sum.inr i)) = x + y.moveRight i
<VAR>x y : SetTheory.PGame<VAR>k : (x + y).LeftMoves<VAR>P : (x + y).LeftMoves → Prop<VAR>hl : ∀ (i : x.LeftMoves), P (SetTheory.PGame.toLeftMovesAdd (Sum.inl i))<VAR>hr : ∀ (i : y.LeftMoves), P (SetTheory.PGame.toLeftMovesAdd (Sum.inr i))<GOAL>P k
<VAR>x y : SetTheory.PGame<VAR>k : (x + y).RightMoves<VAR>P : (x + y).RightMoves → Prop<VAR>hl : ∀ (j : x.RightMoves), P (SetTheory.PGame.toRightMovesAdd (Sum.inl j))<VAR>hr : ∀ (j : y.RightMoves), P (SetTheory.PGame.toRightMovesAdd (Sum.inr j))<GOAL>P k
<VAR>x : SetTheory.PGame<GOAL>x - 0 = x + 0
<VAR>x y : SetTheory.PGame<GOAL>-(x + y) ≤ -x + -y
<VAR>x y : SetTheory.PGame<GOAL>x + y ≤ y + x
<VAR>x y : SetTheory.PGame<GOAL>x + y ≈ y + x
<VAR>x y z : SetTheory.PGame<GOAL>x + y + z ≈ x + (y + z)
<VAR>x : SetTheory.PGame<GOAL>-x + x ≤ 0
<VAR>x : SetTheory.PGame<GOAL>0 ≤ -x + x
<VAR>x : SetTheory.PGame<GOAL>-x + x ≈ 0
<VAR>x : SetTheory.PGame<GOAL>x + -x ≤ 0
<VAR>x : SetTheory.PGame<GOAL>0 ≤ x + -x
<VAR>x : SetTheory.PGame<GOAL>x + -x ≈ 0
<VAR>x : SetTheory.PGame<GOAL>x - x ≈ 0
<VAR>x y z : SetTheory.PGame<GOAL>x ≤ y → x + z ≤ y + z
<VAR>y z : SetTheory.PGame<VAR>h : y.LF z<VAR>x : SetTheory.PGame<GOAL>(y + x).LF (z + x)
<VAR>y z : SetTheory.PGame<VAR>h : y.LF z<VAR>x : SetTheory.PGame<GOAL>(x + y).LF (x + z)
<VAR>w x y z : SetTheory.PGame<VAR>hwx : w.LF x<VAR>hyz : y ≤ z<GOAL>(w + y).LF (x + z)
<VAR>w x y z : SetTheory.PGame<VAR>hwx : w ≤ x<VAR>hyz : y.LF z<GOAL>(w + y).LF (x + z)
<VAR>w x y z : SetTheory.PGame<VAR>h₁ : w ≈ x<VAR>h₂ : y ≈ z<GOAL>w + y ≈ x + z
<VAR>x y z : SetTheory.PGame<VAR>h : x ≈ y<GOAL>x + z ≈ y + z
<VAR>x y z : SetTheory.PGame<GOAL>y ≈ z → x + y ≈ x + z
<VAR>w x y z : SetTheory.PGame<VAR>h₁ : w ≈ x<VAR>h₂ : y ≈ z<GOAL>w - y ≈ x - z
<VAR>x y z : SetTheory.PGame<VAR>h : x ≈ y<GOAL>x - z ≈ y - z
<VAR>x y z : SetTheory.PGame<GOAL>y ≈ z → x - y ≈ x - z
<VAR>x y : SetTheory.PGame<GOAL>x ≤ y ↔ 0 ≤ y - x
<VAR>x y : SetTheory.PGame<GOAL>x.LF y ↔ SetTheory.PGame.LF 0 (y - x)
<VAR>x y : SetTheory.PGame<GOAL>x < y ↔ 0 < y - x
<VAR>x x' : SetTheory.PGame<GOAL>x ≤ x.insertLeft x'
<VAR>x x' : SetTheory.PGame<VAR>h : x'.LF x<GOAL>x.insertLeft x' ≈ x
<VAR>x x' : SetTheory.PGame<GOAL>(-x).insertRight (-x') = -x.insertLeft x'
<VAR>x x' : SetTheory.PGame<GOAL>(-x).insertLeft (-x') = -x.insertRight x'
<VAR>x x' : SetTheory.PGame<GOAL>x.insertRight x' ≤ x
<VAR>x x' : SetTheory.PGame<VAR>h : x.LF x'<GOAL>x.insertRight x' ≈ x
<VAR>x x' x'' : SetTheory.PGame<GOAL>(x.insertLeft x').insertRight x'' = (x.insertRight x'').insertLeft x'
<GOAL>SetTheory.PGame.star.LeftMoves = PUnit.{u_1 + 1}
<GOAL>SetTheory.PGame.star.RightMoves = PUnit.{u_1 + 1}
<VAR>x : SetTheory.PGame.star.LeftMoves<GOAL>SetTheory.PGame.star.moveLeft x = 0
<VAR>x : SetTheory.PGame.star.RightMoves<GOAL>SetTheory.PGame.star.moveRight x = 0
<GOAL>-SetTheory.PGame.star = SetTheory.PGame.star
<VAR>n : ℕ<GOAL>catalan (n + 1) = ∑ i : Fin n.succ, catalan ↑i * catalan (n - ↑i)
<VAR>n : ℕ<GOAL>catalan (n + 1) = ∑ ij ∈ Finset.antidiagonal n, catalan ij.1 * catalan ij.2
<VAR>n i : ℕ<VAR>h : i ≤ n<GOAL>gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n : ℕ<GOAL>gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)
<VAR>n : ℕ<GOAL>(n + 1) * catalan n = n.centralBinom
<GOAL>Tree.treesOfNumNodesEq 0 = {Tree.nil}