ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>p : α<VAR>hp : 0 < p<GOAL>⋃ n, Set.Icc (n • p) ((n + 1) • p) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<VAR>a : α<GOAL>⋃ n, Set.Ioc (a + ↑n) (a + ↑n + 1) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<VAR>a : α<GOAL>⋃ n, Set.Ico (a + ↑n) (a + ↑n + 1) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<VAR>a : α<GOAL>⋃ n, Set.Icc (a + ↑n) (a + ↑n + 1) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<GOAL>⋃ n, Set.Ioc (↑n) (↑n + 1) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<GOAL>⋃ n, Set.Ico (↑n) (↑n + 1) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Archimedean α<GOAL>⋃ n, Set.Icc (↑n) (↑n + 1) = Set.univ
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a b c : R<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>c * a ≤ c * b
<VAR>α : Type u<VAR>self : OrderedSemiring α<GOAL>0 ≤ 1
<VAR>α : Type u<VAR>self : OrderedSemiring α<VAR>a b c : α<GOAL>a ≤ b → 0 ≤ c → c * a ≤ c * b
<VAR>α : Type u<VAR>self : OrderedSemiring α<VAR>a b c : α<GOAL>a ≤ b → 0 ≤ c → a * c ≤ b * c
<VAR>α : Type u<VAR>self : OrderedRing α<GOAL>0 ≤ 1
<VAR>α : Type u<VAR>self : OrderedRing α<VAR>a b : α<GOAL>0 ≤ a → 0 ≤ b → 0 ≤ a * b
<VAR>α : Type u<VAR>self : StrictOrderedSemiring α<GOAL>0 ≤ 1
<VAR>α : Type u<VAR>self : StrictOrderedSemiring α<VAR>a b c : α<GOAL>a < b → 0 < c → a * c < b * c
<VAR>α : Type u<VAR>self : StrictOrderedSemiring α<VAR>a b c : α<GOAL>a < b → 0 < c → c * a < c * b
<VAR>α : Type u<VAR>self : StrictOrderedRing α<VAR>a b : α<GOAL>0 < a → 0 < b → 0 < a * b
<VAR>α : Type u<VAR>self : StrictOrderedRing α<GOAL>0 ≤ 1
<VAR>α : Type u_2<VAR>self : CanonicallyOrderedCommSemiring α<VAR>a b : α<GOAL>a * b = 0 → a = 0 ∨ b = 0
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>a : α<VAR>Nontrivial α<GOAL>Odd a → 0 < a
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>a b : α<GOAL>0 < a * b ↔ 0 < a ∧ 0 < b
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>a : α<VAR>ha : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ n
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>a b c d : α<VAR>PosMulStrictMono α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>a b c : α<VAR>Sub α<VAR>OrderedSub α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>h : AddLECancellable (a * c)<GOAL>a * (b - c) = a * b - a * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>a b c : α<VAR>Sub α<VAR>OrderedSub α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>h : AddLECancellable (b * c)<GOAL>(a - b) * c = a * c - b * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a * (b - c) = a * b - a * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (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 * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a * (b - 1) = a * b - a
<VAR>α : Type u<VAR>CanonicallyOrderedCommSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a - 1) * b = a * b - b
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addLeftEmbedding c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addRightEmbedding c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addLeftEmbedding c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addRightEmbedding c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addLeftEmbedding c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addRightEmbedding c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addLeftEmbedding c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.map (addRightEmbedding c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => c + x) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => c + x) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => c + x) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => c + x) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => x + c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => x + c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => x + c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
<VAR>α : Type u_2<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.image (fun x => x + c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 0 < a<VAR>x : α<GOAL>(OrderIso.mulLeft₀ a ha) x = a * x
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 0 < a<VAR>x : α<GOAL>(RelIso.symm (OrderIso.mulLeft₀ a ha)) x = a⁻¹ * x
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 0 < a<VAR>x : α<GOAL>(RelIso.symm (OrderIso.mulRight₀ a ha)) x = x * a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 0 < a<VAR>x : α<GOAL>(OrderIso.mulRight₀ a ha) x = x * a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>a ≤ b / c ↔ a * c ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>a ≤ b / c ↔ c * a ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hb : 0 < b<GOAL>a / b ≤ c ↔ a ≤ c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hb : 0 < b<GOAL>a / b ≤ c ↔ a ≤ b * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hb : 0 < b<VAR>hc : 0 < c<GOAL>a / b ≤ c ↔ a / c ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>a < b / c ↔ a * c < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>a < b / c ↔ c * a < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>b / c < a ↔ b < a * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>b / c < a ↔ b < c * a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hb : 0 < b<VAR>hc : 0 < c<GOAL>a / b < c ↔ a / c < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>b⁻¹ * a ≤ c ↔ a ≤ b * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>b⁻¹ * a ≤ c ↔ a ≤ c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>a * b⁻¹ ≤ c ↔ a ≤ b * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>a * b⁻¹ ≤ c ↔ a ≤ c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>a / a ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>b⁻¹ * a < c ↔ a < b * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>b⁻¹ * a < c ↔ a < c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>a * b⁻¹ < c ↔ a < b * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : 0 < b<GOAL>a * b⁻¹ < c ↔ a < c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<GOAL>a⁻¹ ≤ b ↔ 1 ≤ b * a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<GOAL>a⁻¹ ≤ b ↔ 1 ≤ a * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<GOAL>a⁻¹ < b ↔ 1 < b * a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<GOAL>a⁻¹ < b ↔ 1 < a * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hb : 0 ≤ b<VAR>hc : 0 ≤ c<VAR>h : a ≤ c * b<GOAL>a / b ≤ c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hb : 0 ≤ b<VAR>hc : 0 ≤ c<VAR>h : a ≤ b / c<GOAL>a * c ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>h : a ≤ b<VAR>hb : 0 ≤ b<GOAL>a / b ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>h : a ≤ b<VAR>hb : 0 ≤ b<GOAL>a * b⁻¹ ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>h : a ≤ b<VAR>hb : 0 ≤ b<GOAL>b⁻¹ * a ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : a ≤ b<GOAL>b⁻¹ ≤ a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a⁻¹ ≤ b ↔ b⁻¹ ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : a⁻¹ ≤ b<GOAL>b⁻¹ ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a ≤ b⁻¹ ↔ b ≤ a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a⁻¹ < b⁻¹ ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>hb : 0 < b<VAR>h : b < a<GOAL>a⁻¹ < b⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a⁻¹ < b ↔ b⁻¹ < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : a⁻¹ < b<GOAL>b⁻¹ < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a < b⁻¹ ↔ b < a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 1 < a<GOAL>a⁻¹ < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h₁ : 0 < a<VAR>h₂ : a < 1<GOAL>1 < a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 1 ≤ a<GOAL>a⁻¹ ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h₁ : 0 < a<VAR>h₂ : a ≤ 1<GOAL>1 ≤ a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h₀ : 0 < a<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>1 < a⁻¹ ↔ 0 < a ∧ a < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>a / c ≤ b / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>h : a < b<VAR>hc : 0 < c<GOAL>a / c < b / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>ha : 0 ≤ a<VAR>hc : 0 < c<VAR>h : c ≤ b<GOAL>a / b ≤ a / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>ha : 0 < a<VAR>hc : 0 < c<VAR>h : c < b<GOAL>a / b < a / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 ≤ c<VAR>hab : a ≤ b<GOAL>a / c ≤ b / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>a / c ≤ b / c ↔ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>hc : 0 < c<GOAL>a / c < b / c ↔ a < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hc : 0 < c<GOAL>a / b < a / c ↔ c < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c : α<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hc : 0 < c<GOAL>a / b ≤ a / c ↔ c ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d : α<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>a / b < c / d ↔ a * d < c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d : α<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>a / b ≤ c / d ↔ a * d ≤ c * b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d : α<VAR>hc : 0 ≤ c<VAR>hac : a ≤ c<VAR>hd : 0 < d<VAR>hbd : d ≤ b<GOAL>a / b ≤ c / d
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d : α<VAR>hac : a < c<VAR>hbd : d ≤ b<VAR>c0 : 0 ≤ c<VAR>d0 : 0 < d<GOAL>a / b < c / d
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d : α<VAR>hac : a ≤ c<VAR>hbd : d < b<VAR>c0 : 0 < c<VAR>d0 : 0 < d<GOAL>a / b < c / d
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 1 ≤ b<GOAL>a / b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 1 < b<GOAL>a / b < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb₀ : 0 < b<VAR>hb₁ : b ≤ 1<GOAL>a ≤ a / b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>hb : 0 < b<GOAL>1 ≤ a / b ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>hb : 0 < b<GOAL>a / b ≤ 1 ↔ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>hb : 0 < b<GOAL>1 < a / b ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>hb : 0 < b<GOAL>a / b < 1 ↔ a < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>1 / a ≤ b ↔ 1 / b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>1 / a < b ↔ 1 / b < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a ≤ 1 / b ↔ b ≤ 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a < 1 / b ↔ b < 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : a ≤ b<GOAL>1 / b ≤ 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : a < b<GOAL>1 / b < 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : 1 / a ≤ 1 / b<GOAL>b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>h : 1 / a < 1 / b<GOAL>b < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>1 / a ≤ 1 / b ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>1 / a < 1 / b ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h1 : 0 < a<VAR>h2 : a < 1<GOAL>1 < 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h1 : 0 < a<VAR>h2 : a ≤ 1<GOAL>1 ≤ 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h : 0 < a<GOAL>0 < a / 2
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<GOAL>0 < 1 / 2
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>a / 2 ≤ a ↔ 0 ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>a / 2 < a ↔ 0 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<GOAL>1 / 2 < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<GOAL>2⁻¹ < 1
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<GOAL>a < (a + b) / 2 ↔ a < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<GOAL>(a + b) / 2 < b ↔ a < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>a / 3 + a / 3 + a / 3 = a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<GOAL>0 < a / b ↔ 0 < b
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>hb : 0 < b<GOAL>0 < a / b ↔ 0 < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d : α<VAR>h : a * (b / c) ≤ d<VAR>hc : 0 < c<GOAL>b * a ≤ d * c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b c d e : α<VAR>h : a / b ≤ c / d<VAR>he : 0 ≤ e<GOAL>a / (b * e) ≤ c / (d * e)
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h : 0 < a<VAR>b : α<GOAL>∃ c, 0 < c ∧ b * c < a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h : 0 < a<VAR>b : α<GOAL>∃ c, 0 < c ∧ b < c * a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>Monotone fun x => x / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 0 < a<GOAL>StrictMono fun x => x / a
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>β : Type u_4<VAR>Preorder β<VAR>f : β → α<VAR>hf : Monotone f<VAR>c : α<VAR>hc : 0 ≤ c<GOAL>Monotone fun x => f x / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>β : Type u_4<VAR>Preorder β<VAR>f : β → α<VAR>hf : StrictMono f<VAR>c : α<VAR>hc : 0 < c<GOAL>StrictMono fun x => f x / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>c : α<VAR>hc : 0 ≤ c<VAR>a b : α<GOAL>min (a / c) (b / c) = min a b / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>c : α<VAR>hc : 0 ≤ c<VAR>a b : α<GOAL>max (a / c) (b / c) = max a b / c
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<GOAL>StrictAntiOn (fun x => 1 / x) (Set.Ioi 0)
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 ≤ a<VAR>m n : ℕ<VAR>mn : m ≤ n<GOAL>1 / a ^ n ≤ 1 / a ^ m
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>mn : m < n<GOAL>1 / a ^ n < 1 / a ^ m
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 ≤ a<GOAL>Antitone fun n => 1 / a ^ n
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 < a<GOAL>StrictAnti fun n => 1 / a ^ n
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<GOAL>StrictAntiOn (fun x => x⁻¹) (Set.Ioi 0)
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 ≤ a<VAR>m n : ℕ<VAR>mn : m ≤ n<GOAL>(a ^ n)⁻¹ ≤ (a ^ m)⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>mn : m < n<GOAL>(a ^ n)⁻¹ < (a ^ m)⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 ≤ a<GOAL>Antitone fun n => (a ^ n)⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>a1 : 1 < a<GOAL>StrictAnti fun n => (a ^ n)⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsGLB s b<GOAL>IsGLB ((fun b => a * b) '' s) (a * b)
<VAR>α : Type u_2<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsGLB s b<GOAL>IsGLB ((fun b => b * a) '' s) (b * a)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>0 ≤ a / b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>0 < a / b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>a / b < 0
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : b < 0<GOAL>a / b < 0
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>b / c ≤ a ↔ a * c ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>b / c ≤ a ↔ c * a ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>a ≤ b / c ↔ b ≤ a * c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>a ≤ b / c ↔ b ≤ c * a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>b / c < a ↔ a * c < b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>b / c < a ↔ c * a < b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>a < b / c ↔ b < a * c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>a < b / c ↔ b < c * a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>h : b ≤ a<VAR>hb : b ≤ 0<GOAL>a / b ≤ 1
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a⁻¹ ≤ b ↔ b⁻¹ ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a ≤ b⁻¹ ↔ b ≤ a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a⁻¹ < b⁻¹ ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a⁻¹ < b ↔ b⁻¹ < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a < b⁻¹ ↔ b < a⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>c : α<GOAL>AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>c : α<GOAL>AntitoneOn (fun x => (x - c)⁻¹) (Set.Iio c)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>ha : c < a<GOAL>AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>ha : b < c<GOAL>AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
<VAR>α : Type u_2<VAR>LinearOrderedField α<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
<VAR>α : Type u_2<VAR>LinearOrderedField α<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Iio 0)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : 0 < a<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c ≤ 0<VAR>h : b ≤ a<GOAL>a / c ≤ b / c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<VAR>h : b < a<GOAL>a / c < b / c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>a / c ≤ b / c ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hc : c < 0<GOAL>a / c < b / c ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<GOAL>1 ≤ a / b ↔ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<GOAL>a / b ≤ 1 ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<GOAL>1 < a / b ↔ a < b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<GOAL>a / b < 1 ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a ≤ b ↔ 1 / b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a < b ↔ 1 / b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a ≤ 1 / b ↔ b ≤ 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a < 1 / b ↔ b < 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a