ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>hdf : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0)<VAR>hBf : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hdg : DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Iio 0)<VAR>hBg : ∃ c < 2, ∃ B, g =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, f ↑x = g ↑x<VAR>him : ∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)<GOAL>Set.EqOn f g {z | z.re ≤ 0 ∧ z.im ≤ 0}
<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.Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * Complex.I)‖ ≤ C<VAR>hz_re : 0 ≤ z.re<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.Ioi 0 ×ℂ Set.Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → f ↑x = 0<VAR>him : ∀ x ≤ 0, f (↑x * Complex.I) = 0<GOAL>Set.EqOn f 0 {z | 0 ≤ z.re ∧ z.im ≤ 0}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>hdf : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0)<VAR>hBf : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hdg : DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Iio 0)<VAR>hBg : ∃ c < 2, ∃ B, g =O[Bornology.cobounded ℂ ⊓ 𝓟 (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x<VAR>him : ∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)<GOAL>Set.EqOn f g {z | 0 ≤ z.re ∧ z.im ≤ 0}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Filter.Tendsto (fun x => f ↑x) Filter.atTop (𝓝 0)<VAR>him : ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C<VAR>hz : 0 ≤ z.re<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>C : ℝ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C<VAR>hz : 0 ≤ z.re<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℂ → E<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Asymptotics.SuperpolynomialDecay Filter.atTop expR fun x => ‖f ↑x‖<VAR>him : ∃ C, ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C<GOAL>Set.EqOn f 0 {z | 0 ≤ z.re}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : ℂ → E<VAR>hfd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hgd : DiffContOnCl ℂ g {z | 0 < z.re}<VAR>hfexp : ∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hgexp : ∃ c < 2, ∃ B, g =O[Bornology.cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Asymptotics.SuperpolynomialDecay Filter.atTop expR fun x => ‖f ↑x - g ↑x‖<VAR>hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C<VAR>hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * Complex.I)‖ ≤ C<GOAL>Set.EqOn f g {z | 0 ≤ z.re}
<VAR>C : Ordinal.{u_2} → Sort u_1<VAR>b : Ordinal.{u_2}<VAR>H0 : C 0<VAR>H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o<GOAL>b.CNFRec H0 H 0 = H0
<VAR>b : Ordinal.{u_2}<VAR>o : Ordinal.{u_2}<VAR>C : Ordinal.{u_2} → Sort u_1<VAR>ho : o ≠ 0<VAR>H0 : C 0<VAR>H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o<GOAL>b.CNFRec H0 H o = H o ho (b.CNFRec H0 H (o % b ^ Ordinal.log b o))
<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.CNF b 0 = []
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>Ordinal.CNF b o = (Ordinal.log b o, o / b ^ Ordinal.log b o) :: Ordinal.CNF b (o % b ^ Ordinal.log b o)
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>Ordinal.CNF 0 o = [(0, o)]
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>Ordinal.CNF 1 o = [(0, o)]
<VAR>b o : Ordinal.{u_1}<VAR>hb : b ≤ 1<VAR>ho : o ≠ 0<GOAL>Ordinal.CNF b o = [(0, o)]
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>hb : o < b<GOAL>Ordinal.CNF b o = [(0, o)]
<VAR>b o : Ordinal.{u_1}<GOAL>List.foldr (fun p r => b ^ p.1 * p.2 + r) 0 (Ordinal.CNF b o) = o
<VAR>b o : Ordinal.{u}<VAR>x : Ordinal.{u} × Ordinal.{u}<GOAL>x ∈ Ordinal.CNF b o → x.1 ≤ Ordinal.log b o
<VAR>b o : Ordinal.{u}<VAR>x : Ordinal.{u} × Ordinal.{u}<VAR>h : x ∈ Ordinal.CNF b o<GOAL>x.1 ≤ o
<VAR>b o : Ordinal.{u}<VAR>x : Ordinal.{u} × Ordinal.{u}<GOAL>x ∈ Ordinal.CNF b o → 0 < x.2
<VAR>b o : Ordinal.{u}<VAR>hb : 1 < b<VAR>x : Ordinal.{u} × Ordinal.{u}<GOAL>x ∈ Ordinal.CNF b o → x.2 < b
<VAR>b o : Ordinal.{u_1}<GOAL>List.Sorted (fun x x_1 => x > x_1) (List.map Prod.fst (Ordinal.CNF b o))
<VAR>o : Ordinal.{u_1}<GOAL>let_fun this := ⋯;
o.toPGame = SetTheory.PGame.mk (Quotient.out o).α PEmpty.{u_1 + 1} (fun x => (Ordinal.typein (fun x x_1 => x < x_1) x).toPGame) PEmpty.elim
<VAR>o : Ordinal.{u_1}<GOAL>o.toPGame.LeftMoves = (Quotient.out o).α
<VAR>o : Ordinal.{u_1}<GOAL>o.toPGame.RightMoves = PEmpty.{u_1 + 1}
<VAR>o : Ordinal.{u_1}<VAR>i : o.toPGame.LeftMoves<GOAL>↑(Ordinal.toLeftMovesToPGame.symm i) < o
HEq o.toPGame.moveLeft fun x => (Ordinal.typein (fun x x_1 => x < x_1) x).toPGame
<VAR>o : Ordinal.{u_1}<VAR>i : o.toPGame.LeftMoves<GOAL>o.toPGame.moveLeft i = (↑(Ordinal.toLeftMovesToPGame.symm i)).toPGame
<VAR>o : Ordinal.{u_1}<VAR>i : ↑(Set.Iio o)<GOAL>o.toPGame.moveLeft (Ordinal.toLeftMovesToPGame i) = (↑i).toPGame
<GOAL>default = Ordinal.toLeftMovesToPGame ⟨0, ⋯⟩
<VAR>i : (Ordinal.toPGame 1).LeftMoves<GOAL>Ordinal.toLeftMovesToPGame.symm i = ⟨0, ⋯⟩
<VAR>x : (Ordinal.toPGame 1).LeftMoves<GOAL>(Ordinal.toPGame 1).moveLeft x = Ordinal.toPGame 0
<VAR>a b : Ordinal.{u_1}<VAR>h : a < b<GOAL>a.toPGame < b.toPGame
<VAR>a : Ordinal.{u_1}<GOAL>0 ≤ a.toPGame
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame ⧏ b.toPGame ↔ a < b
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame ≤ b.toPGame ↔ a ≤ b
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame < b.toPGame ↔ a < b
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame ≈ b.toPGame ↔ a = b
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame = b.toPGame ↔ a = b
<GOAL>∀ (a : Ordinal.{u}), Ordinal.toPGameEmbedding a = a.toPGame
<VAR>a b : Ordinal.{u_1}<GOAL>⟦a.toPGame⟧ + ⟦b.toPGame⟧ = ⟦(a ♯ b).toPGame⟧
<VAR>n : ℕ<GOAL>(SetTheory.PGame.powHalf n).LeftMoves = PUnit.{u_1 + 1}
<GOAL>(SetTheory.PGame.powHalf 0).RightMoves = PEmpty.{u_1 + 1}
<VAR>n : ℕ<GOAL>(SetTheory.PGame.powHalf (n + 1)).RightMoves = PUnit.{u_1 + 1}
<VAR>n : ℕ<VAR>i : (SetTheory.PGame.powHalf n).LeftMoves<GOAL>(SetTheory.PGame.powHalf n).moveLeft i = 0
<VAR>n : ℕ<VAR>i : (SetTheory.PGame.powHalf (n + 1)).RightMoves<GOAL>(SetTheory.PGame.powHalf (n + 1)).moveRight i = SetTheory.PGame.powHalf n
<GOAL>(SetTheory.PGame.powHalf 1).birthday = 2
<VAR>n : ℕ<GOAL>(SetTheory.PGame.powHalf n).Numeric
<VAR>n : ℕ<GOAL>SetTheory.PGame.powHalf (n + 1) < SetTheory.PGame.powHalf n
<VAR>n : ℕ<GOAL>SetTheory.PGame.powHalf (n + 1) ≤ SetTheory.PGame.powHalf n
<VAR>n : ℕ<GOAL>SetTheory.PGame.powHalf n ≤ 1
<VAR>n : ℕ<GOAL>SetTheory.PGame.powHalf (n + 1) < 1
<VAR>n : ℕ<GOAL>0 < SetTheory.PGame.powHalf n
<VAR>n : ℕ<GOAL>0 ≤ SetTheory.PGame.powHalf n
<VAR>n : ℕ<GOAL>SetTheory.PGame.powHalf (n + 1) + SetTheory.PGame.powHalf (n + 1) ≈ SetTheory.PGame.powHalf n
<GOAL>SetTheory.PGame.powHalf 1 + SetTheory.PGame.powHalf 1 ≈ 1
<VAR>n : ℕ<GOAL>2 * Surreal.powHalf (n + 1) = Surreal.powHalf n
<VAR>n : ℕ<GOAL>2 ^ n * Surreal.powHalf n = 1
<VAR>n k : ℕ<GOAL>2 ^ n * Surreal.powHalf (n + k) = Surreal.powHalf k
<VAR>m : ℤ<VAR>n k : ℕ<GOAL>↑m * 2 ^ n * Surreal.powHalf (n + k) = ↑m * Surreal.powHalf k
<VAR>m₁ m₂ : ℤ<VAR>y₁ y₂ : ℕ<VAR>h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂<GOAL>↑m₁ * Surreal.powHalf y₂ = ↑m₂ * Surreal.powHalf y₁
<VAR>m : ℤ<VAR>p : ↥(Submonoid.powers 2)<GOAL>Surreal.dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = ↑m * Surreal.powHalf (Submonoid.log p)
<VAR>m : ℤ<VAR>n : ℕ<GOAL>Surreal.dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • Surreal.powHalf n
<VAR>m : ℤ<VAR>n : ℕ<GOAL>↑m * Surreal.powHalf (Submonoid.log (Submonoid.pow 2 n)) = ↑m * Surreal.powHalf n
<VAR>α : Type u<VAR>g : Ordinal.{u} → α<GOAL>¬Set.InjOn g (Set.Iio (SuccOrder.succ (Cardinal.mk α)).ord)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>Monotone (OrdinalApprox.lfpApprox f x)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a : Ordinal.{u}<GOAL>x ≤ OrdinalApprox.lfpApprox f x a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h : x ≤ f x<VAR>a : Ordinal.{u}<GOAL>OrdinalApprox.lfpApprox f x (a + 1) = f (OrdinalApprox.lfpApprox f x a)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a ≤ b<VAR>h : OrdinalApprox.lfpApprox f x a ∈ Function.fixedPoints ⇑f<GOAL>OrdinalApprox.lfpApprox f x b = OrdinalApprox.lfpApprox f x a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>∃ a < (Order.succ (Cardinal.mk α)).ord, ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b c : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a < b<VAR>h_ac : a ≤ c<VAR>h_fab : OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b<GOAL>OrdinalApprox.lfpApprox f x c ∈ Function.fixedPoints ⇑f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_init : x ≤ f x<GOAL>OrdinalApprox.lfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a : α<VAR>h_a : a ∈ Function.fixedPoints ⇑f<VAR>h_le_init : x ≤ a<VAR>i : Ordinal.{u}<GOAL>OrdinalApprox.lfpApprox f x i ≤ a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>OrdinalApprox.lfpApprox f ⊥ (Order.succ (Cardinal.mk α)).ord = OrderHom.lfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>OrderHom.lfp f ∈ Set.range (OrdinalApprox.lfpApprox f ⊥)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>Antitone (OrdinalApprox.gfpApprox f x)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a : Ordinal.{u}<GOAL>OrdinalApprox.gfpApprox f x a ≤ x
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h : f x ≤ x<VAR>a : Ordinal.{u}<GOAL>OrdinalApprox.gfpApprox f x (a + 1) = f (OrdinalApprox.gfpApprox f x a)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h_init : f x ≤ x<VAR>h_ab : a ≤ b<VAR>h : OrdinalApprox.gfpApprox f x a ∈ Function.fixedPoints ⇑f<GOAL>OrdinalApprox.gfpApprox f x b = OrdinalApprox.gfpApprox f x a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>∃ a < (Order.succ (Cardinal.mk α)).ord, ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.gfpApprox f x a = OrdinalApprox.gfpApprox f x b
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_init : f x ≤ x<GOAL>OrdinalApprox.gfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a : α<VAR>h_a : a ∈ Function.fixedPoints ⇑f<VAR>h_le_init : a ≤ x<VAR>i : Ordinal.{u}<GOAL>a ≤ OrdinalApprox.gfpApprox f x i
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>OrdinalApprox.gfpApprox f ⊤ (Order.succ (Cardinal.mk α)).ord = OrderHom.gfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>OrderHom.gfp f ∈ Set.range (OrdinalApprox.gfpApprox f ⊤)
<VAR>x : SetTheory.PGame<GOAL>x.birthday = max (Ordinal.lsub fun i => (x.moveLeft i).birthday) (Ordinal.lsub fun i => (x.moveRight i).birthday)
<VAR>x : SetTheory.PGame<VAR>i : x.LeftMoves<GOAL>(x.moveLeft i).birthday < x.birthday
<VAR>x : SetTheory.PGame<VAR>i : x.RightMoves<GOAL>(x.moveRight i).birthday < x.birthday
<VAR>x : SetTheory.PGame<VAR>o : Ordinal.{u_1}<GOAL>o < x.birthday ↔ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday
<VAR>x y : SetTheory.PGame<GOAL>x.Relabelling y → x.birthday = y.birthday
<VAR>x : SetTheory.PGame<GOAL>x.birthday = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves
<VAR>x : SetTheory.PGame<GOAL>(-x).birthday = x.birthday
<VAR>x : SetTheory.PGame<GOAL>x ≤ x.birthday.toPGame
<VAR>x : SetTheory.PGame<GOAL>-x.birthday.toPGame ≤ x
<VAR>x y : SetTheory.PGame<GOAL>(x + y).birthday = x.birthday.nadd y.birthday
<VAR>a : SetTheory.PGame<GOAL>(a + 0).birthday = a.birthday
<VAR>a : SetTheory.PGame<GOAL>(0 + a).birthday = a.birthday
<VAR>a : SetTheory.PGame<GOAL>(a + 1).birthday = Order.succ a.birthday
<VAR>a : SetTheory.PGame<GOAL>(1 + a).birthday = Order.succ a.birthday
<VAR>n : ℕ<GOAL>(↑n).birthday = ↑n
<VAR>a : SetTheory.PGame<VAR>n : ℕ<GOAL>(a + ↑n).birthday = a.birthday + ↑n
<VAR>a : SetTheory.PGame<VAR>n : ℕ<GOAL>(↑n + a).birthday = a.birthday + ↑n
SetTheory.PGame.nim o = SetTheory.PGame.mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) o₂)) fun o₂ => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) o₂)
<VAR>o : Ordinal.{u_1}<GOAL>(SetTheory.PGame.nim o).LeftMoves = (Quotient.out o).α
<VAR>o : Ordinal.{u_1}<GOAL>(SetTheory.PGame.nim o).RightMoves = (Quotient.out o).α
HEq (SetTheory.PGame.nim o).moveLeft fun i => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) i)
HEq (SetTheory.PGame.nim o).moveRight fun i => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) i)
<VAR>o : Ordinal.{u_1}<VAR>i : (SetTheory.PGame.nim o).LeftMoves<GOAL>↑(SetTheory.PGame.toLeftMovesNim.symm i) < o
<VAR>o : Ordinal.{u_1}<VAR>i : (SetTheory.PGame.nim o).RightMoves<GOAL>↑(SetTheory.PGame.toRightMovesNim.symm i) < o
<VAR>o : Ordinal.{u}<VAR>i : (SetTheory.PGame.nim o).LeftMoves<GOAL>(SetTheory.PGame.nim o).moveLeft i = SetTheory.PGame.nim ↑(SetTheory.PGame.toLeftMovesNim.symm i)
<VAR>o : Ordinal.{u_1}<VAR>i : ↑(Set.Iio o)<GOAL>(SetTheory.PGame.nim o).moveLeft (SetTheory.PGame.toLeftMovesNim i) = SetTheory.PGame.nim ↑i
<VAR>o : Ordinal.{u_1}<VAR>i : (SetTheory.PGame.nim o).RightMoves<GOAL>(SetTheory.PGame.nim o).moveRight i = SetTheory.PGame.nim ↑(SetTheory.PGame.toRightMovesNim.symm i)
<VAR>o : Ordinal.{u_1}<VAR>i : ↑(Set.Iio o)<GOAL>(SetTheory.PGame.nim o).moveRight (SetTheory.PGame.toRightMovesNim i) = SetTheory.PGame.nim ↑i
<GOAL>SetTheory.PGame.nim 0 ≈ 0
<GOAL>default = SetTheory.PGame.toLeftMovesNim ⟨0, ⋯⟩
<GOAL>default = SetTheory.PGame.toRightMovesNim ⟨0, ⋯⟩
<VAR>i : (SetTheory.PGame.nim 1).LeftMoves<GOAL>SetTheory.PGame.toLeftMovesNim.symm i = ⟨0, ⋯⟩
<VAR>i : (SetTheory.PGame.nim 1).RightMoves<GOAL>SetTheory.PGame.toRightMovesNim.symm i = ⟨0, ⋯⟩
<VAR>x : (SetTheory.PGame.nim 1).LeftMoves<GOAL>(SetTheory.PGame.nim 1).moveLeft x = SetTheory.PGame.nim 0
<VAR>x : (SetTheory.PGame.nim 1).RightMoves<GOAL>(SetTheory.PGame.nim 1).moveRight x = SetTheory.PGame.nim 0
<GOAL>SetTheory.PGame.nim 1 ≈ SetTheory.PGame.star
<VAR>o : Ordinal.{u_1}<GOAL>(SetTheory.PGame.nim o).birthday = o
<VAR>o : Ordinal.{u_1}<GOAL>-SetTheory.PGame.nim o = SetTheory.PGame.nim o
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>(SetTheory.PGame.nim o).Fuzzy 0
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>SetTheory.PGame.nim o₁ + SetTheory.PGame.nim o₂ ≈ 0 ↔ o₁ = o₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>(SetTheory.PGame.nim o₁ + SetTheory.PGame.nim o₂).Fuzzy 0 ↔ o₁ ≠ o₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>SetTheory.PGame.nim o₁ ≈ SetTheory.PGame.nim o₂ ↔ o₁ = o₂
<VAR>G : SetTheory.PGame<GOAL>G.grundyValue = Ordinal.mex fun i => (G.moveLeft i).grundyValue
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G ≈ SetTheory.PGame.nim G.grundyValue
<VAR>G : SetTheory.PGame<VAR>G.Impartial<VAR>o : Ordinal.{u_1}<GOAL>G.grundyValue = o ↔ G ≈ SetTheory.PGame.nim o
<VAR>o : Ordinal.{u}<GOAL>(SetTheory.PGame.nim o).grundyValue = o
<VAR>G H : SetTheory.PGame<VAR>G.Impartial<VAR>H.Impartial<GOAL>G.grundyValue = H.grundyValue ↔ G ≈ H
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G.grundyValue = 0 ↔ G ≈ 0
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>(-G).grundyValue = G.grundyValue
<VAR>G : SetTheory.PGame<VAR>G.Impartial<GOAL>G.grundyValue = Ordinal.mex fun i => (G.moveRight i).grundyValue
<VAR>n m : ℕ<GOAL>(SetTheory.PGame.nim ↑n + SetTheory.PGame.nim ↑m).grundyValue = ↑(n ^^^ m)
<VAR>n m : ℕ<GOAL>SetTheory.PGame.nim ↑n + SetTheory.PGame.nim ↑m ≈ SetTheory.PGame.nim ↑(n ^^^ m)
<VAR>G H : SetTheory.PGame<VAR>G.Impartial<VAR>H.Impartial<VAR>n m : ℕ<VAR>hG : G.grundyValue = ↑n<VAR>hH : H.grundyValue = ↑m<GOAL>(G + H).grundyValue = ↑(n ^^^ m)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>Quiver V<VAR>Quiver W<VAR>obj : V → W<VAR>map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>X : V<GOAL>{ obj := obj, map := map }.obj X = obj X
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>Quiver V<VAR>Quiver W<VAR>obj : V → W<VAR>map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>X Y : V<VAR>f : X ⟶ Y<GOAL>{ obj := obj, map := map }.map f = map f
<VAR>V : Type u<VAR>Quiver V<VAR>W : Type u₂<VAR>Quiver W<VAR>F G : V ⥤q W<VAR>h_obj : ∀ (X : V), F.obj X = G.obj X<VAR>h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))<GOAL>F = G
<VAR>V : Type u_1<VAR>Quiver V<VAR>X : V<GOAL>(𝟭q V).obj X = X
<VAR>V : Type u_1<VAR>Quiver V<GOAL>∀ {X Y : V} (f : X ⟶ Y), (𝟭q V).map f = f
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>W : Type u_3<VAR>Quiver W<VAR>F : U ⥤q V<VAR>G : V ⥤q W<GOAL>∀ {X Y : U} (f : X ⟶ Y), (F ⋙q G).map f = G.map (F.map f)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>W : Type u_3<VAR>Quiver W<VAR>F : U ⥤q V<VAR>G : V ⥤q W<VAR>X : U<GOAL>(F ⋙q G).obj X = G.obj (F.obj X)
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>F : U ⥤q V<GOAL>F ⋙q 𝟭q V = F
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>F : U ⥤q V<GOAL>𝟭q U ⋙q F = F
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Z : Type u_4<VAR>Quiver U<VAR>Quiver V<VAR>Quiver W<VAR>Quiver Z<VAR>F : U ⥤q V<VAR>G : V ⥤q W<VAR>H : W ⥤q Z<GOAL>F ⋙q G ⋙q H = F ⋙q (G ⋙q H)
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>Quiver U<VAR>Quiver V<VAR>F : U ⥤q V<VAR>X Y : U<VAR>f g : X ⟶ Y<VAR>h : f = g<GOAL>F.map f = F.map g
<VAR>V : Type u<VAR>a b : Quiver.Empty V<GOAL>(a ⟶ b) = PEmpty.{u}
<VAR>a b : Ordinal.{u}<GOAL>a ^ b = if a = 0 then 1 - b else b.limitRecOn 1 (fun x IH => IH * a) fun b x => b.bsup
<VAR>a : Ordinal.{u_1}<GOAL>a ^ 0 = 1
<VAR>a b : Ordinal.{u_1}<GOAL>a ^ Order.succ b = a ^ b * a
<VAR>a : Ordinal.{u_1}<VAR>b : Ordinal.{u_1}<VAR>a0 : 0 < a<GOAL>0 < a ^ b
<VAR>a : Ordinal.{u_1}<VAR>b : Ordinal.{u_1}<VAR>a0 : a ≠ 0<GOAL>a ^ b ≠ 0
<VAR>a : Ordinal.{u_1}<VAR>h : 1 < a<GOAL>Ordinal.IsNormal fun x => a ^ x
<VAR>a b c : Ordinal.{u_1}<VAR>a1 : 1 < a<GOAL>a ^ b < a ^ c ↔ b < c
<VAR>a b c : Ordinal.{u_1}<VAR>a1 : 1 < a<GOAL>a ^ b ≤ a ^ c ↔ b ≤ c
<VAR>a b c : Ordinal.{u_1}<VAR>a1 : 1 < a<GOAL>a ^ b = a ^ c ↔ b = c
<VAR>a b : Ordinal.{u_1}<VAR>a1 : 1 < a<GOAL>b.IsLimit → (a ^ b).IsLimit
<VAR>a b : Ordinal.{u_1}<VAR>c : Ordinal.{u_1}<VAR>ab : a ≤ b<GOAL>a ^ c ≤ b ^ c
<VAR>a : Ordinal.{u_1}<VAR>b : Ordinal.{u_1}<VAR>b1 : 0 < b<GOAL>a ≤ a ^ b
<VAR>a : Ordinal.{u_1}<VAR>b : Ordinal.{u_1}<VAR>a1 : 1 < a<GOAL>b ≤ a ^ b
<VAR>a b c : Ordinal.{u_1}<VAR>ab : a < b<GOAL>a ^ Order.succ c < b ^ Order.succ c
<VAR>a : Ordinal.{u_1}<VAR>b c : Ordinal.{u_1}<VAR>h : b ≤ c<GOAL>a ^ b ∣ a ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>a1 : 1 < a<GOAL>a ^ b ∣ a ^ c ↔ b ≤ c
<VAR>a b c : Ordinal.{u_1}<GOAL>a ^ (b * c) = (a ^ b) ^ c
<VAR>b x : Ordinal.{u_1}<VAR>h : 1 < b<GOAL>{o | x < b ^ o}.Nonempty
<VAR>b : Ordinal.{u_1}<VAR>h : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>Ordinal.log b x = (sInf {o | x < b ^ o}).pred
<VAR>b : Ordinal.{u_1}<VAR>h : ¬1 < b<VAR>x : Ordinal.{u_1}<GOAL>Ordinal.log b x = 0
<VAR>b : Ordinal.{u_1}<VAR>h : b ≤ 1<VAR>x : Ordinal.{u_1}<GOAL>Ordinal.log b x = 0
<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.log 0 b = 0
<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.log b 0 = 0
<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.log 1 b = 0
<VAR>b x : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<GOAL>Order.succ (Ordinal.log b x) = sInf {o | x < b ^ o}
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>x < b ^ Order.succ (Ordinal.log b x)
<VAR>b : Ordinal.{u_1}<VAR>x : Ordinal.{u_1}<VAR>hx : x ≠ 0<GOAL>b ^ Ordinal.log b x ≤ x
<VAR>b x c : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<GOAL>b ^ c ≤ x ↔ c ≤ Ordinal.log b x
<VAR>b x c : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<GOAL>x < b ^ c ↔ Ordinal.log b x < c
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : o ≠ 0<VAR>hbo : b ≤ o<GOAL>0 < Ordinal.log b o
<VAR>b o : Ordinal.{u_1}<VAR>hbo : o < b<GOAL>Ordinal.log b o = 0
<VAR>b : Ordinal.{u_1}<VAR>x y : Ordinal.{u_1}<VAR>xy : x ≤ y<GOAL>Ordinal.log b x ≤ Ordinal.log b y
<VAR>b x : Ordinal.{u_1}<GOAL>Ordinal.log b x ≤ x
<VAR>b : Ordinal.{u_1}<GOAL>Ordinal.log b 1 = 0
<VAR>b : Ordinal.{u_1}<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>o % b ^ Ordinal.log b o < o
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : o ≠ 0<VAR>hbo : b ≤ o<GOAL>Ordinal.log b (o % b ^ Ordinal.log b o) < Ordinal.log b o
<VAR>b v : Ordinal.{u_1}<VAR>hb : b ≠ 0<VAR>u : Ordinal.{u_1}<VAR>hv : v ≠ 0<VAR>w : Ordinal.{u_1}<GOAL>0 < b ^ u * v + w
<VAR>b u w : Ordinal.{u_1}<VAR>v : Ordinal.{u_1}<VAR>hw : w < b ^ u<GOAL>b ^ u * v + w < b ^ u * Order.succ v
<VAR>b u v w : Ordinal.{u_1}<VAR>hvb : v < b<VAR>hw : w < b ^ u<GOAL>b ^ u * v + w < b ^ Order.succ u
<VAR>b u v w : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hv : v ≠ 0<VAR>hvb : v < b<VAR>hw : w < b ^ u<GOAL>Ordinal.log b (b ^ u * v + w) = u
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>Ordinal.log b (b ^ x) = x
<VAR>b : Ordinal.{u_1}<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>0 < o / b ^ Ordinal.log b o
<VAR>b : Ordinal.{u_1}<VAR>o : Ordinal.{u_1}<VAR>hb : 1 < b<GOAL>o / b ^ Ordinal.log b o < b
<VAR>x y : Ordinal.{u_1}<VAR>b : Ordinal.{u_1}<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Ordinal.log b x + Ordinal.log b y ≤ Ordinal.log b (x * y)
<VAR>m n : ℕ<GOAL>↑(m ^ n) = ↑m ^ ↑n
<VAR>o : Ordinal.{u_1}<VAR>ho : 0 < o<GOAL>(Ordinal.sup fun n => o ^ ↑n) = o ^ ω
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<VAR>e : b ⟶ a<GOAL>Quiver.Path.nil ≠ p.cons e
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<VAR>e : b ⟶ a<GOAL>p.cons e ≠ Quiver.Path.nil
<VAR>V : Type u<VAR>Quiver V<VAR>a b c d : V<VAR>p : Quiver.Path a b<VAR>p' : Quiver.Path a c<VAR>e : b ⟶ d<VAR>e' : c ⟶ d<VAR>h : p.cons e = p'.cons e'<GOAL>b = c
<VAR>V : Type u<VAR>Quiver V<VAR>a b c d : V<VAR>p : Quiver.Path a b<VAR>p' : Quiver.Path a c<VAR>e : b ⟶ d<VAR>e' : c ⟶ d<VAR>h : p.cons e = p'.cons e'<GOAL>HEq p p'
<VAR>V : Type u<VAR>Quiver V<VAR>a b c d : V<VAR>p : Quiver.Path a b<VAR>p' : Quiver.Path a c<VAR>e : b ⟶ d<VAR>e' : c ⟶ d<VAR>h : p.cons e = p'.cons e'<GOAL>HEq e e'
<VAR>V : Type u<VAR>Quiver V<VAR>a : V<GOAL>Quiver.Path.nil.length = 0
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>p : Quiver.Path a b<VAR>e : b ⟶ c<GOAL>(p.cons e).length = p.length + 1
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<VAR>hzero : p.length = 0<GOAL>a = b
<VAR>V : Type u<VAR>Quiver V<VAR>a b c d : V<VAR>p : Quiver.Path a b<VAR>q : Quiver.Path b c<VAR>e : c ⟶ d<GOAL>p.comp (q.cons e) = (p.comp q).cons e
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<GOAL>p.comp Quiver.Path.nil = p
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<GOAL>Quiver.Path.nil.comp p = p
<VAR>V : Type u<VAR>Quiver V<VAR>a b c d : V<VAR>p : Quiver.Path a b<VAR>q : Quiver.Path b c<VAR>r : Quiver.Path c d<GOAL>(p.comp q).comp r = p.comp (q.comp r)
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<VAR>c : V<VAR>q : Quiver.Path b c<GOAL>(p.comp q).length = p.length + q.length
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>p₁ p₂ : Quiver.Path a b<VAR>q₁ q₂ : Quiver.Path b c<VAR>hq : q₁.length = q₂.length<GOAL>p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂