ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>Quiver.SingleObj.pathEquivList.symm (a :: l) = (Quiver.SingleObj.pathEquivList.symm l).cons a
<VAR>M : Type u_1<VAR>Add M<VAR>U V : Ultrafilter M<VAR>p : M → Prop<GOAL>(∀ᶠ (m : M) in ↑(U + V), p m) ↔ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, p (m + m')
<VAR>M : Type u_1<VAR>Mul M<VAR>U V : Ultrafilter M<VAR>p : M → Prop<GOAL>(∀ᶠ (m : M) in ↑(U * V), p m) ↔ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, p (m * m')
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>V : Ultrafilter M<GOAL>Continuous fun x => x + V
<VAR>M : Type u_1<VAR>Semigroup M<VAR>V : Ultrafilter M<GOAL>Continuous fun x => x * V
<VAR>M : Type u_1<VAR>Semigroup M<VAR>a : Stream' M<VAR>m : M<VAR>hm : m ∈ Hindman.FP a<GOAL>∃ n, ∀ m' ∈ Hindman.FP (Stream'.drop n a), m * m' ∈ Hindman.FP a
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>a : Stream' M<VAR>m : M<VAR>hm : m ∈ Hindman.FS a<GOAL>∃ n, ∀ m' ∈ Hindman.FS (Stream'.drop n a), m + m' ∈ Hindman.FS a
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>a : Stream' M<GOAL>∃ U, U + U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ Hindman.FS a
<VAR>M : Type u_1<VAR>Semigroup M<VAR>a : Stream' M<GOAL>∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ Hindman.FP a
<VAR>M : Type u_1<VAR>Semigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U * U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<GOAL>∃ a, Hindman.FP a ⊆ s₀
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U + U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<GOAL>∃ a, Hindman.FS a ⊆ s₀
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>a : Stream' M<VAR>s : Set (Set M)<VAR>sfin : s.Finite<VAR>scov : Hindman.FS a ⊆ ⋃₀ s<GOAL>∃ c ∈ s, ∃ b, Hindman.FS b ⊆ c
<VAR>M : Type u_1<VAR>Semigroup M<VAR>a : Stream' M<VAR>s : Set (Set M)<VAR>sfin : s.Finite<VAR>scov : Hindman.FP a ⊆ ⋃₀ s<GOAL>∃ c ∈ s, ∃ b, Hindman.FP b ⊆ c
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>Nonempty M<VAR>s : Set (Set M)<VAR>sfin : s.Finite<VAR>scov : ⊤ ⊆ ⋃₀ s<GOAL>∃ c ∈ s, ∃ a, Hindman.FS a ⊆ c
<VAR>M : Type u_1<VAR>Semigroup M<VAR>Nonempty M<VAR>s : Set (Set M)<VAR>sfin : s.Finite<VAR>scov : ⊤ ⊆ ⋃₀ s<GOAL>∃ c ∈ s, ∃ a, Hindman.FP a ⊆ c
<VAR>M : Type u_1<VAR>Semigroup M<VAR>a : Stream' M<VAR>n : ℕ<GOAL>Hindman.FP (Stream'.drop n a) ⊆ Hindman.FP a
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>a : Stream' M<VAR>n : ℕ<GOAL>Hindman.FS (Stream'.drop n a) ⊆ Hindman.FS a
<VAR>M : Type u_1<VAR>Semigroup M<VAR>a : Stream' M<VAR>i : ℕ<GOAL>a.get i ∈ Hindman.FP a
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>a : Stream' M<VAR>i : ℕ<GOAL>a.get i ∈ Hindman.FS a
<VAR>M : Type u_1<VAR>Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<GOAL>a.get i * a.get j ∈ Hindman.FP a
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<GOAL>a.get i + a.get j ∈ Hindman.FS a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>hs : s.Nonempty<GOAL>∏ i ∈ s, a.get i ∈ Hindman.FP a
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>hs : s.Nonempty<GOAL>∑ i ∈ s, a.get i ∈ Hindman.FS a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>Ordinal.nfpFamily f a = Ordinal.sup (List.foldr f a)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>l : List ι<GOAL>List.foldr f a l ≤ Ordinal.nfpFamily f a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<VAR>a : Ordinal.{max u u_1}<GOAL>a ≤ Ordinal.nfpFamily f a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>a < Ordinal.nfpFamily f b ↔ ∃ l, a < List.foldr f b l
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>b : Ordinal.{max v u}<GOAL>Ordinal.nfpFamily f a ≤ b ↔ ∀ (l : List ι), List.foldr f a l ≤ b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a b : Ordinal.{max u v}<GOAL>(∀ (l : List ι), List.foldr f a l ≤ b) → Ordinal.nfpFamily f a ≤ b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>hf : ∀ (i : ι), Monotone (f i)<GOAL>Monotone (Ordinal.nfpFamily f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>b : Ordinal.{max v u}<VAR>hb : b < Ordinal.nfpFamily f a<VAR>i : ι<GOAL>f i b < Ordinal.nfpFamily f a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>Nonempty ι<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<VAR>a b : Ordinal.{max u v}<GOAL>(∀ (i : ι), f i b < Ordinal.nfpFamily f a) ↔ b < Ordinal.nfpFamily f a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>Nonempty ι<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<VAR>a b : Ordinal.{max u v}<GOAL>(∃ i, Ordinal.nfpFamily f a ≤ f i b) ↔ Ordinal.nfpFamily f a ≤ b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Monotone (f i)<VAR>a b : Ordinal.{max u v}<VAR>ab : a ≤ b<VAR>h : ∀ (i : ι), f i b ≤ b<GOAL>Ordinal.nfpFamily f a ≤ b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : ι<VAR>H : Ordinal.IsNormal (f i)<VAR>a : Ordinal.{max u v}<GOAL>f i (Ordinal.nfpFamily f a) = Ordinal.nfpFamily f a
<VAR>ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<VAR>a b : Ordinal.{max u v}<GOAL>(∀ (i : ι), f i b ≤ Ordinal.nfpFamily f a) ↔ b ≤ Ordinal.nfpFamily f a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<VAR>a : Ordinal.{max u u_1}<VAR>h : ∀ (i : ι), f i a = a<GOAL>Ordinal.nfpFamily f a = a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (⋂ i, Function.fixedPoints (f i))
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<GOAL>Ordinal.derivFamily f 0 = Ordinal.nfpFamily f 0
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>o : Ordinal.{max u v}<GOAL>Ordinal.derivFamily f (Order.succ o) = Ordinal.nfpFamily f (Order.succ (Ordinal.derivFamily f o))
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>o : Ordinal.{max u v}<GOAL>o.IsLimit → Ordinal.derivFamily f o = o.bsup fun a x => Ordinal.derivFamily f a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<GOAL>Ordinal.IsNormal (Ordinal.derivFamily f)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : ι<VAR>H : Ordinal.IsNormal (f i)<VAR>o : Ordinal.{max u v}<GOAL>f i (Ordinal.derivFamily f o) = Ordinal.derivFamily f o
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : ι), f i a ≤ a) ↔ ∃ o, Ordinal.derivFamily f o = a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : ι), f i a = a) ↔ ∃ o, Ordinal.derivFamily f o = a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), Ordinal.IsNormal (f i)<GOAL>Ordinal.derivFamily f = Ordinal.enumOrd (⋂ i, Function.fixedPoints (f i))
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<GOAL>o.nfpBFamily f = Ordinal.nfpFamily (o.familyOfBFamily f)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>l : List (Quotient.out o).α<GOAL>List.foldr (o.familyOfBFamily f) a l ≤ o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<GOAL>a ≤ o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a b : Ordinal.{max v u}<GOAL>a < o.nfpBFamily f b ↔ ∃ l, a < List.foldr (o.familyOfBFamily f) b l
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a b : Ordinal.{max v u}<GOAL>o.nfpBFamily f a ≤ b ↔ ∀ (l : List (Quotient.out o).α), List.foldr (o.familyOfBFamily f) a l ≤ b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a b : Ordinal.{max u v}<GOAL>(∀ (l : List (Quotient.out o).α), List.foldr (o.familyOfBFamily f) a l ≤ b) → o.nfpBFamily f a ≤ b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)<GOAL>Monotone (o.nfpBFamily f)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<VAR>a b : Ordinal.{max v u}<VAR>hb : b < o.nfpBFamily f a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>f i hi b < o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a) ↔ b < o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>(∃ i, ∃ (hi : i < o), o.nfpBFamily f a ≤ f i hi b) ↔ o.nfpBFamily f a ≤ b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)<VAR>a b : Ordinal.{max u v}<VAR>ab : a ≤ b<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ b<GOAL>o.nfpBFamily f a ≤ b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<GOAL>f i hi (o.nfpBFamily f a) = o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ o.nfpBFamily f a) ↔ b ≤ o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a<GOAL>o.nfpBFamily f a = a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (⋂ i, ⋂ (hi : i < o), Function.fixedPoints (f i hi))
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<GOAL>o.derivBFamily f = Ordinal.derivFamily (o.familyOfBFamily f)
<VAR>o : Ordinal.{u_1}<VAR>f : (b : Ordinal.{u_1}) → b < o → Ordinal.{max u_1 u_2} → Ordinal.{max u_1 u_2}<GOAL>Ordinal.IsNormal (o.derivBFamily f)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>f i hi (o.derivBFamily f a) = o.derivBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, o.derivBFamily f b = a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∃ b, o.derivBFamily f b = a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)<GOAL>o.derivBFamily f = Ordinal.enumOrd (⋂ i, ⋂ (hi : i < o), Function.fixedPoints (f i hi))
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Ordinal.nfp f = Ordinal.nfpFamily fun x => f
<VAR>f : Ordinal.{u} → Ordinal.{u}<GOAL>(fun a => Ordinal.sup fun n => f^[n] a) = Ordinal.nfp f
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<GOAL>f^[n] a ≤ Ordinal.nfp f a
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>a : Ordinal.{u_1}<GOAL>a ≤ Ordinal.nfp f a
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>a < Ordinal.nfp f b ↔ ∃ n, a < f^[n] b
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>Ordinal.nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>(∀ (n : ℕ), f^[n] a ≤ b) → Ordinal.nfp f a ≤ b
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : Monotone f<GOAL>Monotone (Ordinal.nfp f)
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>a b : Ordinal.{u_1}<GOAL>f b < Ordinal.nfp f a ↔ b < Ordinal.nfp f a
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>a b : Ordinal.{u_1}<GOAL>Ordinal.nfp f a ≤ f b ↔ Ordinal.nfp f a ≤ b
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Monotone f<VAR>a b : Ordinal.{u_1}<VAR>ab : a ≤ b<VAR>h : f b ≤ b<GOAL>Ordinal.nfp f a ≤ b
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>a : Ordinal.{u_1}<GOAL>f (Ordinal.nfp f a) = Ordinal.nfp f a
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>a b : Ordinal.{u_1}<GOAL>f b ≤ Ordinal.nfp f a ↔ b ≤ Ordinal.nfp f a
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>a : Ordinal.{u_1}<VAR>h : f a = a<GOAL>Ordinal.nfp f a = a
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>H : Ordinal.IsNormal f<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (Function.fixedPoints f)
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Ordinal.deriv f = Ordinal.derivFamily fun x => f
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Ordinal.deriv f 0 = Ordinal.nfp f 0
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.deriv f (Order.succ o) = Ordinal.nfp f (Order.succ (Ordinal.deriv f o))
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>o : Ordinal.{u}<GOAL>o.IsLimit → Ordinal.deriv f o = o.bsup fun a x => Ordinal.deriv f a
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<GOAL>Ordinal.IsNormal (Ordinal.deriv f)
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>h : Ordinal.nfp f = id<GOAL>Ordinal.deriv f = id
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>o : Ordinal.{u_1}<GOAL>f (Ordinal.deriv f o) = Ordinal.deriv f o
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>a : Ordinal.{u_1}<GOAL>f a ≤ a ↔ ∃ o, Ordinal.deriv f o = a
<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : Ordinal.IsNormal f<VAR>a : Ordinal.{u_1}<GOAL>f a = a ↔ ∃ o, Ordinal.deriv f o = a
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>H : Ordinal.IsNormal f<GOAL>Ordinal.deriv f = Ordinal.enumOrd (Function.fixedPoints f)
<VAR>a : Ordinal.{u_1}<GOAL>Ordinal.nfp (fun x => a + x) 0 = a * Ordinal.omega
<VAR>a b : Ordinal.{u_1}<VAR>hba : b ≤ a * Ordinal.omega<GOAL>Ordinal.nfp (fun x => a + x) b = a * Ordinal.omega
<VAR>a b : Ordinal.{u_1}<GOAL>a + b = b ↔ a * Ordinal.omega ≤ b
<VAR>a b : Ordinal.{u_1}<GOAL>a + b ≤ b ↔ a * Ordinal.omega ≤ b
<VAR>a b : Ordinal.{u}<GOAL>Ordinal.deriv (fun x => a + x) b = a * Ordinal.omega + b
<VAR>a : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>Ordinal.nfp (fun x => a * x) 1 = a ^ Ordinal.omega
<VAR>a : Ordinal.{u_1}<GOAL>Ordinal.nfp (fun x => a * x) 0 = 0
<GOAL>Ordinal.nfp (HMul.hMul 0) = id
<GOAL>Ordinal.deriv (HMul.hMul 0) = id
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ Ordinal.omega<GOAL>Ordinal.nfp (fun x => a * x) b = a ^ Ordinal.omega
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<GOAL>b = 0 ∨ a ^ Ordinal.omega ≤ b
<VAR>a b : Ordinal.{u_1}<GOAL>a * b = b ↔ a ^ Ordinal.omega ∣ b
<VAR>a b : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>a * b ≤ b ↔ a ^ Ordinal.omega ∣ b
<VAR>a c : Ordinal.{u}<VAR>b : Ordinal.{u}<VAR>ha : 0 < a<VAR>hc : 0 < c<VAR>hca : c ≤ a ^ Ordinal.omega<GOAL>Ordinal.nfp (fun x => a * x) (a ^ Ordinal.omega * b + c) = a ^ Ordinal.omega * Order.succ b
<VAR>a : Ordinal.{u}<VAR>ha : 0 < a<VAR>b : Ordinal.{u}<GOAL>Ordinal.deriv (fun x => a * x) b = a ^ Ordinal.omega * b
<VAR>α : Type u_1<VAR>s : Finset.Colex α<GOAL>{ ofColex := s.ofColex } = s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>{ ofColex := s }.ofColex = s
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>{ ofColex := s } = { ofColex := t } ↔ s = t
<VAR>α : Type u_1<VAR>s t : Finset.Colex α<GOAL>s.ofColex = t.ofColex ↔ s = t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>{ ofColex := s } ≠ { ofColex := t } ↔ s ≠ t
<VAR>α : Type u_1<VAR>s t : Finset.Colex α<GOAL>s.ofColex ≠ t.ofColex ↔ s ≠ t
<VAR>α : Type u_1<GOAL>Function.Injective Finset.Colex.toColex
<VAR>α : Type u_1<GOAL>Function.Injective Finset.Colex.ofColex
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t u : Finset α<VAR>a : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>htu : { ofColex := t } ≤ { ofColex := u }<VAR>has : a ∈ s<VAR>hat : a ∉ t<GOAL>∃ b ∈ u, b ∉ s ∧ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hts : { ofColex := t } ≤ { ofColex := s }<GOAL>s ⊆ t
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset.Colex α<GOAL>s ≤ t ↔ ∀ ⦃a : α⦄, a ∈ s.ofColex → a ∉ t.ofColex → ∃ b ∈ t.ofColex, b ∉ s.ofColex ∧ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<GOAL>{ ofColex := s } ≤ { ofColex := t } ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<GOAL>{ ofColex := s } < { ofColex := t } ↔ s ≠ t ∧ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>Monotone Finset.Colex.toColex
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>StrictMono Finset.Colex.toColex
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>{ ofColex := s } ≤ { ofColex := t }
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>h : s ⊂ t<GOAL>{ ofColex := s } < { ofColex := t }
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{ ofColex := ∅ } = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>⊥.ofColex = ∅
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>a : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>ht : ∀ b ∈ t, b ≤ a<VAR>b : α<GOAL>b ∈ s → b ≤ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>a : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>ht : ∀ b ∈ t, b < a<VAR>b : α<GOAL>b ∈ s → b < a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a : α<GOAL>{ ofColex := s } ≤ { ofColex := {a} } ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a : α<GOAL>{ ofColex := s } < { ofColex := {a} } ↔ ∀ b ∈ s, b < a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a : α<GOAL>{ ofColex := {a} } ≤ { ofColex := s } ↔ ∃ x ∈ s, a ≤ x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>{ ofColex := {a} } ≤ { ofColex := {b} } ↔ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>{ ofColex := {a} } < { ofColex := {b} } ↔ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset.Colex α<GOAL>s ≤ t ↔ ↑s.ofColex \ ↑t.ofColex ⊆ ↑(lowerClosure (↑t.ofColex \ ↑s.ofColex))
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t u : Finset α<VAR>DecidableEq α<VAR>hus : u ⊆ s<VAR>hut : u ⊆ t<GOAL>{ ofColex := s \ u } ≤ { ofColex := t \ u } ↔ { ofColex := s } ≤ { ofColex := t }
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t u : Finset α<VAR>DecidableEq α<VAR>hus : u ⊆ s<VAR>hut : u ⊆ t<GOAL>{ ofColex := s \ u } < { ofColex := t \ u } ↔ { ofColex := s } < { ofColex := t }
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>{ ofColex := s \ t } ≤ { ofColex := t \ s } ↔ { ofColex := s } ≤ { ofColex := t }
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>{ ofColex := s \ t } < { ofColex := t \ s } ↔ { ofColex := s } < { ofColex := t }
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := Finset.cons a s ha } ≤ { ofColex := Finset.cons b s hb } ↔ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := Finset.cons a s ha } < { ofColex := Finset.cons b s hb } ↔ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a b : α<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := insert a s } ≤ { ofColex := insert b s } ↔ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a b : α<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := insert a s } < { ofColex := insert b s } ↔ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a b : α<VAR>DecidableEq α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>{ ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Finset α<VAR>a b : α<VAR>DecidableEq α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>{ ofColex := s.erase a } < { ofColex := s.erase b } ↔ b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset.Colex α<VAR>hst : s ≠ t<GOAL>(symmDiff s.ofColex t.ofColex).Nonempty
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset α<GOAL>{ ofColex := s } < { ofColex := t } ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset.Colex α<GOAL>s < t ↔ ∃ a ∈ t.ofColex, a ∉ s.ofColex ∧ ∀ b ∈ s.ofColex, b ∉ t.ofColex → b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset α<GOAL>{ ofColex := s } ≤ { ofColex := t } ↔ ∀ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset.Colex α<GOAL>s ≤ t ↔ ∀ (h : s ≠ t), (symmDiff s.ofColex t.ofColex).max' ⋯ ∈ t.ofColex
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset α<GOAL>{ ofColex := s } < { ofColex := t } ↔ ∃ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset.Colex α<GOAL>s < t ↔ ∃ (h : s ≠ t), (symmDiff s.ofColex t.ofColex).max' ⋯ ∈ t.ofColex
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset α<GOAL>{ ofColex := s } < { ofColex := t } ↔ ∃ w ∈ t \ s, Finset.filter (fun x => w < x) s = Finset.filter (fun x => w < x) t
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset α<VAR>a : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hcard : s.card ≤ t.card<VAR>ha : a ∈ s<GOAL>{ ofColex := s.erase a } ≤ { ofColex := t.erase (t.min' ⋯) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : StrictMono f<GOAL>{ ofColex := Finset.image f s } ≤ { ofColex := Finset.image f t } ↔ { ofColex := s } ≤ { ofColex := t }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s t : Finset α<VAR>hf : StrictMono f<GOAL>{ ofColex := Finset.image f s } < { ofColex := Finset.image f t } ↔ { ofColex := s } < { ofColex := t }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : StrictMono f<GOAL>StrictMono fun s => { ofColex := Finset.image f s.ofColex }
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Fintype α<GOAL>{ ofColex := Finset.univ } = ⊤
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Fintype α<GOAL>⊤.ofColex = Finset.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>r : ℕ<GOAL>Finset.Colex.IsInitSeg ∅ r
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>r : ℕ<VAR>h₁ : Finset.Colex.IsInitSeg 𝒜₁ r<VAR>h₂ : Finset.Colex.IsInitSeg 𝒜₂ r<GOAL>𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Finset α<VAR>Fintype α<GOAL>t ∈ Finset.Colex.initSeg s ↔ s.card = t.card ∧ { ofColex := t } ≤ { ofColex := s }
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>Fintype α<GOAL>s ∈ Finset.Colex.initSeg s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>Fintype α<GOAL>(Finset.Colex.initSeg s).Nonempty
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>Fintype α<GOAL>Finset.Colex.IsInitSeg (Finset.Colex.initSeg s) s.card
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>Fintype α<VAR>h𝒜 : Finset.Colex.IsInitSeg 𝒜 r<VAR>h𝒜₀ : 𝒜.Nonempty<GOAL>∃ s, s.card = r ∧ 𝒜 = Finset.Colex.initSeg s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>Fintype α<GOAL>Finset.Colex.IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s, s.card = r ∧ 𝒜 = Finset.Colex.initSeg s
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>StrictMono fun s => ∑ k ∈ s.ofColex, n ^ k
<VAR>s t : Finset ℕ<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>∑ k ∈ s, n ^ k ≤ ∑ k ∈ t, n ^ k ↔ { ofColex := s } ≤ { ofColex := t }