ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>hf : BddAbove (Set.range f)<VAR>t : Cardinal.{max u w}<GOAL>Cardinal.lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t
<VAR>ι : Type v<VAR>ι' : Type v'<VAR>f : ι → Cardinal.{w}<VAR>f' : ι' → Cardinal.{w'}<VAR>hf : BddAbove (Set.range f)<VAR>hf' : BddAbove (Set.range f')<VAR>g : ι → ι'<VAR>h : ∀ (i : ι), Cardinal.lift.{w', w} (f i) ≤ Cardinal.lift.{w, w'} (f' (g i))<GOAL>Cardinal.lift.{w', w} (iSup f) ≤ Cardinal.lift.{w, w'} (iSup f')
<VAR>ι : Type v<VAR>ι' : Type v'<VAR>f : ι → Cardinal.{v}<VAR>f' : ι' → Cardinal.{v'}<VAR>hf : BddAbove (Set.range f)<VAR>hf' : BddAbove (Set.range f')<VAR>g : ι → ι'<VAR>h : ∀ (i : ι), Cardinal.lift.{v', v} (f i) ≤ Cardinal.lift.{v, v'} (f' (g i))<GOAL>Cardinal.lift.{v', v} (iSup f) ≤ Cardinal.lift.{v, v'} (iSup f')
<GOAL>Cardinal.lift.{u_1, u_2} Cardinal.aleph0 = Cardinal.aleph0
<VAR>c : Cardinal.{u}<GOAL>Cardinal.aleph0 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 ≤ c
<VAR>c : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} c ≤ Cardinal.aleph0 ↔ c ≤ Cardinal.aleph0
<VAR>c : Cardinal.{u}<GOAL>Cardinal.aleph0 < Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 < c
<VAR>c : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} c < Cardinal.aleph0 ↔ c < Cardinal.aleph0
<VAR>n : ℕ<GOAL>Cardinal.mk (Fin n) = ↑n
<VAR>n : ℕ<GOAL>Cardinal.lift.{u, v} ↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n
<VAR>a : Cardinal.{u}<VAR>n : ℕ<GOAL>Cardinal.lift.{v, u} a = ↑n ↔ a = ↑n
<VAR>a : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.lift.{v, u} a = OfNat.ofNat n ↔ a = OfNat.ofNat n
<VAR>n : ℕ<VAR>a : Cardinal.{u}<GOAL>↑n = Cardinal.lift.{v, u} a ↔ ↑n = a
<VAR>a : Cardinal.{u}<GOAL>0 = Cardinal.lift.{v, u} a ↔ 0 = a
<VAR>a : Cardinal.{u}<GOAL>1 = Cardinal.lift.{v, u} a ↔ 1 = a
<VAR>a : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n = Cardinal.lift.{v, u} a ↔ OfNat.ofNat n = a
<VAR>a : Cardinal.{u}<VAR>n : ℕ<GOAL>Cardinal.lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n
<VAR>a : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} a ≤ 1 ↔ a ≤ 1
<VAR>a : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.lift.{v, u} a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n
<VAR>n : ℕ<VAR>a : Cardinal.{u}<GOAL>↑n ≤ Cardinal.lift.{v, u} a ↔ ↑n ≤ a
<VAR>a : Cardinal.{u}<GOAL>1 ≤ Cardinal.lift.{v, u} a ↔ 1 ≤ a
<VAR>a : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≤ Cardinal.lift.{v, u} a ↔ OfNat.ofNat n ≤ a
<VAR>a : Cardinal.{u}<VAR>n : ℕ<GOAL>Cardinal.lift.{v, u} a < ↑n ↔ a < ↑n
<VAR>a : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.lift.{v, u} a < OfNat.ofNat n ↔ a < OfNat.ofNat n
<VAR>n : ℕ<VAR>a : Cardinal.{u}<GOAL>↑n < Cardinal.lift.{v, u} a ↔ ↑n < a
<VAR>a : Cardinal.{u}<GOAL>0 < Cardinal.lift.{v, u} a ↔ 0 < a
<VAR>a : Cardinal.{u}<GOAL>1 < Cardinal.lift.{v, u} a ↔ 1 < a
<VAR>a : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n < Cardinal.lift.{v, u} a ↔ OfNat.ofNat n < a
<VAR>n : ℕ<GOAL>Cardinal.lift.{u_1, 0} (Cardinal.mk (Fin n)) = ↑n
<VAR>α : Type u<VAR>s : Finset α<GOAL>Cardinal.mk { x // x ∈ s } = ↑s.card
<VAR>α : Type u<VAR>Fintype α<GOAL>Cardinal.mk (Finset α) = 2 ^ Fintype.card α
<VAR>α : Type u<VAR>β : Type v<VAR>Fintype α<VAR>Zero β<GOAL>Cardinal.mk (α →₀ β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Fintype.card α
<VAR>α β : Type u<VAR>Fintype α<VAR>Zero β<GOAL>Cardinal.mk (α →₀ β) = Cardinal.mk β ^ Fintype.card α
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>↑s.card ≤ Cardinal.mk α
<VAR>n : ℕ<GOAL>↑n.succ = Order.succ ↑n
<VAR>n : ℕ<GOAL>Order.succ ↑n = ↑n + 1
<VAR>n : ℕ<VAR>c : Cardinal.{u_1}<GOAL>↑n + 1 ≤ c ↔ ↑n < c
<VAR>c : Cardinal.{u_1}<GOAL>2 ≤ c ↔ 1 < c
<VAR>α : Type u_1<VAR>n : ℕ<VAR>h : ↑n ≤ Cardinal.mk α<GOAL>∃ s, n ≤ s.card
<VAR>α : Type u<VAR>n : ℕ<VAR>H : ∀ (s : Finset α), s.card ≤ n<GOAL>Cardinal.mk α ≤ ↑n
<VAR>a : Cardinal.{u_1}<VAR>b : Cardinal.{u_1}<VAR>hb : 1 < b<GOAL>a < b ^ a
<VAR>c : Cardinal.{u_1}<GOAL>1 ≤ c ↔ 0 < c
<VAR>c : Cardinal.{u_1}<GOAL>1 ≤ c ↔ c ≠ 0
<VAR>c : Cardinal.{u_1}<GOAL>c < 1 ↔ c = 0
<VAR>n : ℕ<GOAL>↑n < Cardinal.aleph0
<VAR>c : Cardinal.{u_1}<GOAL>c < Cardinal.aleph0 ↔ ∃ n, c = ↑n
<VAR>c : Cardinal.{u_1}<VAR>h : c < Cardinal.aleph0<GOAL>Order.succ c = c + 1
<VAR>c : Cardinal.{u_1}<GOAL>Cardinal.aleph0 ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c
<VAR>n : ℕ<GOAL>¬(↑n).IsLimit
<VAR>c : Cardinal.{u_1}<VAR>h : c.IsLimit<GOAL>Cardinal.aleph0 ≤ c
<VAR>ι : Type u<VAR>Nonempty ι<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (Set.range f)<VAR>n : ℕ<VAR>h : ⨆ i, f i = ↑n<GOAL>∃ i, f i = ↑n
<GOAL>Set.range Nat.cast = Set.Iio Cardinal.aleph0
<VAR>α : Type u<VAR>n : ℕ<GOAL>Cardinal.mk α = ↑n ↔ Nonempty (α ≃ Fin n)
<VAR>α : Type u<GOAL>Cardinal.mk α < Cardinal.aleph0 ↔ Finite α
<VAR>α : Type u<GOAL>Cardinal.mk α < Cardinal.aleph0 ↔ Nonempty (Fintype α)
<VAR>α : Type u<VAR>Finite α<GOAL>Cardinal.mk α < Cardinal.aleph0
<VAR>α : Type u<VAR>S : Set α<GOAL>Cardinal.mk ↑S < Cardinal.aleph0 ↔ S.Finite
<VAR>α : Type u<VAR>p : α → Prop<GOAL>Cardinal.mk { x // p x } < Cardinal.aleph0 ↔ {x | p x}.Finite
<VAR>α : Type u<GOAL>Cardinal.mk α ≤ Cardinal.aleph0 ↔ Countable α
<VAR>α : Type u<VAR>Countable α<GOAL>Cardinal.mk α ≤ Cardinal.aleph0
<VAR>α : Type u<VAR>s : Set α<GOAL>Cardinal.mk ↑s ≤ Cardinal.aleph0 ↔ s.Countable
<VAR>α : Type u<VAR>p : α → Prop<GOAL>Cardinal.mk { x // p x } ≤ Cardinal.aleph0 ↔ {x | p x}.Countable
<VAR>a b : Cardinal.{u_1}<VAR>ha : a < Cardinal.aleph0<VAR>hb : b < Cardinal.aleph0<GOAL>a + b < Cardinal.aleph0
<VAR>a b : Cardinal.{u_1}<GOAL>a + b < Cardinal.aleph0 ↔ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0
<VAR>a b : Cardinal.{u_1}<GOAL>Cardinal.aleph0 ≤ a + b ↔ Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b
<VAR>n : ℕ<VAR>a : Cardinal.{u_1}<GOAL>n • a < Cardinal.aleph0 ↔ n = 0 ∨ a < Cardinal.aleph0
<VAR>n : ℕ<VAR>a : Cardinal.{u_1}<VAR>h : n ≠ 0<GOAL>n • a < Cardinal.aleph0 ↔ a < Cardinal.aleph0
<VAR>a b : Cardinal.{u_1}<VAR>ha : a < Cardinal.aleph0<VAR>hb : b < Cardinal.aleph0<GOAL>a * b < Cardinal.aleph0
<VAR>a b : Cardinal.{u_1}<GOAL>a * b < Cardinal.aleph0 ↔ a = 0 ∨ b = 0 ∨ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0
<VAR>a b : Cardinal.{u_1}<GOAL>Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b)
<VAR>a b : Cardinal.{u}<GOAL>Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ Cardinal.aleph0 ≤ b ∨ Cardinal.aleph0 ≤ a ∧ b ≠ 0
<VAR>a b : Cardinal.{u_1}<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a * b < Cardinal.aleph0 ↔ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0
<VAR>a b : Cardinal.{u_1}<VAR>ha : a < Cardinal.aleph0<VAR>hb : b < Cardinal.aleph0<GOAL>a ^ b < Cardinal.aleph0
<VAR>α : Type u_1<GOAL>Cardinal.mk α = 1 ↔ Subsingleton α ∧ Nonempty α
<VAR>α : Type u<GOAL>Infinite α ↔ Cardinal.aleph0 ≤ Cardinal.mk α
<VAR>α : Type u<GOAL>Cardinal.aleph0 ≤ Cardinal.mk α ↔ Infinite α
<VAR>α : Type u<VAR>Infinite α<GOAL>Cardinal.aleph0 ≤ Cardinal.mk α
<VAR>α : Type u_1<VAR>Countable α<VAR>Infinite α<GOAL>Cardinal.mk α = Cardinal.aleph0
<VAR>α : Type u<GOAL>Nonempty (Denumerable α) ↔ Cardinal.mk α = Cardinal.aleph0
<VAR>α : Type u<VAR>Denumerable α<GOAL>Cardinal.mk α = Cardinal.aleph0
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable ↑s)
<GOAL>Cardinal.aleph0 + Cardinal.aleph0 = Cardinal.aleph0
<GOAL>Cardinal.aleph0 * Cardinal.aleph0 = Cardinal.aleph0
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑n * Cardinal.aleph0 = Cardinal.aleph0
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Cardinal.aleph0 * ↑n = Cardinal.aleph0
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n * Cardinal.aleph0 = Cardinal.aleph0
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.aleph0 * OfNat.ofNat n = Cardinal.aleph0
<VAR>c₁ c₂ : Cardinal.{u_1}<GOAL>c₁ + c₂ ≤ Cardinal.aleph0 ↔ c₁ ≤ Cardinal.aleph0 ∧ c₂ ≤ Cardinal.aleph0
<VAR>n : ℕ<GOAL>Cardinal.aleph0 + ↑n = Cardinal.aleph0
<VAR>n : ℕ<GOAL>↑n + Cardinal.aleph0 = Cardinal.aleph0
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n + Cardinal.aleph0 = Cardinal.aleph0
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.aleph0 + OfNat.ofNat n = Cardinal.aleph0
<VAR>c : Cardinal.{u_1}<VAR>n : ℕ<VAR>h : c ≤ ↑n<GOAL>∃ m ≤ n, c = ↑m
<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i < g i<GOAL>Cardinal.sum f < Cardinal.prod g
<GOAL>Cardinal.mk PEmpty.{u_1 + 1} = 0
<GOAL>Cardinal.mk PUnit.{u_1 + 1} = 1
<VAR>α : Type u<VAR>x : α<GOAL>Cardinal.mk ↑{x} = 1
<VAR>α : Type u<VAR>n : ℕ<GOAL>Cardinal.mk (Mathlib.Vector α n) = Cardinal.mk α ^ n
<VAR>α : Type u<GOAL>Cardinal.mk (List α) = Cardinal.sum fun n => Cardinal.mk α ^ n
<VAR>α : Type u<VAR>r : α → α → Prop<GOAL>Cardinal.mk (Quot r) ≤ Cardinal.mk α
<VAR>α : Type u<VAR>s : Setoid α<GOAL>Cardinal.mk (Quotient s) ≤ Cardinal.mk α
<VAR>α : Type u<VAR>p q : α → Prop<VAR>h : ∀ ⦃x : α⦄, p x → q x<GOAL>Cardinal.mk (Subtype p) ≤ Cardinal.mk (Subtype q)
<VAR>α : Type u<GOAL>Cardinal.mk ↑∅ = 0
<VAR>α : Type u<VAR>s : Set α<GOAL>Cardinal.mk ↑s = 0 ↔ s = ∅
<VAR>α : Type u<GOAL>Cardinal.mk ↑Set.univ = Cardinal.mk α
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set α<GOAL>Cardinal.mk ↑(f '' s) ≤ Cardinal.mk ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)
<VAR>α β : Type u<VAR>f : α → β<GOAL>Cardinal.mk ↑(Set.range f) ≤ Cardinal.mk α
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) ≤ Cardinal.lift.{v, u} (Cardinal.mk α)
<VAR>α β : Type u<VAR>f : α → β<VAR>h : Function.Injective f<GOAL>Cardinal.mk ↑(Set.range f) = Cardinal.mk α
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Cardinal.lift.{max u w, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Cardinal.lift.{u, v} (Cardinal.mk β) ≤ Cardinal.lift.{v, u} (Cardinal.mk α)
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set α<VAR>h : Set.InjOn f s<GOAL>Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>h : Set.InjOn f s<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set α<VAR>hf : Function.Injective f<GOAL>Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>h : Function.Injective f<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
<VAR>α ι : Type u<VAR>f : ι → Set α<GOAL>Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.sum fun i => Cardinal.mk ↑(f i)
<VAR>α : Type u<VAR>ι : Type v<VAR>f : ι → Set α<GOAL>Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) ≤ Cardinal.sum fun i => Cardinal.mk ↑(f i)
<VAR>α ι : Type u<VAR>f : ι → Set α<VAR>h : Pairwise fun i j => Disjoint (f i) (f j)<GOAL>Cardinal.mk ↑(⋃ i, f i) = Cardinal.sum fun i => Cardinal.mk ↑(f i)
<VAR>α : Type u<VAR>ι : Type v<VAR>f : ι → Set α<VAR>h : Pairwise fun i j => Disjoint (f i) (f j)<GOAL>Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) = Cardinal.sum fun i => Cardinal.mk ↑(f i)
<VAR>α ι : Type u<VAR>f : ι → Set α<GOAL>Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.mk ι * ⨆ i, Cardinal.mk ↑(f i)
<VAR>α : Type u<VAR>ι : Type v<VAR>f : ι → Set α<GOAL>Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ι) * ⨆ i, Cardinal.lift.{v, u} (Cardinal.mk ↑(f i))
<VAR>α : Type u<VAR>A : Set (Set α)<GOAL>Cardinal.mk ↑(⋃₀ A) ≤ Cardinal.mk ↑A * ⨆ s, Cardinal.mk ↑↑s
<VAR>ι α : Type u<VAR>A : ι → Set α<VAR>s : Set ι<GOAL>Cardinal.mk ↑(⋃ x ∈ s, A x) ≤ Cardinal.mk ↑s * ⨆ x, Cardinal.mk ↑(A ↑x)
<VAR>α : Type u<VAR>ι : Type v<VAR>A : ι → Set α<VAR>s : Set ι<GOAL>Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ x ∈ s, A x)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ↑s) * ⨆ x, Cardinal.lift.{v, u} (Cardinal.mk ↑(A ↑x))
<VAR>α : Type u<VAR>s : Finset α<GOAL>Cardinal.mk ↑↑s < Cardinal.aleph0
<VAR>α : Type u_1<VAR>s : Set α<VAR>n : ℕ<GOAL>Cardinal.mk ↑s = ↑n ↔ ∃ t, ↑t = s ∧ t.card = n
<VAR>α : Type u<VAR>n : ℕ<GOAL>Cardinal.mk α = ↑n ↔ ∃ t, ↑t = Set.univ ∧ t.card = n
<VAR>α : Type u<VAR>n : ℕ<GOAL>Cardinal.mk α = ↑n ↔ ∃ h, Fintype.card α = n
<VAR>α : Type u<VAR>S T : Set α<GOAL>Cardinal.mk ↑(S ∪ T) + Cardinal.mk ↑(S ∩ T) = Cardinal.mk ↑S + Cardinal.mk ↑T
<VAR>α : Type u<VAR>S T : Set α<GOAL>Cardinal.mk ↑(S ∪ T) ≤ Cardinal.mk ↑S + Cardinal.mk ↑T
<VAR>α : Type u<VAR>S T : Set α<VAR>H : Disjoint S T<GOAL>Cardinal.mk ↑(S ∪ T) = Cardinal.mk ↑S + Cardinal.mk ↑T
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<GOAL>Cardinal.mk ↑(insert a s) = Cardinal.mk ↑s + 1
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<GOAL>Cardinal.mk ↑(insert a s) ≤ Cardinal.mk ↑s + 1
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Cardinal.mk ↑s + Cardinal.mk ↑sᶜ = Cardinal.mk α
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>Cardinal.mk ↑s ≤ Cardinal.mk ↑t
<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<GOAL>Cardinal.mk ↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
<VAR>α : Type u<VAR>p q : α → Prop<VAR>h : ∀ (x : α), p x → q x<GOAL>Cardinal.mk { x // p x } ≤ Cardinal.mk { x // q x }
<VAR>α : Type u<VAR>S T : Set α<GOAL>Cardinal.mk ↑S ≤ Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T
<VAR>α : Type u<VAR>S T : Set α<VAR>h : T ⊆ S<GOAL>Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T = Cardinal.mk ↑S
<VAR>α : Type u_1<VAR>P Q : Set α<GOAL>Cardinal.mk ↑(P ∪ Q) ≤ Cardinal.aleph0 ↔ Cardinal.mk ↑P ≤ Cardinal.aleph0 ∧ Cardinal.mk ↑Q ≤ Cardinal.aleph0
<VAR>α β : Type u<VAR>p : β → Prop<VAR>e : α ≃ β<GOAL>Cardinal.mk { a // p (e a) } = Cardinal.mk { b // p b }
<VAR>α : Type u<VAR>s : Set α<VAR>t : α → Prop<GOAL>Cardinal.mk ↑{x | x ∈ s ∧ t x} = Cardinal.mk ↑{x | t ↑x}
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : Function.Injective f<GOAL>Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ↑s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : s ⊆ Set.range f<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s))
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : Function.Injective f<VAR>h2 : s ⊆ Set.range f<GOAL>Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) = Cardinal.lift.{u, v} (Cardinal.mk ↑s)
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set β<VAR>h : Function.Injective f<VAR>h2 : s ⊆ Set.range f<GOAL>Cardinal.mk ↑(f ⁻¹' s) = Cardinal.mk ↑s
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set β<VAR>h : Function.Injective f<GOAL>Cardinal.mk ↑(f ⁻¹' s) ≤ Cardinal.mk ↑s
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set β<VAR>h : s ⊆ Set.range f<GOAL>Cardinal.mk ↑s ≤ Cardinal.mk ↑(f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ f '' s<GOAL>Cardinal.lift.{u, v} (Cardinal.mk ↑t) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑{x | x ∈ s ∧ f x ∈ t})
<VAR>α β : Type u<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ f '' s<GOAL>Cardinal.mk ↑t ≤ Cardinal.mk ↑{x | x ∈ s ∧ f x ∈ t}
<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>s : Set α<GOAL>c ≤ Cardinal.mk ↑s ↔ ∃ p ⊆ s, Cardinal.mk ↑p = c
<VAR>α : Type u<GOAL>2 ≤ Cardinal.mk α ↔ ∃ x y, x ≠ y
<VAR>α : Type u<VAR>x : α<GOAL>2 ≤ Cardinal.mk α ↔ ∃ y, y ≠ x
<VAR>α : Type u<GOAL>Cardinal.mk α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = Set.univ
<VAR>α : Type u<VAR>x : α<GOAL>Cardinal.mk α = 2 ↔ ∃! y, y ≠ x
<VAR>α : Type u_1<VAR>l : List α<VAR>h : ↑l.length < Cardinal.mk α<GOAL>∃ z, z ∉ l
<VAR>α : Type u_1<VAR>h : 3 ≤ Cardinal.mk α<VAR>x y : α<GOAL>∃ z, z ≠ x ∧ z ≠ y
<VAR>b c : Cardinal.{u}<VAR>a : Cardinal.{u}<VAR>h : c < b<GOAL>a ^ c ≤ a ^< b
<VAR>a b c : Cardinal.{u}<GOAL>a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c
<VAR>a b c : Cardinal.{u_1}<VAR>h : b ≤ c<GOAL>a ^< b ≤ a ^< c
<VAR>a : Cardinal.{u_1}<GOAL>Monotone fun c => a ^< c
<VAR>a b : Cardinal.{u_1}<VAR>h : a ≠ 0<GOAL>a ^< Order.succ b = a ^ b
<VAR>a b c : Cardinal.{u_1}<GOAL>a ^< min b c = min (a ^< b) (a ^< c)
<VAR>a b c : Cardinal.{u_1}<GOAL>a ^< max b c = max (a ^< b) (a ^< c)
<VAR>a : Cardinal.{u_1}<VAR>h : a ≠ 0<GOAL>0 ^< a = 1
<VAR>a : Cardinal.{u_1}<GOAL>a ^< 0 = 0
<VAR>V : Type u_1<VAR>Quiver V<VAR>a b : V<GOAL>Quiver.WeaklyConnectedComponent.mk a = Quiver.WeaklyConnectedComponent.mk b ↔ Nonempty (Quiver.Path a b)
<VAR>x : SetTheory.PGame<GOAL>x.Numeric ↔ (∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) ∧ (∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) ∧ ∀ (j : x.RightMoves), (x.moveRight j).Numeric
<VAR>x : SetTheory.PGame<VAR>h₁ : ∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j<VAR>h₂ : ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric<VAR>h₃ : ∀ (j : x.RightMoves), (x.moveRight j).Numeric<GOAL>x.Numeric
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>i : x.LeftMoves<VAR>j : x.RightMoves<GOAL>x.moveLeft i < x.moveRight j
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>i : x.LeftMoves<GOAL>(x.moveLeft i).Numeric
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>j : x.RightMoves<GOAL>(x.moveRight j).Numeric
<VAR>x' x : SetTheory.PGame<VAR>h : x'.IsOption x<VAR>hx : x.Numeric<GOAL>x'.Numeric
<VAR>C : SetTheory.PGame → Prop<VAR>H : ∀ (l r : Type u_1) (L : l → SetTheory.PGame) (R : r → SetTheory.PGame), (∀ (i : l) (j : r), L i < R j) → (∀ (i : l), (L i).Numeric) → (∀ (i : r), (R i).Numeric) → (∀ (i : l), C (L i)) → (∀ (i : r), C (R i)) → C (SetTheory.PGame.mk l r L R)<VAR>x : SetTheory.PGame<GOAL>x.Numeric → C x
<VAR>x y : SetTheory.PGame<VAR>r : x ≡r y<VAR>ox : x.Numeric<GOAL>y.Numeric
<VAR>x y : SetTheory.PGame<VAR>r : x ≡r y<GOAL>x.Numeric ↔ y.Numeric
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x ⧏ y → ¬y ⧏ x
<VAR>x y : SetTheory.PGame<VAR>h : x ⧏ y<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x ≤ y
<VAR>x y : SetTheory.PGame<VAR>h : x ⧏ y<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x < y
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x ⧏ y ↔ x < y
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x ≤ y ↔ (∀ (i : x.LeftMoves), x.moveLeft i < y) ∧ ∀ (j : y.RightMoves), x < y.moveRight j
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x < y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>((∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y) → x < y
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x < y ↔ (∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧ ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>¬x ‖ y
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x < y ∨ x ≈ y ∨ y < x
<VAR>x : SetTheory.PGame<VAR>IsEmpty x.LeftMoves<VAR>IsEmpty x.RightMoves<GOAL>x.Numeric
<VAR>x : SetTheory.PGame<VAR>IsEmpty x.LeftMoves<GOAL>(∀ (j : x.RightMoves), (x.moveRight j).Numeric) → x.Numeric
<VAR>x : SetTheory.PGame<VAR>IsEmpty x.RightMoves<VAR>H : ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric<GOAL>x.Numeric
<VAR>x : SetTheory.PGame<GOAL>x.Numeric → (-x).Numeric
<VAR>x x' : SetTheory.PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : x' ≤ x<GOAL>(x.insertLeft x').Numeric
<VAR>x x' : SetTheory.PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : x ≤ x'<GOAL>(x.insertRight x').Numeric
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>i : x.LeftMoves<GOAL>x.moveLeft i < x
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>i : x.LeftMoves<GOAL>x.moveLeft i ≤ x
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>j : x.RightMoves<GOAL>x < x.moveRight j
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>j : x.RightMoves<GOAL>x ≤ x.moveRight j
<VAR>x y : SetTheory.PGame<GOAL>x.Numeric → y.Numeric → (x + y).Numeric
<VAR>x y : SetTheory.PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>(x - y).Numeric
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>Surreal.mk x hx = Surreal.mk y hy ↔ x ≈ y
<VAR>x : SetTheory.PGame<VAR>hx : x.Numeric<GOAL>Surreal.mk x hx = 0 ↔ x ≈ 0
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>Surreal.mk x hx ≤ Surreal.mk y hy ↔ x ≤ y
<VAR>x : SetTheory.PGame<VAR>hx : x.Numeric<GOAL>0 ≤ Surreal.mk x hx ↔ 0 ≤ x
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>Surreal.mk x hx < Surreal.mk y hy ↔ x < y
<VAR>x : SetTheory.PGame<VAR>hx : x.Numeric<GOAL>0 < Surreal.mk x hx ↔ 0 < x
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>i : x.LeftMoves<GOAL>Surreal.mk (x.moveLeft i) ⋯ < Surreal.mk x o
<VAR>x : SetTheory.PGame<VAR>o : x.Numeric<VAR>j : x.RightMoves<GOAL>Surreal.mk x o < Surreal.mk (x.moveRight j) ⋯
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>Surreal.mk (x + y) ⋯ = Surreal.mk x hx + Surreal.mk y hy
<VAR>x y : SetTheory.PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<GOAL>Surreal.mk (x - y) ⋯ = Surreal.mk x hx - Surreal.mk y hy
<GOAL>0 = Surreal.mk 0 SetTheory.PGame.numeric_zero
<VAR>n : ℕ<GOAL>Surreal.toGame ↑n = ↑n
<VAR>ι : Type u_1<VAR>Small.{u, u_1} ι<VAR>f : ι → Surreal<GOAL>BddAbove (Set.range f)
<VAR>s : Set Surreal<VAR>Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>ι : Type u_1<VAR>Small.{u, u_1} ι<VAR>f : ι → Surreal<GOAL>BddBelow (Set.range f)
<VAR>s : Set Surreal<VAR>Small.{u, u + 1} ↑s<GOAL>BddBelow s
<VAR>V : Type u<VAR>Quiver V<VAR>r : V<VAR>self : Quiver.RootedConnected r<VAR>b : V<GOAL>Nonempty (Quiver.Path r b)
<VAR>V : Type u<VAR>Quiver V<VAR>r : V<VAR>Quiver.RootedConnected r<VAR>a : V<VAR>p : Quiver.Path r a<GOAL>(Quiver.shortestPath r a).length ≤ p.length
<VAR>V : Type u_1<VAR>Quiver V<VAR>W : Type u_2<VAR>σ : V → W<GOAL>(Quiver.Push.of σ).obj = σ
<VAR>V : Type u_1<VAR>Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<GOAL>(Quiver.Push.lift σ φ τ h).obj = τ
<VAR>V : Type u_1<VAR>Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<GOAL>Quiver.Push.of σ ⋙q Quiver.Push.lift σ φ τ h = φ
<VAR>V : Type u_1<VAR>Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<VAR>Φ : Quiver.Push σ ⥤q W'<VAR>Φ₀ : Φ.obj = τ<VAR>Φcomp : Quiver.Push.of σ ⋙q Φ = φ<GOAL>Φ = Quiver.Push.lift σ φ τ h
<VAR>α : Type u_1<VAR>x y : Quiver.SingleObj α<GOAL>x = y
<VAR>α : Type u_1<VAR>a : α<GOAL>Quiver.SingleObj.toHom.symm a = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Quiver.SingleObj.toHom a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : Quiver.SingleObj α<GOAL>(Quiver.SingleObj.toPrefunctor f).obj a = id a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Quiver.SingleObj α ⥤q Quiver.SingleObj β<VAR>a : α<GOAL>Quiver.SingleObj.toPrefunctor.symm f a = f.map (Quiver.SingleObj.toHom a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>∀ {X Y : Quiver.SingleObj α} (a : α), (Quiver.SingleObj.toPrefunctor f).map a = f a
<VAR>α : Type u_1<GOAL>Quiver.SingleObj.toPrefunctor id = 𝟭q (Quiver.SingleObj α)
<VAR>α : Type u_1<GOAL>Quiver.SingleObj.toPrefunctor.symm (𝟭q (Quiver.SingleObj α)) = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<GOAL>Quiver.SingleObj.toPrefunctor (g ∘ f) = Quiver.SingleObj.toPrefunctor f ⋙q Quiver.SingleObj.toPrefunctor g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : Quiver.SingleObj α ⥤q Quiver.SingleObj β<VAR>g : Quiver.SingleObj β ⥤q Quiver.SingleObj γ<GOAL>Quiver.SingleObj.toPrefunctor.symm (f ⋙q g) = Quiver.SingleObj.toPrefunctor.symm g ∘ Quiver.SingleObj.toPrefunctor.symm f
<VAR>α : Type u_1<VAR>x : Quiver.SingleObj α<VAR>p : Quiver.Path (Quiver.SingleObj.star α) x<GOAL>Quiver.SingleObj.listToPath (Quiver.SingleObj.pathToList p) = Quiver.Path.cast ⋯ ⋯ p
<VAR>α : Type u_1<VAR>l : List α<GOAL>Quiver.SingleObj.pathToList (Quiver.SingleObj.listToPath l) = l
<VAR>α : Type u_1<GOAL>Quiver.SingleObj.pathEquivList Quiver.Path.nil = []
<VAR>α : Type u_1<VAR>p : Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α)<VAR>a : Quiver.SingleObj.star α ⟶ Quiver.SingleObj.star α<GOAL>Quiver.SingleObj.pathEquivList (p.cons a) = a :: Quiver.SingleObj.pathToList p
<VAR>α : Type u_1<GOAL>Quiver.SingleObj.pathEquivList.symm [] = Quiver.Path.nil