ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ l, f i ≤ g i<GOAL>(List.map f l).prod ≤ (List.map g l).prod
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h₁ : ∀ i ∈ l, f i ≤ g i<VAR>h₂ : ∃ i ∈ l, f i < g i<GOAL>(List.map f l).sum < (List.map g l).sum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h₁ : ∀ i ∈ l, f i ≤ g i<VAR>h₂ : ∃ i ∈ l, f i < g i<GOAL>(List.map f l).prod < (List.map g l).prod
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>hl : l ≠ []<VAR>f g : ι → M<VAR>hlt : ∀ i ∈ l, f i < g i<GOAL>(List.map f l).prod < (List.map g l).prod
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>hl : l ≠ []<VAR>f g : ι → M<VAR>hlt : ∀ i ∈ l, f i < g i<GOAL>(List.map f l).sum < (List.map g l).sum
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>n : M<VAR>h : ∀ x ∈ l, x ≤ n<GOAL>l.sum ≤ l.length • n
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>n : M<VAR>h : ∀ x ∈ l, x ≤ n<GOAL>l.prod ≤ n ^ l.length
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>n : M<VAR>h : ∀ x ∈ l, n ≤ x<GOAL>l.length • n ≤ l.sum
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>n : M<VAR>h : ∀ x ∈ l, n ≤ x<GOAL>n ^ l.length ≤ l.prod
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h : (List.map f l).sum < (List.map g l).sum<GOAL>∃ i ∈ l, f i < g i
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h : (List.map f l).prod < (List.map g l).prod<GOAL>∃ i ∈ l, f i < g i
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>hl : l ≠ []<VAR>f g : ι → M<VAR>h : (List.map f l).prod ≤ (List.map g l).prod<GOAL>∃ x ∈ l, f x ≤ g x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>hl : l ≠ []<VAR>f g : ι → M<VAR>h : (List.map f l).sum ≤ (List.map g l).sum<GOAL>∃ x ∈ l, f x ≤ g x
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>hl₁ : ∀ x ∈ l, 1 ≤ x<GOAL>1 ≤ l.prod
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>l : List M<VAR>hl₁ : ∀ x ∈ l, 0 ≤ x<GOAL>0 ≤ l.sum
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>AddMonoid M<VAR>AddMonoid N<VAR>LinearOrder N<VAR>f : M → N<VAR>h0 : f 0 ≤ 0<VAR>hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)<VAR>l : List M<GOAL>f l.sum ≤ List.foldr max 0 (List.map f l)
<VAR>M : Type u_3<VAR>OrderedAddCommMonoid M<VAR>l : List M<GOAL>(∀ x ∈ l, 0 < x) → l ≠ [] → 0 < l.sum
<VAR>M : Type u_3<VAR>OrderedCommMonoid M<VAR>l : List M<GOAL>(∀ x ∈ l, 1 < x) → l ≠ [] → 1 < l.prod
<VAR>M : Type u_3<VAR>OrderedAddCommMonoid M<VAR>l : List M<VAR>hl₁ : ∀ x ∈ l, 0 ≤ x<VAR>x : M<GOAL>x ∈ l → x ≤ l.sum
<VAR>M : Type u_3<VAR>OrderedCommMonoid M<VAR>l : List M<VAR>hl₁ : ∀ x ∈ l, 1 ≤ x<VAR>x : M<GOAL>x ∈ l → x ≤ l.prod
<VAR>M : Type u_3<VAR>OrderedCommMonoid M<VAR>l : List M<VAR>hl₁ : ∀ x ∈ l, 1 ≤ x<VAR>hl₂ : l.prod = 1<VAR>x : M<VAR>hx : x ∈ l<GOAL>x = 1
<VAR>M : Type u_3<VAR>OrderedAddCommMonoid M<VAR>l : List M<VAR>hl₁ : ∀ x ∈ l, 0 ≤ x<VAR>hl₂ : l.sum = 0<VAR>x : M<VAR>hx : x ∈ l<GOAL>x = 0
<VAR>M : Type u_3<VAR>CanonicallyOrderedCommMonoid M<VAR>l : List M<GOAL>l.prod = 1 ↔ ∀ x ∈ l, x = 1
<VAR>M : Type u_3<VAR>CanonicallyOrderedAddCommMonoid M<VAR>l : List M<GOAL>l.sum = 0 ↔ ∀ x ∈ l, x = 0
<VAR>M : Type u_3<VAR>CanonicallyOrderedCommMonoid M<VAR>L : List M<GOAL>Monotone fun i => (List.take i L).prod
<VAR>M : Type u_3<VAR>CanonicallyOrderedAddCommMonoid M<VAR>L : List M<GOAL>Monotone fun i => (List.take i L).sum
<VAR>R : Type u_1<VAR>OrderedCommSemiring R<VAR>s : Multiset R<VAR>h : ∀ a ∈ s, 0 ≤ a<GOAL>0 ≤ s.prod
<VAR>R : Type u_1<VAR>CanonicallyOrderedCommSemiring R<VAR>Nontrivial R<VAR>m : Multiset R<GOAL>0 < m.prod ↔ ∀ x ∈ m, 0 < x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : α<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a : WithTop α<GOAL>a * ⊤ = if a = 0 then 0 else ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a : WithTop α<VAR>h : a ≠ 0<GOAL>a * ⊤ = ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>b : WithTop α<GOAL>⊤ * b = if b = 0 then 0 else ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>b : WithTop α<VAR>hb : b ≠ 0<GOAL>⊤ * b = ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<GOAL>⊤ * ⊤ = ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : WithTop α<GOAL>a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (fun x x_1 => x * x_1) a b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : WithTop α<GOAL>a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>b : α<VAR>hb : b ≠ 0<VAR>a : WithTop α<GOAL>a * ↑b = Option.bind a fun a => some (a * b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b : WithTop α<GOAL>↑a * b = Option.bind b fun b => some (a * b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : WithTop α<GOAL>WithTop.untop' 0 (a * b) = WithTop.untop' 0 a * WithTop.untop' 0 b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>LT α<VAR>a b : WithTop α<VAR>ha : a < ⊤<VAR>hb : b < ⊤<GOAL>a * b < ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>LT α<VAR>a b : WithTop α<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a * b < ⊤
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>MulZeroOneClass R<VAR>DecidableEq R<VAR>Nontrivial R<VAR>MulZeroOneClass S<VAR>DecidableEq S<VAR>Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<GOAL>⇑(f.withTopMap hf) = WithTop.map ⇑f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MonoidWithZero α<VAR>NoZeroDivisors α<VAR>Nontrivial α<VAR>a : α<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MonoidWithZero α<VAR>NoZeroDivisors α<VAR>Nontrivial α<VAR>n : ℕ<VAR>n_pos : 0 < n<GOAL>⊤ ^ n = ⊤
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CanonicallyOrderedCommSemiring α<VAR>a b c : WithTop α<GOAL>(a + b) * c = a * c + b * c
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CanonicallyOrderedCommSemiring R<VAR>DecidableEq R<VAR>Nontrivial R<VAR>CanonicallyOrderedCommSemiring S<VAR>DecidableEq S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>⇑(f.withTopMap hf) = (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a : WithBot α<GOAL>a * ⊥ = if a = 0 then 0 else ⊥
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a : WithBot α<VAR>h : a ≠ 0<GOAL>a * ⊥ = ⊥
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>b : WithBot α<GOAL>⊥ * b = if b = 0 then 0 else ⊥
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>b : WithBot α<VAR>hb : b ≠ 0<GOAL>⊥ * b = ⊥
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<GOAL>⊥ * ⊥ = ⊥
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : WithBot α<GOAL>a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (fun x x_1 => x * x_1) a b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : WithBot α<GOAL>a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>b : α<VAR>hb : b ≠ 0<VAR>a : WithBot α<GOAL>a * ↑b = Option.bind a fun a => some (a * b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b : WithBot α<GOAL>↑a * b = Option.bind b fun b => some (a * b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>a b : WithBot α<GOAL>WithBot.unbot' 0 (a * b) = WithBot.unbot' 0 a * WithBot.unbot' 0 b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>LT α<VAR>a b : WithBot α<VAR>ha : ⊥ < a<VAR>hb : ⊥ < b<GOAL>⊥ < a * b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>LT α<VAR>a b : WithBot α<VAR>ha : a ≠ ⊥<VAR>hb : b ≠ ⊥<GOAL>⊥ < a * b
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a c d : α<GOAL>a⁻¹ ∈ Set.Icc c d ↔ a ∈ Set.Icc d⁻¹ c⁻¹
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a c d : α<GOAL>-a ∈ Set.Icc c d ↔ a ∈ Set.Icc (-d) (-c)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a c d : α<GOAL>-a ∈ Set.Ico c d ↔ a ∈ Set.Ioc (-d) (-c)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a c d : α<GOAL>a⁻¹ ∈ Set.Ico c d ↔ a ∈ Set.Ioc d⁻¹ c⁻¹
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a c d : α<GOAL>a⁻¹ ∈ Set.Ioc c d ↔ a ∈ Set.Ico d⁻¹ c⁻¹
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a c d : α<GOAL>-a ∈ Set.Ioc c d ↔ a ∈ Set.Ico (-d) (-c)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a c d : α<GOAL>-a ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (-d) (-c)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a c d : α<GOAL>a⁻¹ ∈ Set.Ioo c d ↔ a ∈ Set.Ioo d⁻¹ c⁻¹
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c - b) (d - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c - b) (d - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c - b) (d - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c - b) (d - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Icc c d ↔ b ∈ Set.Icc (c - a) (d - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Ico c d ↔ b ∈ Set.Ico (c - a) (d - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Ioc c d ↔ b ∈ Set.Ioc (c - a) (d - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a + b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (c - a) (d - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c + b) (d + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Ico c d ↔ a ∈ Set.Ico (c + b) (d + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c + b) (d + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c + b) (d + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Icc c d ↔ b ∈ Set.Icc (a - d) (a - c)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Ico c d ↔ b ∈ Set.Ioc (a - d) (a - c)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Ioc c d ↔ b ∈ Set.Ico (a - d) (a - c)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c d : α<GOAL>a - b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (a - d) (a - c)
<VAR>R : Type u_2<VAR>LinearOrderedAddCommGroup R<VAR>x y z : R<GOAL>|x - y| ≤ z ↔ y ∈ Set.Icc (x - z) (x + z)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>x dx y dy : α<VAR>h : dy < dx<VAR>hx : 0 < dx<GOAL>Nonempty ↑(Set.Ico x (x + dx) \ Set.Ico y (y + dy))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (a * b ^ n) (a * b ^ (n + 1)))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (a + n • b) (a + (n + 1) • b))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ico (a + n • b) (a + (n + 1) • b))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ico (a * b ^ n) (a * b ^ (n + 1)))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (a + n • b) (a + (n + 1) • b))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (a * b ^ n) (a * b ^ (n + 1)))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (b ^ n) (b ^ (n + 1)))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (n • b) ((n + 1) • b))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ico (b ^ n) (b ^ (n + 1)))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ico (n • b) ((n + 1) • b))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (b ^ n) (b ^ (n + 1)))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>b : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (n • b) ((n + 1) • b))
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (a + ↑n) (a + ↑n + 1))
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Set.Ico (a + ↑n) (a + ↑n + 1))
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (a + ↑n) (a + ↑n + 1))
<VAR>α : Type u_1<VAR>OrderedRing α<GOAL>Pairwise (Disjoint on fun n => Set.Ico (↑n) (↑n + 1))
<VAR>α : Type u_1<VAR>OrderedRing α<GOAL>Pairwise (Disjoint on fun n => Set.Ioo (↑n) (↑n + 1))
<VAR>α : Type u_1<VAR>OrderedRing α<GOAL>Pairwise (Disjoint on fun n => Set.Ioc (↑n) (↑n + 1))
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<GOAL>(∀ x ∈ s, 1 ≤ x) → 1 ≤ s.prod
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<GOAL>(∀ x ∈ s, 0 ≤ x) → 0 ≤ s.sum
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<GOAL>(∀ x ∈ s, 0 ≤ x) → ∀ x ∈ s, x ≤ s.sum
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<GOAL>(∀ x ∈ s, 1 ≤ x) → ∀ x ∈ s, x ≤ s.prod
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<VAR>n : α<VAR>h : ∀ x ∈ s, x ≤ n<GOAL>s.prod ≤ n ^ Multiset.card s
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<VAR>n : α<VAR>h : ∀ x ∈ s, x ≤ n<GOAL>s.sum ≤ Multiset.card s • n
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<GOAL>(∀ x ∈ s, 0 ≤ x) → s.sum = 0 → ∀ x ∈ s, x = 0
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<GOAL>(∀ x ∈ s, 1 ≤ x) → s.prod = 1 → ∀ x ∈ s, x = 1
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s t : Multiset α<VAR>h : Multiset.Rel (fun x x_1 => x ≤ x_1) s t<GOAL>s.prod ≤ t.prod
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s t : Multiset α<VAR>h : Multiset.Rel (fun x x_1 => x ≤ x_1) s t<GOAL>s.sum ≤ t.sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>(Multiset.map f s).sum ≤ (Multiset.map g s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>(Multiset.map f s).prod ≤ (Multiset.map g s).prod
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<VAR>f : α → α<VAR>h : ∀ x ∈ s, f x ≤ x<GOAL>(Multiset.map f s).sum ≤ s.sum
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<VAR>f : α → α<VAR>h : ∀ x ∈ s, f x ≤ x<GOAL>(Multiset.map f s).prod ≤ s.prod
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<VAR>f : α → α<VAR>h : ∀ x ∈ s, x ≤ f x<GOAL>s.sum ≤ (Multiset.map f s).sum
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<VAR>f : α → α<VAR>h : ∀ x ∈ s, x ≤ f x<GOAL>s.prod ≤ (Multiset.map f s).prod
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>h : ∀ x ∈ s, a ≤ x<GOAL>Multiset.card s • a ≤ s.sum
<VAR>α : Type u_2<VAR>OrderedCommMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>h : ∀ x ∈ s, a ≤ x<GOAL>a ^ Multiset.card s ≤ s.prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>s : Multiset α<VAR>hps : ∀ a ∈ s, p a<GOAL>f s.prod ≤ (Multiset.map f s).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 0 = 0<VAR>hp_one : p 0<VAR>h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a + b)<VAR>s : Multiset α<VAR>hps : ∀ a ∈ s, p a<GOAL>f s.sum ≤ (Multiset.map f s).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>OrderedCommMonoid β<VAR>f : α → β<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b<VAR>s : Multiset α<GOAL>f s.prod ≤ (Multiset.map f s).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>f : α → β<VAR>h_one : f 0 = 0<VAR>h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b<VAR>s : Multiset α<GOAL>f s.sum ≤ (Multiset.map f s).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>s : Multiset α<VAR>hs_nonempty : s ≠ ∅<VAR>hs : ∀ a ∈ s, p a<GOAL>f s.prod ≤ (Multiset.map f s).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a + b)<VAR>s : Multiset α<VAR>hs_nonempty : s ≠ ∅<VAR>hs : ∀ a ∈ s, p a<GOAL>f s.sum ≤ (Multiset.map f s).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>OrderedCommMonoid β<VAR>f : α → β<VAR>h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b<VAR>s : Multiset α<VAR>hs_nonempty : s ≠ ∅<GOAL>f s.prod ≤ (Multiset.map f s).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>f : α → β<VAR>h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b<VAR>s : Multiset α<VAR>hs_nonempty : s ≠ ∅<GOAL>f s.sum ≤ (Multiset.map f s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>hle : ∀ i ∈ s, f i ≤ g i<VAR>hlt : ∃ i ∈ s, f i < g i<GOAL>(Multiset.map f s).sum < (Multiset.map g s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedCancelCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>hle : ∀ i ∈ s, f i ≤ g i<VAR>hlt : ∃ i ∈ s, f i < g i<GOAL>(Multiset.map f s).prod < (Multiset.map g s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>hs : s ≠ ∅<VAR>hfg : ∀ i ∈ s, f i < g i<GOAL>(Multiset.map f s).sum < (Multiset.map g s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>OrderedCancelCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>hs : s ≠ ∅<VAR>hfg : ∀ i ∈ s, f i < g i<GOAL>(Multiset.map f s).prod < (Multiset.map g s).prod
<VAR>α : Type u_2<VAR>CanonicallyOrderedCommMonoid α<VAR>m : Multiset α<GOAL>m.prod = 1 ↔ ∀ x ∈ m, x = 1
<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>m : Multiset α<GOAL>m.sum = 0 ↔ ∀ x ∈ m, x = 0
<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>m : Multiset α<VAR>a : α<VAR>ha : a ∈ m<GOAL>a ≤ m.sum
<VAR>α : Type u_2<VAR>CanonicallyOrderedCommMonoid α<VAR>m : Multiset α<VAR>a : α<VAR>ha : a ∈ m<GOAL>a ≤ m.prod
<VAR>α : Type u_4<VAR>LinearOrder α<VAR>OrderBot α<VAR>l : Multiset α<VAR>n : α<VAR>h : ∀ x ∈ l, x ≤ n<GOAL>Multiset.fold max ⊥ l ≤ n
<VAR>α : Type u_2<VAR>LinearOrderedAddCommGroup α<VAR>s : Multiset α<GOAL>|s.sum| ≤ (Multiset.map abs s).sum
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>W X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Z ⊗ Y ⟶ W<VAR>wh : Z ◁ f ≫ h = Z ◁ g ≫ h<GOAL>Z ◁ CategoryTheory.Limits.coequalizer.π f g ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv ≫ CategoryTheory.Limits.coequalizer.desc h wh = h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>X Y Z X' Y' Z' : C<VAR>f g : X ⟶ Y<VAR>f' g' : X' ⟶ Y'<VAR>p : Z ⊗ X ⟶ X'<VAR>q : Z ⊗ Y ⟶ Y'<VAR>wf : Z ◁ f ≫ q = p ≫ f'<VAR>wg : Z ◁ g ≫ q = p ≫ g'<VAR>h : Y' ⟶ Z'<VAR>wh : f' ≫ h = g' ≫ h<GOAL>Z ◁ CategoryTheory.Limits.coequalizer.π f g ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv ≫ CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (Z ◁ f) (Z ◁ g) f' g' p q wf wg) ≫ CategoryTheory.Limits.coequalizer.desc h wh = q ≫ h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>W X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⊗ Z ⟶ W<VAR>wh : f ▷ Z ≫ h = g ▷ Z ≫ h<GOAL>CategoryTheory.Limits.coequalizer.π f g ▷ Z ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv ≫ CategoryTheory.Limits.coequalizer.desc h wh = h