ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>r : ℝ<GOAL>(↑r).Infinitesimal ↔ r = 0
<VAR>x : ℝ*<GOAL>(-x).Infinitesimal ↔ x.Infinitesimal
<VAR>f : ℕ → ℝ<VAR>h : Filter.Tendsto f Filter.atTop (𝓝 0)<GOAL>(Hyperreal.ofSeq f).Infinitesimal
<VAR>x : ℝ*<GOAL>x.Infinitesimal → x ≠ 0 → ∀ (r : ℝ), x ≠ ↑r
<VAR>x : ℝ*<VAR>hx : ¬x.Infinite<GOAL>(x - ↑x.st).Infinitesimal
<VAR>x : ℝ*<GOAL>x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹
<VAR>x : ℝ*<GOAL>x.Infinite → x⁻¹.Infinitesimal
<VAR>x : ℝ*<VAR>h0 : x ≠ 0<GOAL>x.Infinite ↔ x⁻¹.Infinitesimal
<VAR>x : ℝ*<GOAL>x⁻¹.InfinitePos ↔ x.Infinitesimal ∧ 0 < x
<VAR>x : ℝ*<GOAL>x⁻¹.InfiniteNeg ↔ x.Infinitesimal ∧ x < 0
<VAR>x : ℝ*<VAR>h : x ≠ 0<GOAL>x.Infinitesimal ↔ x⁻¹.Infinite
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hi : ¬x.Infinitesimal<VAR>hr : x.IsSt r<GOAL>x⁻¹.IsSt r⁻¹
<VAR>x : ℝ*<GOAL>x⁻¹.st = x.st⁻¹
<VAR>x y : ℝ*<GOAL>x.InfinitePos → ¬y.Infinitesimal → 0 < y → (x * y).InfinitePos
<VAR>x y : ℝ*<GOAL>¬x.Infinitesimal → 0 < x → y.InfinitePos → (x * y).InfinitePos
<VAR>x y : ℝ*<GOAL>¬x.Infinitesimal → x < 0 → y.InfiniteNeg → (x * y).InfinitePos
<VAR>x y : ℝ*<GOAL>¬x.Infinitesimal → x < 0 → y.InfinitePos → (x * y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>¬x.Infinitesimal → 0 < x → y.InfiniteNeg → (x * y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.InfinitePos → y.InfinitePos → (x * y).InfinitePos
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → y.InfiniteNeg → (x * y).InfinitePos
<VAR>x y : ℝ*<GOAL>x.InfinitePos → y.InfiniteNeg → (x * y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → y.InfinitePos → (x * y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.Infinite → ¬y.Infinitesimal → (x * y).Infinite
<VAR>x y : ℝ*<GOAL>¬x.Infinitesimal → y.Infinite → (x * y).Infinite
<VAR>x y : ℝ*<GOAL>x.Infinite → y.Infinite → (x * y).Infinite
<VAR>α : Type u<VAR>FinEnum α<VAR>x : α<GOAL>x ∈ FinEnum.toList α
<VAR>α : Type u<VAR>FinEnum α<GOAL>(FinEnum.toList α).Nodup
<VAR>α : Type u<VAR>DecidableEq α<VAR>s : Finset α<VAR>xs : List α<GOAL>s ∈ FinEnum.Finset.enum xs ↔ ∀ x ∈ s, x ∈ xs
<VAR>α : Type u_1<VAR>FinEnum α<VAR>β : α → Type u_2<VAR>(a : α) → FinEnum (β a)<VAR>xs : List α<VAR>f : (a : α) → a ∈ xs → β a<GOAL>f ∈ xs.pi fun x => FinEnum.toList (β x)
<VAR>α : Type u_1<VAR>FinEnum α<VAR>β : α → Type u_2<VAR>(a : α) → FinEnum (β a)<VAR>f : (a : α) → β a<GOAL>f ∈ List.Pi.enum β
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<VAR>x : α<VAR>b b' : Set α<VAR>hc : b ∈ c<VAR>hb : x ∈ b<VAR>hc' : b' ∈ c<VAR>hb' : x ∈ b'<GOAL>b = b'
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>y : α<GOAL>{x | r.Rel x y} ∈ r.classes
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(Setoid.ker f).classes ⊆ Set.range fun y => {x | f x = y}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Finite β<VAR>f : α → β<GOAL>(Setoid.ker f).classes.Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype β<VAR>f : α → β<VAR>Fintype ↑(Setoid.ker f).classes<GOAL>Fintype.card ↑(Setoid.ker f).classes ≤ Fintype.card β
<VAR>α : Type u_1<VAR>r₁ r₂ : Setoid α<GOAL>r₁ = r₂ ↔ ∀ (x : α), {y | r₁.Rel x y} = {y | r₂.Rel x y}
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x y : α<GOAL>r.Rel x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
<VAR>α : Type u_1<VAR>r₁ r₂ : Setoid α<GOAL>r₁ = r₂ ↔ r₁.classes = r₂.classes
<VAR>α : Type u_1<VAR>r : Setoid α<GOAL>∅ ∉ r.classes
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>a : α<GOAL>∃! b, b ∈ r.classes ∧ a ∈ b
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x : α<VAR>b : Set α<VAR>hc : b ∈ r.classes<VAR>hb : x ∈ b<VAR>b' : Set α<VAR>hc' : b' ∈ r.classes<VAR>hb' : x ∈ b'<GOAL>b = b'
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<VAR>s : Set α<VAR>y : α<VAR>hs : s ∈ c<VAR>hy : y ∈ s<GOAL>s = {x | (Setoid.mkClasses c H).Rel x y}
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<VAR>y : α<GOAL>{x | (Setoid.mkClasses c H).Rel x y} ∈ c
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<VAR>x : α<GOAL>{y | (Setoid.mkClasses c H).Rel x y} ∈ c
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<GOAL>c.PairwiseDisjoint id
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hu : ⋃₀ c = Set.univ<VAR>H : c.PairwiseDisjoint id<VAR>a : α<GOAL>∃! b, b ∈ c ∧ a ∈ b
<VAR>α : Type u_1<VAR>r : Setoid α<GOAL>Setoid.mkClasses r.classes ⋯ = r
<VAR>α : Type u_1<VAR>r : Setoid α<GOAL>⋃₀ r.classes = Set.univ
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>a : α<GOAL>↑(r.quotientEquivClasses ⟦a⟧) = {x | r.Rel x a}
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hc : Setoid.IsPartition c<VAR>s : Set α<VAR>h : s ∈ c<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>r : Setoid α<GOAL>Setoid.IsPartition r.classes
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hc : Setoid.IsPartition c<GOAL>c.PairwiseDisjoint id
<VAR>α : Type u_2<VAR>s : Set (Set α)<VAR>h₁ : s.PairwiseDisjoint id<VAR>h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x<VAR>h₃ : ∅ ∉ s<GOAL>Setoid.IsPartition s
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hc : Setoid.IsPartition c<GOAL>⋃₀ c = Set.univ
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hc : Setoid.IsPartition c<VAR>s : Set α<VAR>hs : s ∈ c<GOAL>∃ y, s = {x | (Setoid.mkClasses c ⋯).Rel x y}
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hc : Setoid.IsPartition c<GOAL>(Setoid.mkClasses c ⋯).classes = c
<VAR>α : Type u_1<VAR>c : Finset (Set α)<VAR>hc : Setoid.IsPartition ↑c<GOAL>hc.finpartition.parts = c
<VAR>α : Type u_1<VAR>f : Finpartition Set.univ<GOAL>Setoid.IsPartition ↑f.parts
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>self : IndexedPartition s<VAR>x : α<VAR>i j : ι<GOAL>x ∈ s i → x ∈ s j → i = j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>self : IndexedPartition s<VAR>i : ι<GOAL>self.some i ∈ s i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>self : IndexedPartition s<VAR>x : α<GOAL>x ∈ s (self.index x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>∃ i, x ∈ s i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<GOAL>⋃ i, s i = Set.univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<GOAL>Pairwise fun i j => Disjoint (s i) (s j)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<VAR>i : ι<GOAL>x ∈ s i ↔ hs.index x = i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>i : ι<GOAL>s i = {x | hs.index x = i}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>i : ι<GOAL>hs.index (hs.some i) = i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>hs.setoid.Rel (hs.some (hs.index x)) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x y : α<GOAL>hs.proj x = hs.proj y ↔ hs.index x = hs.index y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>hs.proj (hs.some (hs.index x)) = hs.proj x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>hs.equivQuotient (hs.index x) = hs.proj x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>hs.equivQuotient.symm (hs.proj x) = hs.index x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<GOAL>⇑hs.equivQuotient ∘ hs.index = hs.proj
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>hs.out (hs.proj x) = hs.some (hs.index x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : hs.Quotient<GOAL>hs.index (Quotient.out' x) = hs.index (hs.out x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : hs.Quotient<GOAL>hs.proj (hs.out x) = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>setOf (hs.setoid.Rel x) = s (hs.index x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : hs.Quotient<GOAL>hs.proj ⁻¹' {x} = s (hs.equivQuotient.symm x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>x : α<GOAL>hs.piecewise f x = f (hs.index x) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>h_injOn : ∀ (i : ι), Set.InjOn (f i) (s i)<VAR>h_disjoint : Set.univ.PairwiseDisjoint fun i => f i '' s i<GOAL>Function.Injective (hs.piecewise f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>t : ι → Set β<VAR>ht : IndexedPartition t<VAR>hf : ∀ (i : ι), Set.BijOn (f i) (s i) (t i)<GOAL>Function.Bijective (hs.piecewise f)
<VAR>a b c : SignType<GOAL>a * b * c = a * (b * c)
<VAR>a b : SignType<GOAL>a ≤ b → b ≤ a → a = b
<VAR>a b c : SignType<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a : SignType<GOAL>0 ≤ a ↔ a = 0 ∨ a = 1
<VAR>a : SignType<GOAL>0 ≤ a ↔ a ≠ -1
<VAR>a : SignType<GOAL>-1 < a ↔ 0 ≤ a
<VAR>a : SignType<GOAL>a ≤ 0 ↔ a = -1 ∨ a = 0
<VAR>a : SignType<GOAL>a ≤ 0 ↔ a ≠ 1
<VAR>a : SignType<GOAL>a < 1 ↔ a ≤ 0
<VAR>a : SignType<GOAL>a < 0 ↔ a = -1
<VAR>a : SignType<GOAL>a ≤ -1 ↔ a = -1
<VAR>a : SignType<GOAL>0 < a ↔ a = 1
<VAR>a : SignType<GOAL>1 ≤ a ↔ a = 1
<VAR>a : SignType<GOAL>a = -a ↔ a = 0
<VAR>a : SignType<GOAL>-a = a ↔ a = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Neg α<VAR>β : Type u_2<VAR>One β<VAR>Neg β<VAR>Zero β<VAR>f : α → β<VAR>h₁ : f 1 = 1<VAR>h₂ : f 0 = 0<VAR>h₃ : f (-1) = -1<VAR>s : SignType<GOAL>f ↑s = ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>AddGroupWithOne α<VAR>One β<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>OneHomClass F α β<VAR>f : F<VAR>s : SignType<GOAL>f ↑s = ↑s
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Neg α<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Neg α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Neg α<GOAL>↑(-1) = -1
<VAR>α : Type u_2<VAR>One α<VAR>SubtractionMonoid α<VAR>s : SignType<GOAL>↑(-s) = -↑s
<VAR>α : Type u_2<VAR>AddGroupWithOne α<VAR>s : SignType<GOAL>↑↑s = ↑s
<VAR>α : Type u_1<VAR>MulZeroOneClass α<VAR>HasDistribNeg α<GOAL>∀ (a : SignType), SignType.castHom a = ↑a
<VAR>α : Type u_1<VAR>f : SignType → α<GOAL>Set.range f = {f SignType.zero, f SignType.neg, f SignType.pos}
<VAR>α : Type u_1<VAR>MulZeroOneClass α<VAR>HasDistribNeg α<VAR>a b : SignType<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>HasDistribNeg α<VAR>a : SignType<VAR>k : ℕ<GOAL>↑(a ^ k) = ↑a ^ k
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>HasDistribNeg α<VAR>a : SignType<VAR>k : ℤ<GOAL>↑(a ^ k) = ↑a ^ k
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<GOAL>SignType.sign 0 = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>ha : 0 < a<GOAL>SignType.sign a = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>ha : a < 0<GOAL>SignType.sign a = -1
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>SignType.sign a = 1 ↔ 0 < a
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>SignType.sign a = -1 ↔ a < 0
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>β : Type u_2<VAR>F : Type u_3<VAR>Zero β<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>FunLike F α β<VAR>ZeroHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>SignType.sign (f a) = SignType.sign a
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<GOAL>SignType.sign a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<GOAL>SignType.sign a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<GOAL>0 ≤ SignType.sign a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<GOAL>SignType.sign a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>Nontrivial α<GOAL>SignType.sign 1 = 1
<VAR>α : Type u_2<VAR>OrderedRing α<VAR>Nontrivial α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>n : ℤ<GOAL>SignType.sign ↑n = SignType.sign n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x y : α<GOAL>SignType.sign (x * y) = SignType.sign x * SignType.sign y
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x : α<GOAL>↑(SignType.sign x) * |x| = x
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x : α<GOAL>|x| * ↑(SignType.sign x) = x
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x : α<GOAL>↑(SignType.sign x) * x = |x|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x : α<GOAL>x * ↑(SignType.sign x) = |x|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x : α<VAR>n : ℕ<GOAL>SignType.sign (x ^ n) = SignType.sign x ^ n
<VAR>α : Type u_1<VAR>AddGroup α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>SignType.sign (-a) = -SignType.sign a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>SignType.sign (-a) = -SignType.sign a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.Nonempty<VAR>t : SignType<VAR>h : ∀ i ∈ s, SignType.sign (f i) = t<GOAL>SignType.sign (∑ i ∈ s, f i) = t
<VAR>n : ℤ<GOAL>n.sign = ↑(SignType.sign n)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → ℤ<GOAL>∃ β t sgn g, (∀ (b : β), g b ∈ s) ∧ t.card = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → ℤ<GOAL>∃ β x sgn g, (∀ (b : β), g b ∈ s) ∧ Fintype.card β = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
<VAR>α : Type u_1<VAR>Nonempty α<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : α → ℤ<VAR>n : ℕ<VAR>h : ∑ i ∈ s, (f i).natAbs ≤ n<GOAL>∃ β x sgn g, (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a
<VAR>s : ℕ<VAR>H : 1 ≤ s<GOAL>¬s ≤ Ordnode.delta * 0
<VAR>a b : ℕ<VAR>h₁ : Ordnode.delta * a < b<VAR>h₂ : Ordnode.delta * b < a<GOAL>False
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(l.node' x r).Sized
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (Ordnode.node s l x r).Sized<GOAL>Ordnode.node s l x r = l.node' x r
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>H : (Ordnode.node s l x r).Sized<GOAL>(Ordnode.node s l x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>hl : t.Sized<VAR>C : Ordnode α → Prop<VAR>H0 : C Ordnode.nil<VAR>H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)<GOAL>C t
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.Sized → t.size = t.realSize
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>ht : t.Sized<GOAL>t.size = 0 ↔ t = Ordnode.nil
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (Ordnode.node s l x r).Sized<GOAL>0 < s
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.dual.dual = t
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.dual.size = t.size
<VAR>l r : ℕ<GOAL>Ordnode.BalancedSz l r → Ordnode.BalancedSz r l
<VAR>l : ℕ<GOAL>Ordnode.BalancedSz l 0 ↔ l ≤ 1
<VAR>l r₁ r₂ : ℕ<VAR>h₁ : r₁ ≤ r₂<VAR>h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ Ordnode.delta * l<VAR>H : Ordnode.BalancedSz l r₁<GOAL>Ordnode.BalancedSz l r₂
<VAR>l r₁ r₂ : ℕ<VAR>h₁ : r₁ ≤ r₂<VAR>h₂ : l + r₂ ≤ 1 ∨ l ≤ Ordnode.delta * r₁<VAR>H : Ordnode.BalancedSz l r₂<GOAL>Ordnode.BalancedSz l r₁
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.Balanced → t.dual.Balanced
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>sz : ℕ<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>l.rotateL x (Ordnode.node sz m y r) = if m.size < Ordnode.ratio * r.size then l.node3L x m y r else l.node4L x m y r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<GOAL>l.rotateL x Ordnode.nil = l.node' x Ordnode.nil
<VAR>α : Type u_1<VAR>sz : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(Ordnode.node sz l x m).rotateR y r = if m.size < Ordnode.ratio * l.size then l.node3R x m y r else l.node4R x m y r
<VAR>α : Type u_1<VAR>y : α<VAR>r : Ordnode α<GOAL>Ordnode.nil.rotateR y r = Ordnode.nil.node' y r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(l.rotateR x r).dual = r.dual.rotateL x l.dual
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(l.balanceL x r).dual = r.dual.balanceR x l.dual
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hm : m.Sized<VAR>hr : r.Sized<GOAL>(l.node3L x m y r).Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hm : m.Sized<VAR>hr : r.Sized<GOAL>(l.node3R x m y r).Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(l.node3L x m y r).size = l.size + m.size + r.size + 2
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(l.node3R x m y r).size = l.size + m.size + r.size + 2
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.Sized → t.dual.Sized
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.dual.Sized ↔ t.Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(l.rotateL x r).Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(l.rotateR x r).Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hm : r.Sized<GOAL>(l.rotateL x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(l.balance' x r).Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(l.balance' x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>P Q : α → Prop<VAR>H : ∀ (a : α), P a → Q a<VAR>t : Ordnode α<GOAL>Ordnode.All P t → Ordnode.All Q t
<VAR>α : Type u_1<VAR>P Q : α → Prop<VAR>H : ∀ (a : α), P a → Q a<VAR>t : Ordnode α<GOAL>Ordnode.Any P t → Ordnode.Any Q t
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>x : α<GOAL>Ordnode.All P {x} ↔ P x
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>x : α<GOAL>Ordnode.Any P {x} ↔ P x
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>t : Ordnode α<GOAL>Ordnode.All P t.dual ↔ Ordnode.All P t
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>t : Ordnode α<GOAL>Ordnode.All P t ↔ ∀ (x : α), Ordnode.Emem x t → P x
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>t : Ordnode α<GOAL>Ordnode.Any P t ↔ ∃ x, Ordnode.Emem x t ∧ P x
<VAR>α : Type u_1<VAR>x : α<VAR>t : Ordnode α<GOAL>Ordnode.Emem x t ↔ ∀ (P : α → Prop), Ordnode.All P t → P x
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.node' x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.node3L x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.node3R x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.node4L x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.node4R x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.rotateL x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.rotateR x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>Ordnode.All P (l.balance' x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>r : List α<GOAL>Ordnode.foldr List.cons t r = t.toList ++ r
<VAR>α : Type u_1<GOAL>Ordnode.nil.toList = []
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(Ordnode.node s l x r).toList = l.toList ++ x :: r.toList
<VAR>α : Type u_1<VAR>x : α<VAR>t : Ordnode α<GOAL>Ordnode.Emem x t ↔ x ∈ t.toList
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.toList.length = t.realSize
<VAR>α : Type u_1<VAR>t₁ t₂ : Ordnode α<VAR>h₁ : t₁.Sized<VAR>h₂ : t₂.Sized<GOAL>t₁.Equiv t₂ ↔ t₁.toList = t₂.toList
<VAR>α : Type u_1<VAR>LE α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Sized<VAR>h_mem : x ∈ t<GOAL>0 < t.size
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>x : α<GOAL>t.dual.findMin' x = Ordnode.findMax' x t
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>x : α<GOAL>Ordnode.findMax' x t.dual = t.findMin' x
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.dual.findMin = t.findMax
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.eraseMin.dual = t.dual.eraseMax
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>l.splitMin' x r = (l.findMin' x, (Ordnode.node s l x r).eraseMin)
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>l.splitMax' x r = ((Ordnode.node s l x r).eraseMax, Ordnode.findMax' x r)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>t : Ordnode α<VAR>x : α<GOAL>Ordnode.All P t → P x → P (t.findMin' x)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>x : α<VAR>t : Ordnode α<GOAL>P x → Ordnode.All P t → P (Ordnode.findMax' x t)
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.merge Ordnode.nil = t
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>Ordnode.nil.merge t = t
<VAR>α : Type u_1<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<GOAL>(Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr) = if Ordnode.delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr else if Ordnode.delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr)) else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)
<VAR>α : Type u_1<VAR>Preorder α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<GOAL>(Ordnode.insert x t).dual = Ordnode.insert x t.dual
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<GOAL>l.balance x r = l.balance' x r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H1 : l.size = 0 → r.size ≤ 1<VAR>H2 : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ Ordnode.delta * l.size<GOAL>l.balanceL x r = l.balance x r
<VAR>n m : ℕ<GOAL>Ordnode.Raised n m ↔ n ≤ m ∧ m ≤ n + 1
<VAR>n m : ℕ<VAR>H : Ordnode.Raised n m<GOAL>n.dist m ≤ 1
<VAR>n m : ℕ<VAR>H : Ordnode.Raised n m<GOAL>m.dist n ≤ 1
<VAR>k : ℕ<VAR>n m : ℕ<VAR>H : Ordnode.Raised n m<GOAL>Ordnode.Raised (k + n) (k + m)
<VAR>k : ℕ<VAR>n m : ℕ<VAR>H : Ordnode.Raised n m<GOAL>Ordnode.Raised (n + k) (m + k)
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x₁ x₂ : α<VAR>r₁ r₂ : Ordnode α<VAR>H : Ordnode.Raised r₁.size r₂.size<GOAL>Ordnode.Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r'<GOAL>l.balanceL x r = l.balance' x r
<VAR>α : Type u_1<VAR>l r : Ordnode α<VAR>H : (∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨ ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r'<GOAL>(∃ l', Ordnode.Raised l' r.dual.size ∧ Ordnode.BalancedSz l' l.dual.size) ∨ ∃ r', Ordnode.Raised l.dual.size r' ∧ Ordnode.BalancedSz r.dual.size r'