ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : 0 < a<GOAL>-a < a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : a < 1<GOAL>a < a⁻¹
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : a < 0<GOAL>a < -a
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>c⁻¹ * a ≤ b ↔ a ≤ b * c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>-c + a ≤ b ↔ a ≤ b + c
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a * b⁻¹ ≤ c ↔ a ≤ b * c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a + -b ≤ c ↔ a ≤ b + c
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a + -b ≤ c + -d ↔ a + d ≤ c + b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>c⁻¹ * a < b ↔ a < b * c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>-c + a < b ↔ a < b + c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a + -b < c ↔ a < b + c
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a * b⁻¹ < c ↔ a < b * c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a + -b < c + -d ↔ a + d < c + b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>c : α<GOAL>a - c ≤ b - c ↔ a ≤ b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>c : α<GOAL>a / c ≤ b / c ↔ a ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a ≤ b<VAR>c : α<GOAL>a - c ≤ b - c
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a ≤ b<VAR>c : α<GOAL>a / c ≤ b / c
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>0 ≤ a - b ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>1 ≤ a / b ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a / b ≤ 1 ↔ a ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a - b ≤ 0 ↔ a ≤ b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ≤ c / b ↔ a * b ≤ c
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ≤ c - b ↔ a + b ≤ c
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a / c ≤ b ↔ a ≤ b * c
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a - c ≤ b ↔ a ≤ b + c
<VAR>α : Type u<VAR>Group α<VAR>LE α<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>b c : α<VAR>a : α<GOAL>a / b ≤ a / c ↔ c ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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>b c : α<VAR>a : α<GOAL>a - b ≤ a - c ↔ c ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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>h : a ≤ b<VAR>c : α<GOAL>c - b ≤ c - a
<VAR>α : Type u<VAR>Group α<VAR>LE α<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>h : a ≤ b<VAR>c : α<GOAL>c / b ≤ c / a
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a - b ≤ c - d ↔ a + d ≤ c + b
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / b ≤ c / d ↔ a * d ≤ c * b
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b ≤ c / a ↔ a * b ≤ c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b ≤ c - a ↔ a + b ≤ c
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a / b ≤ c ↔ a ≤ b * c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a - b ≤ c ↔ a ≤ b + c
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b⁻¹ ≤ a / c ↔ c ≤ a * b
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>-b ≤ a - c ↔ c ≤ a + b
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a⁻¹ ≤ b / c ↔ c ≤ a * b
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>-a ≤ b - c ↔ c ≤ a + b
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a - b ≤ c ↔ a - c ≤ b
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a / b ≤ c ↔ a / c ≤ b
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ≤ b - c ↔ c ≤ b - a
<VAR>α : Type u<VAR>CommGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ≤ b / c ↔ c ≤ b / a
<VAR>α : Type u<VAR>CommGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a / d ≤ b / c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a - d ≤ b - c
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>c : α<GOAL>a - c < b - c ↔ a < b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>c : α<GOAL>a / c < b / c ↔ a < b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < b<VAR>c : α<GOAL>a / c < b / c
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < b<VAR>c : α<GOAL>a - c < b - c
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>1 < a / b ↔ b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>0 < a - b ↔ b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a - b < 0 ↔ a < b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a / b < 1 ↔ a < b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a < c - b ↔ a + b < c
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a < c / b ↔ a * b < c
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a / c < b ↔ a < b * c
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a - c < b ↔ a < b + c
<VAR>α : Type u<VAR>Group α<VAR>LT α<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>b c : α<VAR>a : α<GOAL>a / b < a / c ↔ c < b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<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>b c : α<VAR>a : α<GOAL>a - b < a - c ↔ c < b
<VAR>α : Type u<VAR>Group α<VAR>LT α<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 c : α<GOAL>a⁻¹ < b / c ↔ c < a * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<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 c : α<GOAL>-a < b - c ↔ c < a + b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<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>h : a < b<VAR>c : α<GOAL>c - b < c - a
<VAR>α : Type u<VAR>Group α<VAR>LT α<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>h : a < b<VAR>c : α<GOAL>c / b < c / a
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a - b < c - d ↔ a + d < c + b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a / b < c / d ↔ a * d < c * b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b < c / a ↔ a * b < c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b < c - a ↔ a + b < c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a - b < c ↔ a < b + c
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a / b < c ↔ a < b * c
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>-b < a - c ↔ c < a + b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b⁻¹ < a / c ↔ c < a * b
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a - b < c ↔ a - c < b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a / b < c ↔ a / c < b
<VAR>α : Type u<VAR>CommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a < b / c ↔ c < b / a
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a < b - c ↔ c < b - a
<VAR>α : Type u<VAR>AddCommGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a - d < b - c
<VAR>α : Type u<VAR>CommGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a / d < b / c
<VAR>α : Type u<VAR>CommGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / d < b / c → a < b ∨ c < d
<VAR>α : Type u<VAR>AddCommGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a - d < b - c → a < b ∨ c < d
<VAR>α : Type u<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>cmp (a - b) 0 = cmp a b
<VAR>α : Type u<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>cmp (a / b) 1 = cmp a b
<VAR>α : Type u<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 0 < ε → a < b + ε<GOAL>a ≤ b
<VAR>α : Type u<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 1 < ε → a < b * ε<GOAL>a ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
<VAR>α : Type u<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
<VAR>α : Type u<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a - b ≤ -a + b ↔ a ≤ b
<VAR>α : Type u<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a / b ≤ a⁻¹ * b ↔ a ≤ b
<VAR>α : Type u_1<VAR>CommGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a / b ≤ b / a ↔ a ≤ b
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a - b ≤ b - a ↔ a ≤ b
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>hf : Monotone f<GOAL>Antitone fun x => (f x)⁻¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>hf : Monotone f<GOAL>Antitone fun x => -f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>hf : Antitone f<GOAL>Monotone fun x => (f x)⁻¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>hf : Antitone f<GOAL>Monotone fun x => -f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : MonotoneOn f s<GOAL>AntitoneOn (fun x => -f x) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : MonotoneOn f s<GOAL>AntitoneOn (fun x => (f x)⁻¹) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : AntitoneOn f s<GOAL>MonotoneOn (fun x => (f x)⁻¹) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : AntitoneOn f s<GOAL>MonotoneOn (fun x => -f x) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>hf : StrictMono f<GOAL>StrictAnti fun x => (f x)⁻¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>hf : StrictMono f<GOAL>StrictAnti fun x => -f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>hf : StrictAnti f<GOAL>StrictMono fun x => -f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>hf : StrictAnti f<GOAL>StrictMono fun x => (f x)⁻¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : StrictMonoOn f s<GOAL>StrictAntiOn (fun x => -f x) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : StrictMonoOn f s<GOAL>StrictAntiOn (fun x => (f x)⁻¹) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>Group α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : StrictAntiOn f s<GOAL>StrictMonoOn (fun x => (f x)⁻¹) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddGroup α<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>Preorder β<VAR>f : β → α<VAR>s : Set β<VAR>hf : StrictAntiOn f s<GOAL>StrictMonoOn (fun x => -f x) s
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>⊥ = ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>Preorder α<VAR>x : α<VAR>hx : 0 ≤ x<GOAL>⟨x, hx⟩ = 0 ↔ x = 0
<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>x y : α<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
<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 : { x // 0 ≤ x }<GOAL>↑(a + b) = ↑a + ↑b
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ℕ<VAR>x : α<VAR>hx : 0 ≤ x<GOAL>n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ℕ<VAR>a : { x // 0 ≤ x }<GOAL>↑(n • a) = n • ↑a
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>LE α<VAR>ZeroLEOneClass α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>LE α<VAR>ZeroLEOneClass α<VAR>x : α<VAR>hx : 0 ≤ x<GOAL>⟨x, hx⟩ = 1 ↔ x = 1
<VAR>α : Type u_1<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulMono α<VAR>a b : { x // 0 ≤ x }<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u_1<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulMono α<VAR>x y : α<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ℕ<VAR>r : { x // 0 ≤ x }<GOAL>↑(n • r) = n • ↑r
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>n : ℕ<GOAL>⟨↑n, ⋯⟩ = ↑n
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>a : α<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ n
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>a : { x // 0 ≤ x }<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>x : α<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<GOAL>↑(Nonneg.toNonneg a) = max a 0
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<VAR>h : 0 ≤ a<GOAL>Nonneg.toNonneg a = ⟨a, h⟩
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : { x // 0 ≤ x }<GOAL>Nonneg.toNonneg ↑a = a
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : α<VAR>b : { x // 0 ≤ x }<GOAL>Nonneg.toNonneg a ≤ b ↔ a ≤ ↑b
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>a : { x // 0 ≤ x }<VAR>b : α<GOAL>a < Nonneg.toNonneg b ↔ ↑a < b
<VAR>α : Type u_1<VAR>Zero α<VAR>LinearOrder α<VAR>Sub α<VAR>x y : α<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>⟨x, hx⟩ - ⟨y, hy⟩ = Nonneg.toNonneg (x - y)
<VAR>R : Type u_1<VAR>OrderedSemiring R<VAR>a : R<VAR>Hsq : 0 ≤ a * a<VAR>Hsq' : 0 ≤ (1 + a) * (1 + a)<VAR>H : 0 ≤ 2 + a<VAR>n : ℕ<GOAL>1 + ↑n * a ≤ (1 + a) ^ n
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a : R<VAR>H : -2 ≤ a<VAR>n : ℕ<GOAL>1 + ↑n * a ≤ (1 + a) ^ n
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a : R<VAR>H : -1 ≤ a<VAR>n : ℕ<GOAL>1 + ↑n * (a - 1) ≤ a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - toIcoDiv hp a b • p ∈ Set.Ico a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>n : ℤ<VAR>h : b - n • p ∈ Set.Ico a (a + p)<GOAL>toIcoDiv hp a b = n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - toIocDiv hp a b • p ∈ Set.Ioc a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>n : ℤ<VAR>h : b - n • p ∈ Set.Ioc a (a + p)<GOAL>toIocDiv hp a b = n