ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : a < 0<VAR>hb : b < c<GOAL>a + b < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : a < 1<VAR>hb : b < c<GOAL>a * b < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a < 0<VAR>hbc : b < c<GOAL>a + b < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a < 1<VAR>hbc : b < c<GOAL>a * b < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<GOAL>a * b ≤ 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>a + b ≤ 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 1<VAR>hb : b ≤ 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b ≤ 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 1<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a < 1<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 1 ≤ a<VAR>hbc : b ≤ c<GOAL>b ≤ a * c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 0 ≤ a<VAR>hbc : b ≤ c<GOAL>b ≤ a + c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : 0 < a<VAR>hbc : b ≤ c<GOAL>b < a + c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : 1 < a<VAR>hbc : b ≤ c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 1 ≤ a<VAR>hbc : b < c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 0 ≤ a<VAR>hbc : b < c<GOAL>b < a + c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : 1 < a<VAR>hbc : b < c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : 0 < a<VAR>hbc : b < c<GOAL>b < a + c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 0 < a<VAR>hbc : b < c<GOAL>b < a + c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : 1 < a<VAR>hbc : b < c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>1 ≤ a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 1 < a<VAR>hb : 1 ≤ b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 1 < a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 < a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a + b < c<VAR>hle : 0 ≤ b<GOAL>a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a * b < c<VAR>hle : 1 ≤ b<GOAL>a < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a + b ≤ c<VAR>hle : 0 ≤ b<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a * b ≤ c<VAR>hle : 1 ≤ b<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a < b + c<VAR>hle : c ≤ 0<GOAL>a < b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a < b * c<VAR>hle : c ≤ 1<GOAL>a < b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a ≤ b * c<VAR>hle : c ≤ 1<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a ≤ b + c<VAR>hle : c ≤ 0<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a * b < c<VAR>hle : 1 ≤ a<GOAL>b < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a + b < c<VAR>hle : 0 ≤ a<GOAL>b < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a * b ≤ c<VAR>hle : 1 ≤ a<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a + b ≤ c<VAR>hle : 0 ≤ a<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a < b + c<VAR>hle : b ≤ 0<GOAL>a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a < b * c<VAR>hle : b ≤ 1<GOAL>a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a ≤ b * c<VAR>hle : b ≤ 1<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a ≤ b + c<VAR>hle : b ≤ 0<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>PartialOrder α<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 : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a + b = 0 ↔ a = 0 ∧ b = 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>PartialOrder α<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 : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>a * b = 1 ↔ a = 1 ∧ b = 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>hab : 0 ≤ a + b<GOAL>a = 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<VAR>hab : 1 ≤ a * b<GOAL>a = 1
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<VAR>hab : a * b ≤ 1<GOAL>a = 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b ≤ 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>PartialOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<VAR>hab : 1 ≤ a * b<GOAL>b = 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>PartialOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>hab : 0 ≤ a + b<GOAL>b = 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>PartialOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<VAR>hab : a * b ≤ 1<GOAL>b = 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>PartialOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b ≤ 0<GOAL>b = 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>∃ b, b * b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>a : α<GOAL>Monotone fun x => a * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>a : α<GOAL>Monotone fun x => a + f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MonotoneOn f s<VAR>a : α<GOAL>MonotoneOn (fun x => a + f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : MonotoneOn f s<VAR>a : α<GOAL>MonotoneOn (fun x => a * f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>a : α<GOAL>Antitone fun x => a * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>a : α<GOAL>Antitone fun x => a + f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : AntitoneOn f s<VAR>a : α<GOAL>AntitoneOn (fun x => a + f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : AntitoneOn f s<VAR>a : α<GOAL>AntitoneOn (fun x => a * f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>a : α<GOAL>Monotone fun x => f x * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>a : α<GOAL>Monotone fun x => f x + a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MonotoneOn f s<VAR>a : α<GOAL>MonotoneOn (fun x => f x + a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : MonotoneOn f s<VAR>a : α<GOAL>MonotoneOn (fun x => f x * a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>a : α<GOAL>Antitone fun x => f x * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>a : α<GOAL>Antitone fun x => f x + a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : AntitoneOn f s<VAR>a : α<GOAL>AntitoneOn (fun x => f x + a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hf : AntitoneOn f s<VAR>a : α<GOAL>AntitoneOn (fun x => f x * a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : MonotoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : AntitoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictMono f<VAR>c : α<GOAL>StrictMono fun x => c + f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictMono f<VAR>c : α<GOAL>StrictMono fun x => c * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictMonoOn f s<VAR>c : α<GOAL>StrictMonoOn (fun x => c + f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictMonoOn f s<VAR>c : α<GOAL>StrictMonoOn (fun x => c * f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictAnti f<VAR>c : α<GOAL>StrictAnti fun x => c + f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictAnti f<VAR>c : α<GOAL>StrictAnti fun x => c * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictAntiOn f s<VAR>c : α<GOAL>StrictAntiOn (fun x => c + f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictAntiOn f s<VAR>c : α<GOAL>StrictAntiOn (fun x => c * f x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictMono f<VAR>c : α<GOAL>StrictMono fun x => f x + c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictMono f<VAR>c : α<GOAL>StrictMono fun x => f x * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictMonoOn f s<VAR>c : α<GOAL>StrictMonoOn (fun x => f x + c) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictMonoOn f s<VAR>c : α<GOAL>StrictMonoOn (fun x => f x * c) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictAnti f<VAR>c : α<GOAL>StrictAnti fun x => f x * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictAnti f<VAR>c : α<GOAL>StrictAnti fun x => f x + c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>hf : StrictAntiOn f s<VAR>c : α<GOAL>StrictAntiOn (fun x => f x * c) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hf : StrictAntiOn f s<VAR>c : α<GOAL>StrictAntiOn (fun x => f x + c) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictMono f<VAR>hg : StrictMono g<GOAL>StrictMono fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictMono f<VAR>hg : StrictMono g<GOAL>StrictMono fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictMonoOn f s<VAR>hg : StrictMonoOn g s<GOAL>StrictMonoOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictMonoOn f s<VAR>hg : StrictMonoOn g s<GOAL>StrictMonoOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictAnti f<VAR>hg : StrictAnti g<GOAL>StrictAnti fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictAnti f<VAR>hg : StrictAnti g<GOAL>StrictAnti fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictAntiOn f s<VAR>hg : StrictAntiOn g s<GOAL>StrictAntiOn (fun x => f x * g x) s