ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>(∑ i : ι, f i) • ∑ i : ι, g i ≤ Fintype.card ι • ∑ i : ι, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>Fintype.card ι • ∑ i : ι, f i • g i ≤ (∑ i : ι, f i) • ∑ i : ι, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑s.card * ∑ i ∈ s, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<GOAL>↑s.card * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(∑ i ∈ s, f i) ^ 2 ≤ ↑s.card * ∑ i ∈ s, f i ^ 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>(∑ i : ι, f i) * ∑ i : ι, g i ≤ ↑(Fintype.card ι) * ∑ i : ι, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>↑(Fintype.card ι) * ∑ i : ι, f i * g i ≤ (∑ i : ι, f i) * ∑ i : ι, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>NonemptyInterval.toProd 1 = 1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>NonemptyInterval.toProd 0 = 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>(NonemptyInterval.toProd 1).1 = 1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>(NonemptyInterval.toProd 0).1 = 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>(NonemptyInterval.toProd 1).2 = 1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>(NonemptyInterval.toProd 0).2 = 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>↑0 = 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>↑1 = 1
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>NonemptyInterval.pure 1 = 1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>NonemptyInterval.pure 0 = 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>Interval.pure 1 = 1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>Interval.pure 0 = 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>0 ≠ ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>1 ≠ ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>Zero α<GOAL>⊥ ≠ 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>One α<GOAL>⊥ ≠ 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<GOAL>↑0 = 0
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>One α<GOAL>↑1 = 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>One α<GOAL>1 ∈ 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<GOAL>0 ∈ 0
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s t : NonemptyInterval α<GOAL>(s * t).toProd = s.toProd * t.toProd
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s t : NonemptyInterval α<GOAL>(s + t).toProd = s.toProd + t.toProd
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s t : NonemptyInterval α<GOAL>(s + t).toProd.1 = s.toProd.1 + t.toProd.1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s t : NonemptyInterval α<GOAL>(s * t).toProd.1 = s.toProd.1 * t.toProd.1
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s t : NonemptyInterval α<GOAL>(s + t).toProd.2 = s.toProd.2 + t.toProd.2
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s t : NonemptyInterval α<GOAL>(s * t).toProd.2 = s.toProd.2 * t.toProd.2
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s t : NonemptyInterval α<GOAL>↑(s * t) = ↑s * ↑t
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s t : NonemptyInterval α<GOAL>↑(s + t) = ↑s + ↑t
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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 b : α<GOAL>NonemptyInterval.pure a + NonemptyInterval.pure b = NonemptyInterval.pure (a + b)
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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 b : α<GOAL>NonemptyInterval.pure a * NonemptyInterval.pure b = NonemptyInterval.pure (a * b)
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>t : Interval α<GOAL>⊥ * t = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>t : Interval α<GOAL>⊥ + t = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s : Interval α<GOAL>s + ⊥ = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s : Interval α<GOAL>s * ⊥ = ⊥
<VAR>α : Type u_2<VAR>Monoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s : NonemptyInterval α<VAR>n : ℕ<GOAL>(s ^ n).toProd = s.toProd ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s : NonemptyInterval α<VAR>n : ℕ<GOAL>(n • s).toProd = n • s.toProd
<VAR>α : Type u_2<VAR>Monoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s : NonemptyInterval α<VAR>n : ℕ<GOAL>(s ^ n).toProd.1 = s.toProd.1 ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s : NonemptyInterval α<VAR>n : ℕ<GOAL>(n • s).toProd.1 = n • s.toProd.1
<VAR>α : Type u_2<VAR>Monoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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>s : NonemptyInterval α<VAR>n : ℕ<GOAL>(s ^ n).toProd.2 = s.toProd.2 ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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>s : NonemptyInterval α<VAR>n : ℕ<GOAL>(n • s).toProd.2 = n • s.toProd.2
<VAR>α : Type u_2<VAR>Monoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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 : α<VAR>n : ℕ<GOAL>NonemptyInterval.pure a ^ n = NonemptyInterval.pure (a ^ n)
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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 : α<VAR>n : ℕ<GOAL>n • NonemptyInterval.pure a = NonemptyInterval.pure (n • a)
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : NonemptyInterval α<VAR>n : ℕ<GOAL>↑(n • s) = n • ↑s
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : NonemptyInterval α<VAR>n : ℕ<GOAL>↑(s ^ n) = ↑s ^ n
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>n : ℕ<GOAL>n ≠ 0 → ⊥ ^ n = ⊥
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>n : ℕ<GOAL>n ≠ 0 → n • ⊥ = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>(s - t).toProd.1 = s.toProd.1 - t.toProd.2
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>(s - t).toProd.2 = s.toProd.2 - t.toProd.1
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>↑(s - t) = ↑s - ↑t
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>a - b ∈ s - t
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>NonemptyInterval.pure a - NonemptyInterval.pure b = NonemptyInterval.pure (a - b)
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>t : Interval α<GOAL>⊥ - t = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Interval α<GOAL>s - ⊥ = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>(s / t).toProd.1 = s.toProd.1 / t.toProd.2
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>(s / t).toProd.2 = s.toProd.2 / t.toProd.1
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<GOAL>↑(s / t) = ↑s / ↑t
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : NonemptyInterval α<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>a / b ∈ s / t
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>NonemptyInterval.pure a / NonemptyInterval.pure b = NonemptyInterval.pure (a / b)
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>t : Interval α<GOAL>⊥ / t = ⊥
<VAR>α : Type u_2<VAR>Preorder α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Interval α<GOAL>s / ⊥ = ⊥
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>s : NonemptyInterval α<GOAL>s⁻¹.toProd.1 = s.toProd.2⁻¹
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : NonemptyInterval α<GOAL>(-s).toProd.1 = -s.toProd.2
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>s : NonemptyInterval α<GOAL>s⁻¹.toProd.2 = s.toProd.1⁻¹
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : NonemptyInterval α<GOAL>(-s).toProd.2 = -s.toProd.1
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : NonemptyInterval α<GOAL>↑(-s) = -↑s
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>s : NonemptyInterval α<GOAL>↑s⁻¹ = (↑s)⁻¹
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>s : NonemptyInterval α<VAR>a : α<VAR>ha : a ∈ s<GOAL>a⁻¹ ∈ s⁻¹
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : NonemptyInterval α<VAR>a : α<VAR>ha : a ∈ s<GOAL>-a ∈ -s
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>a : α<GOAL>(NonemptyInterval.pure a)⁻¹ = NonemptyInterval.pure a⁻¹
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>-NonemptyInterval.pure a = NonemptyInterval.pure (-a)
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<GOAL>-⊥ = ⊥
<VAR>α : Type u_2<VAR>OrderedCommGroup α<GOAL>⊥⁻¹ = ⊥
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>s t : NonemptyInterval α<GOAL>s * t = 1 ↔ ∃ a b, s = NonemptyInterval.pure a ∧ t = NonemptyInterval.pure b ∧ a * b = 1
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s t : NonemptyInterval α<GOAL>s + t = 0 ↔ ∃ a b, s = NonemptyInterval.pure a ∧ t = NonemptyInterval.pure b ∧ a + b = 0
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s t : Interval α<GOAL>s + t = 0 ↔ ∃ a b, s = Interval.pure a ∧ t = Interval.pure b ∧ a + b = 0
<VAR>α : Type u_2<VAR>OrderedCommGroup α<VAR>s t : Interval α<GOAL>s * t = 1 ↔ ∃ a b, s = Interval.pure a ∧ t = Interval.pure b ∧ a * b = 1
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : NonemptyInterval α<GOAL>0 ≤ s.length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>(NonemptyInterval.pure a).length = 0
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<GOAL>NonemptyInterval.length 0 = 0
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : NonemptyInterval α<GOAL>(-s).length = s.length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s t : NonemptyInterval α<GOAL>(s + t).length = s.length + t.length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s t : NonemptyInterval α<GOAL>(s - t).length = s.length + t.length
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>f : ι → NonemptyInterval α<VAR>s : Finset ι<GOAL>(∑ i ∈ s, f i).length = ∑ i ∈ s, (f i).length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : Interval α<GOAL>0 ≤ s.length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>(Interval.pure a).length = 0
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<GOAL>Interval.length 0 = 0
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s : Interval α<GOAL>(-s).length = s.length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s t : Interval α<GOAL>(s + t).length ≤ s.length + t.length
<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>s t : Interval α<GOAL>(s - t).length ≤ s.length + t.length
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedAddCommGroup α<VAR>f : ι → Interval α<VAR>s : Finset ι<GOAL>(∑ i ∈ s, f i).length ≤ ∑ i ∈ s, (f i).length
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f i • g (σ i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ AntivaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f (σ i) • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ AntivaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i < ∑ i ∈ s, f (σ i) • g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i • g (σ i) ≤ ∑ i : ι, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i • g (σ i) = ∑ i : ι, f i • g i ↔ Monovary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i • g (σ i) < ∑ i : ι, f i • g i ↔ ¬Monovary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) • g i ≤ ∑ i : ι, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Monovary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g i ≤ ∑ i : ι, f i • g (σ i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g (σ i) = ∑ i : ι, f i • g i ↔ Antivary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g i < ∑ i : ι, f i • g (σ i) ↔ ¬Antivary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g i ≤ ∑ i : ι, f (σ i) • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Antivary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>σ : Equiv.Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g i < ∑ i : ι, f (σ i) • g i ↔ ¬Antivary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g (σ i) ≤ ∑ i ∈ s, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g (σ i) = ∑ i ∈ s, f i * g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) * g i ≤ ∑ i ∈ s, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) * g i < ∑ i ∈ s, f i * g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f i * g (σ i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g (σ i) = ∑ i ∈ s, f i * g i ↔ AntivaryOn f (g ∘ ⇑σ) ↑s