ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.left b<GOAL>2 ≤ Finset.card b
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.right b<GOAL>2 ≤ Finset.card b
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.left b<GOAL>Finset.card (SetTheory.PGame.Domineering.moveLeft b m) + 2 = Finset.card b
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.right b<GOAL>Finset.card (SetTheory.PGame.Domineering.moveRight b m) + 2 = Finset.card b
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.left b<GOAL>Finset.card (SetTheory.PGame.Domineering.moveLeft b m) / 2 < Finset.card b / 2
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.right b<GOAL>Finset.card (SetTheory.PGame.Domineering.moveRight b m) / 2 < Finset.card b / 2
<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>m n : ℕ∞<GOAL>↑m < ↑n ↔ m < n
<VAR>m : ℕ∞<GOAL>↑m < Cardinal.aleph0 ↔ m < ⊤
<VAR>m : ℕ∞<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n
<VAR>m : ℕ<VAR>m.AtLeastTwo<VAR>n : ℕ∞<GOAL>OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n
<VAR>m n : ℕ∞<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>n : ℕ∞<GOAL>↑n ≤ Cardinal.aleph0
<VAR>m : ℕ∞<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n
<VAR>m : ℕ<VAR>m.AtLeastTwo<VAR>n : ℕ∞<GOAL>OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n
<VAR>m n : ℕ∞<GOAL>↑m = ↑n ↔ m = n
<VAR>m : ℕ∞<GOAL>0 = ↑m ↔ m = 0
<VAR>m : ℕ∞<GOAL>1 = ↑m ↔ m = 1
<VAR>m : ℕ∞<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
<VAR>m : ℕ<VAR>n : ℕ∞<VAR>m.AtLeastTwo<GOAL>OfNat.ofNat m = ↑n ↔ OfNat.ofNat m = n
<VAR>m : ℕ∞<GOAL>Cardinal.lift.{u, v} ↑m = ↑m
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>Cardinal.lift.{u, v} x < ↑m ↔ x < ↑m
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>Cardinal.lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>Cardinal.lift.{u, v} x = ↑m ↔ x = ↑m
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>↑m < Cardinal.lift.{u, v} x ↔ ↑m < x
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>↑m ≤ Cardinal.lift.{u, v} x ↔ ↑m ≤ x
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>↑m = Cardinal.lift.{u, v} x ↔ ↑m = x
<GOAL>Set.range Cardinal.ofENat = Set.Iic Cardinal.aleph0
<VAR>n : ℕ<GOAL>(↑n).toENatAux = ↑n
<VAR>a : Cardinal.{u_1}<VAR>ha : Cardinal.aleph0 ≤ a<GOAL>a.toENatAux = ⊤
<VAR>n : ℕ∞<GOAL>(↑n).toENatAux = n
<VAR>x : Cardinal.{u_1}<GOAL>x.toENatAux = 0 ↔ x = 0
<GOAL>GaloisConnection Cardinal.ofENat ⇑Cardinal.toENat
<VAR>n : ℕ∞<GOAL>Cardinal.toENat ↑n = n
<GOAL>⇑Cardinal.toENat ∘ Cardinal.ofENat = id
<GOAL>StrictMonoOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
<GOAL>Set.InjOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
<VAR>a : Cardinal.{u_1}<GOAL>↑(Cardinal.toENat a) ≤ a
<VAR>a : Cardinal.{u_1}<GOAL>↑(Cardinal.toENat a) = a ↔ a ≤ Cardinal.aleph0
<VAR>n : ℕ<GOAL>Cardinal.toENat ↑n = ↑n
<VAR>a : Cardinal.{u_1}<VAR>n : ℕ<GOAL>Cardinal.toENat a ≤ ↑n ↔ a ≤ ↑n
<VAR>a : Cardinal.{u_1}<VAR>n : ℕ<GOAL>Cardinal.toENat a = ↑n ↔ a = ↑n
<VAR>a : Cardinal.{u_1}<GOAL>Cardinal.toENat a = 0 ↔ a = 0
<VAR>a : Cardinal.{u_1}<GOAL>Cardinal.toENat a ≤ 1 ↔ a ≤ 1
<VAR>a : Cardinal.{u_1}<GOAL>Cardinal.toENat a = 1 ↔ a = 1
<VAR>a : Cardinal.{u_1}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.toENat a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n
<VAR>a : Cardinal.{u_1}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.toENat a = OfNat.ofNat n ↔ a = OfNat.ofNat n
<VAR>a : Cardinal.{u_1}<GOAL>Cardinal.toENat a = ⊤ ↔ Cardinal.aleph0 ≤ a
<VAR>a : Cardinal.{v}<GOAL>Cardinal.toENat (Cardinal.lift.{u, v} a) = Cardinal.toENat a
<VAR>m : ℕ∞<GOAL>Cardinal.aleph0 + ↑m = Cardinal.aleph0
<VAR>m : ℕ∞<GOAL>↑m + Cardinal.aleph0 = Cardinal.aleph0
<VAR>m : ℕ∞<VAR>hm : m ≠ 0<GOAL>↑m * Cardinal.aleph0 = Cardinal.aleph0
<VAR>m : ℕ∞<VAR>hm : m ≠ 0<GOAL>Cardinal.aleph0 * ↑m = Cardinal.aleph0
<VAR>m n : ℕ∞<GOAL>↑(m * n) = ↑m * ↑n
<VAR>a : Cardinal.{u}<GOAL>IsUnit a ↔ a = 1
<VAR>a b : Cardinal.{u_1}<GOAL>b ≠ 0 → a ∣ b → a ≤ b
<VAR>a b : Cardinal.{u}<VAR>ha : a ≠ 0<VAR>h : a ≤ b<VAR>hb : Cardinal.aleph0 ≤ b<GOAL>a ∣ b
<VAR>a : Cardinal.{u}<VAR>ha : Cardinal.aleph0 ≤ a<GOAL>Prime a
<VAR>a : Cardinal.{u}<VAR>ha : Cardinal.aleph0 ≤ a<GOAL>¬Irreducible a
<VAR>n m : ℕ<GOAL>↑n ∣ ↑m ↔ n ∣ m
<VAR>n : ℕ<GOAL>Prime ↑n ↔ Nat.Prime n
<VAR>a : Cardinal.{u_1}<GOAL>Prime a ↔ Cardinal.aleph0 ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
<VAR>a : Cardinal.{u_1}<GOAL>IsPrimePow a ↔ Cardinal.aleph0 ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n
<VAR>α : Type u_1<VAR>A : α → PSet<GOAL>(PSet.mk α A).Type = α
<VAR>α : Type u_1<VAR>A : α → PSet<GOAL>(PSet.mk α A).Func = A
<VAR>x : PSet<GOAL>PSet.mk x.Type x.Func = x
<VAR>x : PSet<VAR>y : PSet<GOAL>x.Equiv y ↔ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)
<VAR>x : PSet<VAR>y : PSet<VAR>h : x.Equiv y<VAR>i : x.Type<GOAL>∃ j, (x.Func i).Equiv (y.Func j)
<VAR>x : PSet<VAR>y : PSet<VAR>h : x.Equiv y<VAR>j : y.Type<GOAL>∃ i, (x.Func i).Equiv (y.Func j)
<VAR>x : PSet<VAR>y : PSet<VAR>z : PSet<GOAL>x.Equiv y → z.Equiv y → x.Equiv z
<VAR>x : PSet<VAR>y : PSet<GOAL>x.Equiv y → y.Equiv x
<VAR>x : PSet<VAR>y : PSet<GOAL>x.Equiv y ↔ y.Equiv x
<VAR>x : PSet<VAR>y : PSet<VAR>z : PSet<VAR>h1 : x.Equiv y<VAR>h2 : y.Equiv z<GOAL>x.Equiv z
<VAR>x : PSet<VAR>y : PSet<VAR>IsEmpty x.Type<VAR>IsEmpty y.Type<GOAL>x.Equiv y
<VAR>x y : PSet<GOAL>x.Equiv y ↔ x ⊆ y ∧ y ⊆ x
<VAR>x y z : PSet<GOAL>x.Equiv y → (x ⊆ z ↔ y ⊆ z)
<VAR>x y z : PSet<GOAL>x.Equiv y → (z ⊆ x ↔ z ⊆ y)
<VAR>α : Type u<VAR>A : α → PSet<VAR>a : α<GOAL>A a ∈ PSet.mk α A
<VAR>x : PSet<VAR>i : x.Type<GOAL>x.Func i ∈ x
<VAR>x y : PSet<GOAL>(∀ (w : PSet), w ∈ x ↔ w ∈ y) → x.Equiv y
<VAR>x y : PSet<GOAL>x.Equiv y → ∀ {w : PSet}, w ∈ x ↔ w ∈ y
<VAR>x y : PSet<GOAL>x.Equiv y ↔ ∀ {w : PSet}, w ∈ x ↔ w ∈ y
<VAR>x y : PSet<GOAL>x.Equiv y → ∀ {w : PSet}, x ∈ w ↔ y ∈ w
<VAR>x y : PSet<GOAL>x.Equiv y → Acc (fun x x_1 => x ∈ x_1) y
<GOAL>WellFounded fun x x_1 => x ∈ x_1
<VAR>x y : PSet<GOAL>x ∈ y → y ∉ x
<VAR>a u : PSet<GOAL>a ∈ u.toSet ↔ a ∈ u
<VAR>u : PSet<GOAL>u.Nonempty ↔ ∃ x, x ∈ u
<VAR>x u : PSet<VAR>h : x ∈ u<GOAL>u.Nonempty
<VAR>u : PSet<GOAL>u.toSet.Nonempty ↔ u.Nonempty
<VAR>x : PSet<GOAL>Nonempty x.Type ↔ x.Nonempty
<VAR>x : PSet<VAR>h : Nonempty x.Type<GOAL>x.Nonempty
<VAR>x y : PSet<GOAL>x.Equiv y ↔ x.toSet = y.toSet
<VAR>x : PSet<GOAL>∅ ⊆ x
<VAR>x : PSet<VAR>IsEmpty x.Type<GOAL>x.Equiv ∅
<VAR>x y : PSet<GOAL>y ∈ x.powerset ↔ y ⊆ x
<VAR>x y : PSet<GOAL>y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
<VAR>x : PSet<GOAL>(⋃₀ x).toSet = ⋃₀ (PSet.toSet '' x.toSet)
<VAR>f : PSet → PSet<VAR>H : ∀ (x y : PSet), x.Equiv y → (f x).Equiv (f y)<VAR>x y : PSet<GOAL>y ∈ PSet.image f x ↔ ∃ z ∈ x, y.Equiv (f z)
<VAR>x : PSet<GOAL>x.Lift ∈ PSet.embed
<VAR>a : PSet<VAR>n : ℕ<GOAL>PSet.Arity.Equiv (Function.OfArity.const PSet a n) (Function.OfArity.const PSet a n)
<VAR>n : ℕ<VAR>a : PSet.Resp n<GOAL>a.Equiv a
<VAR>n : ℕ<VAR>a b c : PSet.Resp n<GOAL>a.Equiv b → c.Equiv b → a.Equiv c
<VAR>n : ℕ<VAR>a b : PSet.Resp n<GOAL>a.Equiv b → b.Equiv a
<VAR>n : ℕ<VAR>x y z : PSet.Resp n<VAR>h1 : x.Equiv y<VAR>h2 : y.Equiv z<GOAL>x.Equiv z
<VAR>n : ℕ<VAR>f : PSet.Resp (n + 1)<VAR>x : PSet<GOAL>PSet.Resp.eval (n + 1) f ⟦x⟧ = PSet.Resp.eval n (f.f x)
<VAR>n : ℕ<VAR>s : Function.OfArity ZFSet ZFSet n<VAR>H : PSet.Definable n s<GOAL>PSet.Resp.eval n (PSet.Definable.Resp s) = s
<VAR>x : PSet<GOAL>⟦x⟧ = ZFSet.mk x
<VAR>x : ZFSet<GOAL>ZFSet.mk (Quotient.out x) = x
<VAR>x y : PSet<GOAL>ZFSet.mk x = ZFSet.mk y ↔ x.Equiv y
<VAR>x y : PSet<VAR>h : x.Equiv y<GOAL>ZFSet.mk x = ZFSet.mk y
<VAR>x y : PSet<GOAL>ZFSet.mk x = ZFSet.mk y → x.Equiv y
<VAR>n : ℕ<VAR>f : PSet.Resp (n + 1)<VAR>x : PSet<GOAL>PSet.Resp.eval (n + 1) f (ZFSet.mk x) = PSet.Resp.eval n (f.f x)
<VAR>x y : PSet<GOAL>ZFSet.mk x ∈ ZFSet.mk y ↔ x ∈ y
<VAR>a u : ZFSet<GOAL>a ∈ u.toSet ↔ a ∈ u
<VAR>u : ZFSet<GOAL>u.Nonempty ↔ ∃ x, x ∈ u
<VAR>x u : ZFSet<VAR>h : x ∈ u<GOAL>u.Nonempty
<VAR>u : ZFSet<GOAL>u.toSet.Nonempty ↔ u.Nonempty
<VAR>x y : ZFSet<GOAL>x ⊆ y ↔ ∀ ⦃z : ZFSet⦄, z ∈ x → z ∈ y
<VAR>x y : PSet<GOAL>ZFSet.mk x ⊆ ZFSet.mk y ↔ x ⊆ y
<VAR>x y : ZFSet<GOAL>(∀ (z : ZFSet), z ∈ x ↔ z ∈ y) → x = y
<VAR>x y : ZFSet<GOAL>x = y ↔ ∀ (z : ZFSet), z ∈ x ↔ z ∈ y
<VAR>x y : ZFSet<GOAL>x.toSet = y.toSet ↔ x = y
<VAR>x : ZFSet<GOAL>x ∉ ∅
<VAR>x : ZFSet<GOAL>∅ ⊆ x
<VAR>x : PSet<GOAL>(ZFSet.mk x).Nonempty ↔ x.Nonempty
<VAR>x y z : ZFSet<GOAL>x ∈ insert y z ↔ x = y ∨ x ∈ z
<VAR>x y : ZFSet<GOAL>x ∈ insert x y
<VAR>y z : ZFSet<VAR>x : ZFSet<VAR>h : z ∈ y<GOAL>z ∈ insert x y
<VAR>x y : ZFSet<GOAL>(insert x y).toSet = insert x y.toSet
<VAR>x y : ZFSet<GOAL>x ∈ {y} ↔ x = y
<VAR>x : ZFSet<GOAL>{x}.toSet = {x}
<VAR>u v : ZFSet<GOAL>(insert u v).Nonempty
<VAR>x y z : ZFSet<GOAL>x ∈ {y, z} ↔ x = y ∨ x = z
<VAR>n : ZFSet<GOAL>n ∈ ZFSet.omega → insert n n ∈ ZFSet.omega
<VAR>p : ZFSet → Prop<VAR>x y : ZFSet<GOAL>y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y
<VAR>a : ZFSet<VAR>p : ZFSet → Prop<GOAL>(ZFSet.sep p a).toSet = {x | x ∈ a.toSet ∧ p x}
<VAR>x y : ZFSet<GOAL>y ∈ x.powerset ↔ y ⊆ x
<VAR>α β : Type u<VAR>A : α → PSet<VAR>B : β → PSet<VAR>αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)<VAR>a : (⋃₀ PSet.mk α A).Type<GOAL>∃ b, ((⋃₀ PSet.mk α A).Func a).Equiv ((⋃₀ PSet.mk β B).Func b)
<VAR>x y : ZFSet<GOAL>y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
<VAR>x y z : ZFSet<VAR>hy : y ∈ z<VAR>hz : z ∈ x<GOAL>y ∈ ⋃₀ x
<VAR>x y z : ZFSet<VAR>hy : y ∉ z<VAR>hz : z ∈ x<GOAL>y ∉ ⋂₀ x
<VAR>x : ZFSet<GOAL>⋃₀ {x} = x
<VAR>x : ZFSet<GOAL>⋂₀ {x} = x
<VAR>x : ZFSet<GOAL>(⋃₀ x).toSet = ⋃₀ (ZFSet.toSet '' x.toSet)
<VAR>x : ZFSet<VAR>h : x.Nonempty<GOAL>(⋂₀ x).toSet = ⋂₀ (ZFSet.toSet '' x.toSet)
<VAR>x y : ZFSet<GOAL>{x} = {y} ↔ x = y
<VAR>x y : ZFSet<GOAL>(x ∪ y).toSet = x.toSet ∪ y.toSet
<VAR>x y : ZFSet<GOAL>(x ∩ y).toSet = x.toSet ∩ y.toSet
<VAR>x y : ZFSet<GOAL>(x \ y).toSet = x.toSet \ y.toSet
<VAR>x y z : ZFSet<GOAL>z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y
<VAR>x y z : ZFSet<GOAL>z ∈ x \ y ↔ z ∈ x ∧ z ∉ y
<VAR>x y : ZFSet<GOAL>⋃₀ {x, y} = x ∪ y
<VAR>p : ZFSet → Prop<VAR>x : ZFSet<VAR>h : ∀ (x : ZFSet), (∀ y ∈ x, p y) → p x<GOAL>p x
<VAR>x y : ZFSet<GOAL>x ∈ y → y ∉ x
<VAR>x : ZFSet<VAR>h : x ≠ ∅<GOAL>∃ y ∈ x, x ∩ y = ∅
<VAR>f : ZFSet → ZFSet<VAR>H : PSet.Definable 1 f<VAR>x : ZFSet<VAR>y : ZFSet<GOAL>y ∈ x → f y ∈ ZFSet.image f x
<VAR>f : ZFSet → ZFSet<VAR>H : PSet.Definable 1 f<VAR>x y : ZFSet<GOAL>y ∈ ZFSet.image f x ↔ ∃ z ∈ x, f z = y
<VAR>f : ZFSet → ZFSet<VAR>H : PSet.Definable 1 f<VAR>x : ZFSet<GOAL>(ZFSet.image f x).toSet = f '' x.toSet
<VAR>α : Type u<VAR>f : α → ZFSet<VAR>x : ZFSet<GOAL>x ∈ ZFSet.range f ↔ x ∈ Set.range f
<VAR>α : Type u<VAR>f : α → ZFSet<GOAL>(ZFSet.range f).toSet = Set.range f
<VAR>x y : ZFSet<GOAL>(x.pair y).toSet = {{x}, {x, y}}
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y z : ZFSet<GOAL>z ∈ ZFSet.pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
<VAR>x y x' y' : ZFSet<GOAL>x.pair y = x'.pair y' ↔ x = x' ∧ y = y'
<VAR>x y z : ZFSet<GOAL>z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b
<VAR>x y a b : ZFSet<GOAL>a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y
<VAR>x y f : ZFSet<GOAL>f ∈ x.funs y ↔ x.IsFunc y f
<VAR>f : ZFSet → ZFSet<VAR>PSet.Definable 1 f<VAR>x y : ZFSet<GOAL>y ∈ ZFSet.map f x ↔ ∃ z ∈ x, z.pair (f z) = y
<VAR>f : ZFSet → ZFSet<VAR>H : PSet.Definable 1 f<VAR>x z : ZFSet<VAR>zx : z ∈ x<GOAL>∃! w, z.pair w ∈ ZFSet.map f x
<VAR>f : ZFSet → ZFSet<VAR>PSet.Definable 1 f<VAR>x y : ZFSet<GOAL>x.IsFunc y (ZFSet.map f x) ↔ ∀ z ∈ x, f z ∈ y
<VAR>p : ZFSet → Prop<VAR>x : ZFSet<GOAL>ZFSet.Hereditarily p x ↔ p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y
<VAR>p : ZFSet → Prop<VAR>x : ZFSet<VAR>h : ZFSet.Hereditarily p x<GOAL>p x
<VAR>p : ZFSet → Prop<VAR>x y : ZFSet<VAR>h : ZFSet.Hereditarily p x<VAR>hy : y ∈ x<GOAL>ZFSet.Hereditarily p y
<VAR>p : ZFSet → Prop<VAR>x : ZFSet<GOAL>ZFSet.Hereditarily p x → p ∅
<VAR>x y : Class<GOAL>(∀ (z : ZFSet), x z ↔ y z) → x = y
<VAR>x y : Class<GOAL>x = y ↔ ∀ (z : ZFSet), x z ↔ y z
<VAR>A B : Class<GOAL>A ∈ B ↔ ∃ x, ↑x = A ∧ B x
<VAR>A : Class<GOAL>A ∈ Class.univ ↔ ∃ x, ↑x = A
<VAR>A : Class<GOAL>A = Class.univ ↔ ∀ (x : ZFSet), A x
<VAR>A : Class<GOAL>(∀ (x : ZFSet), A x) → A = Class.univ
<VAR>x y : Class<GOAL>x ∈ y → y ∉ x
<VAR>x y : ZFSet<VAR>h : ↑x = ↑y<GOAL>x = y
<VAR>A : Class<VAR>x : ZFSet<GOAL>A.ToSet ↑x ↔ A x
<VAR>x : ZFSet<VAR>A : Class<GOAL>↑x ∈ A ↔ A x
<VAR>x y : ZFSet<GOAL>↑y x ↔ x ∈ y
<VAR>x y : ZFSet<GOAL>↑x ⊆ ↑y ↔ x ⊆ y
<VAR>p : Class<VAR>x : ZFSet<GOAL>↑(ZFSet.sep p x) = {y | y ∈ x ∧ p y}
<VAR>x y : ZFSet<GOAL>↑(insert x y) = insert x ↑y
<VAR>x y : ZFSet<GOAL>↑(x ∪ y) = ↑x ∪ ↑y
<VAR>x y : ZFSet<GOAL>↑(x ∩ y) = ↑x ∩ ↑y
<VAR>x y : ZFSet<GOAL>↑(x \ y) = ↑x \ ↑y
<VAR>x : ZFSet<GOAL>↑x.powerset = (↑x).powerset
<VAR>A : Class<VAR>x : ZFSet<GOAL>A.powerset x ↔ ↑x ⊆ A
<VAR>x : Class<VAR>y : ZFSet<GOAL>(⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z
<VAR>x : ZFSet<GOAL>↑(⋃₀ x) = ⋃₀ ↑x
<VAR>x y : Class<GOAL>y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
<VAR>x : Class<VAR>y : ZFSet<GOAL>(⋂₀ x) y ↔ ∀ (z : ZFSet), x z → y ∈ z
<VAR>x : ZFSet<VAR>h : x.Nonempty<GOAL>↑(⋂₀ x) = ⋂₀ ↑x
<VAR>x y z : Class<VAR>hy : y ∈ ⋂₀ x<VAR>hz : z ∈ x<GOAL>y ∈ z
<VAR>A : Class<VAR>hA : A.powerset ⊆ A<GOAL>A = Class.univ
<VAR>A : Class<VAR>x : ZFSet<VAR>H : ∀ (y : ZFSet), A y ↔ y = x<GOAL>A.iota = ↑x
<VAR>A : Class<GOAL>A.iota ∈ Class.univ
<VAR>F A : Class<GOAL>F ′ A ∈ Class.univ
<VAR>f : ZFSet → ZFSet<VAR>H : PSet.Definable 1 f<VAR>x y : ZFSet<VAR>h : y ∈ x<GOAL>↑(ZFSet.map f x) ′ ↑y = ↑(f y)
<VAR>x : ZFSet<VAR>h : ∅ ∉ x<GOAL>x.IsFunc (⋃₀ x) x.choice
<VAR>x : ZFSet<VAR>h : ∅ ∉ x<VAR>y : ZFSet<VAR>yx : y ∈ x<GOAL>↑x.choice ′ ↑y ∈ ↑y
<VAR>s : Set ZFSet<VAR>hs : Small.{u, u + 1} ↑s<GOAL>(ZFSet.mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x))).toSet = s
<VAR>x : ZFSet<GOAL>↑(ZFSet.toSet_equiv x) = x.toSet
<VAR>G : SetTheory.PGame<GOAL>G.ImpartialAux ↔ G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).ImpartialAux) ∧ ∀ (j : G.RightMoves), (G.moveRight j).ImpartialAux
<VAR>G : SetTheory.PGame<VAR>self : G.Impartial<GOAL>G.ImpartialAux
<VAR>G : SetTheory.PGame<GOAL>G.Impartial ↔ G.ImpartialAux
<VAR>G : SetTheory.PGame<GOAL>G.Impartial ↔ G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).Impartial) ∧ ∀ (j : G.RightMoves), (G.moveRight j).Impartial
<VAR>G : SetTheory.PGame<VAR>h : G.Impartial<GOAL>G ≈ -G
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>-⟦G⟧ = ⟦G⟧
<VAR>G H : SetTheory.PGame<GOAL>G.Relabelling H → ∀ [inst : G.Impartial], H.Impartial
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>¬0 < G
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>¬G < 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G ≈ 0 ∨ G.Fuzzy 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>¬G ≈ 0 ↔ G.Fuzzy 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>¬G.Fuzzy 0 ↔ G ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G + G ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>⟦G⟧ + ⟦G⟧ = 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<VAR>H : SetTheory.PGame<GOAL>H ≈ G ↔ H + G ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<VAR>H : SetTheory.PGame<GOAL>G ≈ H ↔ G + H ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G ≤ 0 ↔ 0 ≤ G
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G.LF 0 ↔ SetTheory.PGame.LF 0 G
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G ≈ 0 ↔ G ≤ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G.Fuzzy 0 ↔ G.LF 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G ≈ 0 ↔ 0 ≤ G
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G.Fuzzy 0 ↔ SetTheory.PGame.LF 0 G
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>(∀ (i : G.LeftMoves), (G.moveLeft i).Fuzzy 0) ↔ G ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>(∀ (j : G.RightMoves), (G.moveRight j).Fuzzy 0) ↔ G ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>(∃ i, G.moveLeft i ≈ 0) ↔ G.Fuzzy 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>(∃ j, G.moveRight j ≈ 0) ↔ G.Fuzzy 0
<VAR>x : SetTheory.PGame<GOAL>Subsingleton x.Short
<VAR>x : SetTheory.PGame<VAR>x.Short<GOAL>x.birthday < Ordinal.omega
<VAR>S : Type u<VAR>self : SetTheory.PGame.State S<VAR>s t : S<GOAL>t ∈ SetTheory.PGame.State.r s → SetTheory.PGame.State.turnBound t < SetTheory.PGame.State.turnBound s
<VAR>S : Type u<VAR>self : SetTheory.PGame.State S<VAR>s t : S<GOAL>t ∈ SetTheory.PGame.State.l s → SetTheory.PGame.State.turnBound t < SetTheory.PGame.State.turnBound s
<VAR>S : Type u<VAR>SetTheory.PGame.State S<VAR>s t : S<VAR>m : t ∈ SetTheory.PGame.State.l s<GOAL>SetTheory.PGame.State.turnBound s ≠ 0
<VAR>S : Type u<VAR>SetTheory.PGame.State S<VAR>s t : S<VAR>m : t ∈ SetTheory.PGame.State.r s<GOAL>SetTheory.PGame.State.turnBound s ≠ 0
<VAR>S : Type u<VAR>SetTheory.PGame.State S<VAR>s t : S<VAR>m : t ∈ SetTheory.PGame.State.l s<VAR>n : ℕ<VAR>h : SetTheory.PGame.State.turnBound s ≤ n + 1<GOAL>SetTheory.PGame.State.turnBound t ≤ n
<VAR>S : Type u<VAR>SetTheory.PGame.State S<VAR>s t : S<VAR>m : t ∈ SetTheory.PGame.State.r s<VAR>n : ℕ<VAR>h : SetTheory.PGame.State.turnBound s ≤ n + 1<GOAL>SetTheory.PGame.State.turnBound t ≤ n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))<VAR>hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))<GOAL>∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>hBf : ∃ c < a, ∃ B, f =O[Bornology.cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)<VAR>hBg : ∃ c < a, ∃ B, g =O[Bornology.cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)<GOAL>∃ c < a, ∃ B, (f - g) =O[Bornology.cobounded ℂ ⊓ l] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ 𝓟 (Complex.im ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.re|))<VAR>hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.im<VAR>hzb : z.im ≤ b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ 𝓟 (Complex.im ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.re|))<VAR>ha : ∀ (z : ℂ), z.im = a → f z = 0<VAR>hb : ∀ (z : ℂ), z.im = b → f z = 0<GOAL>Set.EqOn f 0 (Complex.im ⁻¹' Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f g : ℂ → E<VAR>hdf : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)<VAR>hBf : ∃ c < π / (b - a), ∃ B, f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ 𝓟 (Complex.im ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.re|))<VAR>hdg : DiffContOnCl ℂ g (Complex.im ⁻¹' Set.Ioo a b)<VAR>hBg : ∃ c < π / (b - a), ∃ B, g =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ 𝓟 (Complex.im ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.re|))<VAR>ha : ∀ (z : ℂ), z.im = a → f z = g z<VAR>hb : ∀ (z : ℂ), z.im = b → f z = g z<GOAL>Set.EqOn f g (Complex.im ⁻¹' Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ 𝓟 (Complex.re ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ 𝓟 (Complex.re ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>ha : ∀ (z : ℂ), z.re = a → f z = 0<VAR>hb : ∀ (z : ℂ), z.re = b → f z = 0<GOAL>Set.EqOn f 0 (Complex.re ⁻¹' Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f g : ℂ → E<VAR>hdf : DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b)<VAR>hBf : ∃ c < π / (b - a), ∃ B, f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ 𝓟 (Complex.re ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hdg : DiffContOnCl ℂ g (Complex.re ⁻¹' Set.Ioo a b)<VAR>hBg : ∃ c < π / (b - a), ∃ B, g =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ 𝓟 (Complex.re ⁻¹' Set.Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>ha : ∀ (z : ℂ), z.re = a → f z = g z<VAR>hb : ∀ (z : ℂ), z.re = b → f z = g z<GOAL>Set.EqOn f g (Complex.re ⁻¹' Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * Complex.I)‖ ≤ C<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → f ↑x = 0<VAR>him : ∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0<GOAL>Set.EqOn f 0 {z | 0 ≤ z.re ∧ 0 ≤ z.im}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>hdf : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0)<VAR>hBf : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hdg : DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Ioi 0)<VAR>hBg : ∃ c < 2, ∃ B, g =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x<VAR>him : ∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)<GOAL>Set.EqOn f g {z | 0 ≤ z.re ∧ 0 ≤ z.im}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * Complex.I)‖ ≤ C<VAR>hz_re : z.re ≤ 0<VAR>hz_im : 0 ≤ z.im<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, f ↑x = 0<VAR>him : ∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0<GOAL>Set.EqOn f 0 {z | z.re ≤ 0 ∧ 0 ≤ z.im}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>hdf : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0)<VAR>hBf : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hdg : DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Ioi 0)<VAR>hBg : ∃ c < 2, ∃ B, g =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, f ↑x = g ↑x<VAR>him : ∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)<GOAL>Set.EqOn f g {z | z.re ≤ 0 ∧ 0 ≤ z.im}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * Complex.I)‖ ≤ C<VAR>hz_re : z.re ≤ 0<VAR>hz_im : z.im ≤ 0<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, f ↑x = 0<VAR>him : ∀ x ≤ 0, f (↑x * Complex.I) = 0<GOAL>Set.EqOn f 0 {z | z.re ≤ 0 ∧ z.im ≤ 0}