ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<VAR>h : a ≤ b<GOAL>1 / b ≤ 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<VAR>h : a < b<GOAL>1 / b < 1 / a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<VAR>h : 1 / a ≤ 1 / b<GOAL>b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>hb : b < 0<VAR>h : 1 / a < 1 / b<GOAL>b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a ≤ 1 / b ↔ b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a < 1 / b ↔ b < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<VAR>h1 : a < 0<VAR>h2 : -1 < a<GOAL>1 / a < -1
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<VAR>h1 : a < 0<VAR>h2 : -1 ≤ a<GOAL>1 / a ≤ -1
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<GOAL>a - a / 2 = a / 2
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<GOAL>a / 2 - a = -(a / 2)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>h : a < b<GOAL>a + (b - a) / 2 < b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<VAR>a2 : 2 ≤ a<GOAL>(1 - 1 / a)⁻¹ ≤ 2
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsLUB s b<GOAL>IsLUB ((fun b => a * b) '' s) (a * b)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsLUB s b<GOAL>IsLUB ((fun b => b * a) '' s) (b * a)
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c d : α<VAR>hc : c ≠ 0<VAR>hd : d ≠ 0<GOAL>(a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b c d : α<VAR>hc : c ≠ 0<VAR>hd : d ≠ 0<GOAL>(a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>h : b < a<GOAL>∃ c, b + c < a ∧ 0 < c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>h : ∀ ε > 0, b - ε ≤ a<GOAL>b ≤ a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<VAR>a0 : 0 ≤ a<VAR>b0 : 0 ≤ b<GOAL>a * a = b * b ↔ a = b
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>c : α<VAR>hc : c ≤ 0<VAR>a b : α<GOAL>min (a / c) (b / c) = max a b / c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>c : α<VAR>hc : c ≤ 0<VAR>a b : α<GOAL>max (a / c) (b / c) = min a b / c
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<GOAL>|a⁻¹| = |a|⁻¹
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a b : α<GOAL>|a / b| = |a| / |b|
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<GOAL>|1 / a| = 1 / |a|
<VAR>α : Type u_4<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a / b
<VAR>α : Type u_4<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 ≤ a / b
<VAR>α : Type u_4<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : b ≠ 0<GOAL>a / b ≠ 0
<VAR>α : Type u_4<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : 0 < b<GOAL>a / b ≠ 0
<VAR>α : Type u_4<VAR>LinearOrderedSemifield α<VAR>a : α<GOAL>0 < a ^ 0
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a d : M<GOAL>Set.BijOn (fun x => x + d) (Set.Ici a) (Set.Ici (a + d))
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a d : M<GOAL>Set.BijOn (fun x => x + d) (Set.Ioi a) (Set.Ioi (a + d))
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b d : M<GOAL>Set.BijOn (fun x => x + d) (Set.Icc a b) (Set.Icc (a + d) (b + d))
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b d : M<GOAL>Set.BijOn (fun x => x + d) (Set.Ioo a b) (Set.Ioo (a + d) (b + d))
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b d : M<GOAL>Set.BijOn (fun x => x + d) (Set.Ioc a b) (Set.Ioc (a + d) (b + d))
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b d : M<GOAL>Set.BijOn (fun x => x + d) (Set.Ico a b) (Set.Ico (a + d) (b + d))
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b : M<GOAL>(fun x => x + a) '' Set.Ici b = Set.Ici (b + a)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b : M<GOAL>(fun x => x + a) '' Set.Ioi b = Set.Ioi (b + a)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => x + a) '' Set.Icc b c = Set.Icc (b + a) (c + a)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => x + a) '' Set.Ico b c = Set.Ico (b + a) (c + a)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => x + a) '' Set.Ioc b c = Set.Ioc (b + a) (c + a)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => x + a) '' Set.Ioo b c = Set.Ioo (b + a) (c + a)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b : M<GOAL>(fun x => a + x) '' Set.Ici b = Set.Ici (a + b)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b : M<GOAL>(fun x => a + x) '' Set.Ioi b = Set.Ioi (a + b)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => a + x) '' Set.Icc b c = Set.Icc (a + b) (a + c)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => a + x) '' Set.Ico b c = Set.Ico (a + b) (a + c)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => a + x) '' Set.Ioc b c = Set.Ioc (a + b) (a + c)
<VAR>M : Type u_1<VAR>OrderedCancelAddCommMonoid M<VAR>ExistsAddOfLE M<VAR>a b c : M<GOAL>(fun x => a + x) '' Set.Ioo b c = Set.Ioo (a + b) (a + c)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => c + x) (Multiset.Ico a b) = Multiset.Ico (c + a) (c + b)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => c + x) (Multiset.Ioc a b) = Multiset.Ioc (c + a) (c + b)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => c + x) (Multiset.Ioo a b) = Multiset.Ioo (c + a) (c + b)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => x + c) (Multiset.Icc a b) = Multiset.Icc (a + c) (b + c)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => x + c) (Multiset.Ico a b) = Multiset.Ico (a + c) (b + c)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => x + c) (Multiset.Ioc a b) = Multiset.Ioc (a + c) (b + c)
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.map (fun x => x + c) (Multiset.Ioo a b) = Multiset.Ioo (a + c) (b + c)
<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Ring R<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>f : R →* M<GOAL>f (-1) = 1
<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Ring R<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>f : R →* M<VAR>x : R<GOAL>f (-x) = f x
<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Ring R<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>f : R →* M<VAR>x y : R<GOAL>f (x - y) = f (y - x)
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>n : ℕ<GOAL>0 ^ n ≤ 1
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>x y : R<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hn : n ≠ 0<GOAL>x ^ n + y ^ n ≤ (x + y) ^ n
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>n : ℕ<GOAL>0 ≤ a → a ≤ 1 → a ^ n ≤ 1
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>h₀ : 0 ≤ a<VAR>h₁ : a < 1<VAR>n : ℕ<GOAL>n ≠ 0 → a ^ n < 1
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>H : 1 ≤ a<VAR>n : ℕ<GOAL>1 ≤ a ^ n
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>h : 1 ≤ a<GOAL>Monotone fun x => a ^ x
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>n m : ℕ<VAR>ha : 1 ≤ a<VAR>h : n ≤ m<GOAL>a ^ n ≤ a ^ m
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>m : ℕ<VAR>ha : 1 ≤ a<VAR>h : m ≠ 0<GOAL>a ≤ a ^ m
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a b : R<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<VAR>n : ℕ<GOAL>a ^ n ≤ b ^ n
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a : R<VAR>ha : 1 < a<VAR>n : ℕ<GOAL>n ≠ 0 → 1 < a ^ n
<VAR>R : Type u_3<VAR>OrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a ^ n + b ^ n ≤ 2 * (a + b) ^ n
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>x y : R<VAR>h : x < y<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>n ≠ 0 → x ^ n < y ^ n
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>StrictMonoOn (fun x => x ^ n) {a | 0 ≤ a}
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>h : 1 < a<GOAL>StrictMono fun x => a ^ x
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>n m : ℕ<VAR>h : 1 < a<VAR>hmn : m < n<GOAL>a ^ m < a ^ n
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>n m : ℕ<VAR>h : 1 < a<GOAL>a ^ n < a ^ m ↔ n < m
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>n m : ℕ<VAR>h : 1 < a<GOAL>a ^ n ≤ a ^ m ↔ n ≤ m
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>m : ℕ<VAR>h : 1 < a<VAR>hm : 1 < m<GOAL>a < a ^ m
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<GOAL>StrictAnti fun x => a ^ x
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>n m : ℕ<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<GOAL>a ^ m < a ^ n ↔ n < m
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>n m : ℕ<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<VAR>hmn : m < n<GOAL>a ^ n < a ^ m
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<VAR>hn : 1 < n<GOAL>a ^ n < a
<VAR>R : Type u_3<VAR>StrictOrderedSemiring R<VAR>a : R<VAR>ha : 0 < a<GOAL>0 < a ^ 2
<VAR>R : Type u_3<VAR>StrictOrderedRing R<VAR>a : R<VAR>ha : a < 0<GOAL>0 < a ^ 2
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hn : n ≠ 0<GOAL>a ^ n ≤ b ^ n ↔ a ≤ b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hn : n ≠ 0<GOAL>a ^ n < b ^ n ↔ a < b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hn : n ≠ 0<GOAL>a ^ n = b ^ n ↔ a = b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>ha₀ : 0 < a<VAR>ha₁ : a ≠ 1<GOAL>Function.Injective fun x => a ^ x
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>m n : ℕ<VAR>ha₀ : 0 < a<VAR>ha₁ : a ≠ 1<GOAL>a ^ m = a ^ n ↔ m = n
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>a ^ n ≤ 1 ↔ a ≤ 1
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>1 ≤ a ^ n ↔ 1 ≤ a
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>a ^ n < 1 ↔ a < 1
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>1 < a ^ n ↔ 1 < a
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>a ^ n = 1 ↔ a = 1
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>a ^ 2 ≤ 1 ↔ a ≤ 1
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>a ^ 2 < 1 ↔ a < 1
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>1 ≤ a ^ 2 ↔ 1 ≤ a
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>1 < a ^ 2 ↔ 1 < a
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>hb : 0 ≤ b<VAR>h : a ^ n < b ^ n<GOAL>a < b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hb : 0 ≤ b<VAR>h : a ^ n ≤ b ^ n<GOAL>a ≤ b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a ^ 2 = b ^ 2 ↔ a = b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>hb : 0 ≤ b<GOAL>a * a < b * b → a < b
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>ExistsAddOfLE R<GOAL>(a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>ExistsAddOfLE R<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>n : ℕ<GOAL>(a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Even n<GOAL>(a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Even n<VAR>a : R<GOAL>0 ≤ a ^ n
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Even n<VAR>ha : a ≠ 0<GOAL>0 < a ^ n
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Even n<VAR>h₀ : n ≠ 0<GOAL>0 < a ^ n ↔ a ≠ 0
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Odd n<GOAL>a ^ n < 0 ↔ a < 0
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Odd n<GOAL>0 ≤ a ^ n ↔ 0 ≤ a
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Odd n<GOAL>a ^ n ≤ 0 ↔ a ≤ 0
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a : R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Odd n<GOAL>0 < a ^ n ↔ 0 < a
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>n : ℕ<VAR>ExistsAddOfLE R<VAR>hn : Odd n<GOAL>StrictMono fun a => a ^ n
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>ExistsAddOfLE R<VAR>a : R<GOAL>0 < a ^ 2 ↔ a ≠ 0
<VAR>R : Type u_3<VAR>LinearOrderedSemiring R<VAR>a b : R<VAR>ExistsAddOfLE R<VAR>h : a ^ 2 ≤ b<GOAL>a ^ 4 ≤ b ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>mabs (a ^ n) = mabs a ^ |n|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>|n • a| = |n| • |a|
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Ring α<VAR>a : α<GOAL>Odd |a| ↔ Odd a
<VAR>α : Type u_1<VAR>LinearOrderedRing α<GOAL>|1| = 1
<VAR>α : Type u_1<VAR>LinearOrderedRing α<GOAL>|2| = 2
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>|a * b| = |a| * |b|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<VAR>n : ℕ<GOAL>|a ^ n| = |a| ^ n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<VAR>n : ℕ<GOAL>|a| ^ n = |a ^ n|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>n : ℕ<VAR>hn : Even n<VAR>a : α<GOAL>|a| ^ n = a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>n : ℕ<GOAL>|(-1) ^ n| = 1
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>n : ℕ<VAR>a : α<VAR>h : n ≠ 0<GOAL>|a ^ n| = 1 ↔ |a| = 1
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>|a| * |a| = a * a
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>|a * a| = a * a
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>|a| = |b| ↔ a * a = b * b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>|a| < |b| ↔ a * a < b * b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>|a| ≤ |b| ↔ a * a ≤ b * b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>|a| ≤ 1 ↔ a * a ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>|a| ^ 2 = a ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>x : α<GOAL>|x ^ 2| = x ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>a ^ 2 < b ^ 2 ↔ |a| < |b|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>h1 : -b < a<VAR>h2 : a < b<GOAL>a ^ 2 < b ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>h1 : -b ≤ a<VAR>h2 : a ≤ b<GOAL>a ^ 2 ≤ b ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>h : a ^ 2 < b ^ 2<VAR>hb : 0 ≤ b<GOAL>|a| < b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>h : a ^ 2 < b ^ 2<VAR>hb : 0 ≤ b<GOAL>-b < a ∧ a < b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>h : a ^ 2 ≤ b ^ 2<VAR>hb : 0 ≤ b<GOAL>|a| ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>h : a ^ 2 ≤ b ^ 2<VAR>hb : 0 ≤ b<GOAL>-b ≤ a ∧ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<GOAL>a ^ 2 = b ^ 2 ↔ |a| = |b|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>a ^ 2 ≤ 1 ↔ |a| ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>a ^ 2 < 1 ↔ |a| < 1
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>1 ≤ a ^ 2 ↔ 1 ≤ |a|
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : α<GOAL>1 < a ^ 2 ↔ 1 < |a|
<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>a : α<GOAL>∃ b > 0, |a| < b
<VAR>α : Type u_1<VAR>LinearOrderedCommRing α<VAR>a b : α<GOAL>|a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
<VAR>α : Type u_1<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<GOAL>|a| ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>Ring α<VAR>LinearOrder α<VAR>a : α<GOAL>|a| ∣ a
<VAR>α : Type u_1<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<GOAL>a ∣ |b| ↔ a ∣ b
<VAR>α : Type u_1<VAR>Ring α<VAR>LinearOrder α<VAR>a : α<GOAL>a ∣ |a|
<VAR>α : Type u_1<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<GOAL>|a| ∣ |b| ↔ a ∣ b
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<GOAL>a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>a : R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>a : R<VAR>n : ℕ<GOAL>a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hb : b ≠ 0<GOAL>a ^ n = -b ^ n ↔ a = -b ∧ Odd n
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>a : R<VAR>n : ℕ<GOAL>a ^ n = -1 ↔ a = -1 ∧ Odd n
<VAR>n a : ℕ<VAR>ha : Even a<GOAL>Odd (n % a) ↔ Odd n
<VAR>n a : ℕ<VAR>ha : Even a<GOAL>Even (n % a) ↔ Even n
<VAR>n a : ℕ<VAR>hn : Odd n<VAR>ha : Even a<GOAL>Odd (n % a)
<VAR>n a : ℕ<VAR>hn : Even n<VAR>ha : Even a<GOAL>Even (n % a)
<VAR>m n : ℕ<VAR>hn : Odd n<VAR>hm : m ∣ n<GOAL>Odd m
<VAR>m n : ℕ<VAR>hn : Odd n<VAR>hm : m ∣ n<GOAL>m ≠ 2
<VAR>α : Type u_1<VAR>OrderedSemiring α<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>h : 0 ∈ Set.Icc 0 1<GOAL>⟨0, h⟩ = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>h : 1 ∈ Set.Icc 0 1<GOAL>⟨1, h⟩ = 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑x = 0 ↔ x = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑x ≠ 0 ↔ x ≠ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑x = 1 ↔ x = 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑x ≠ 1 ↔ x ≠ 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<GOAL>0 ≤ ↑x
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑x ≤ 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>t : ↑(Set.Icc 0 1)<GOAL>0 ≤ t
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>t : ↑(Set.Icc 0 1)<GOAL>t ≤ 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x y : ↑(Set.Icc 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Icc 0 1)<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x y : ↑(Set.Icc 0 1)<GOAL>x * y ≤ x
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x y : ↑(Set.Icc 0 1)<GOAL>x * y ≤ y
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>t : β<VAR>ht : t ∈ Set.Icc 0 1<GOAL>1 - t ∈ Set.Icc 0 1
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>t : β<GOAL>t ∈ Set.Icc 0 1 ↔ 1 - t ∈ Set.Icc 0 1
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>x : ↑(Set.Icc 0 1)<GOAL>0 ≤ 1 - ↑x
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>x : ↑(Set.Icc 0 1)<GOAL>1 - ↑x ≤ 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Nontrivial α<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>h : 0 ∈ Set.Ico 0 1<GOAL>⟨0, h⟩ = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>x : ↑(Set.Ico 0 1)<GOAL>↑x = 0 ↔ x = 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>x : ↑(Set.Ico 0 1)<GOAL>↑x ≠ 0 ↔ x ≠ 0
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Ico 0 1)<GOAL>0 ≤ ↑x
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x : ↑(Set.Ico 0 1)<GOAL>↑x < 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>t : ↑(Set.Ico 0 1)<GOAL>0 ≤ t
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>x y : ↑(Set.Ico 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>h : 1 ∈ Set.Ioc 0 1<GOAL>⟨1, h⟩ = 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioc 0 1)<GOAL>↑x = 1 ↔ x = 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioc 0 1)<GOAL>↑x ≠ 1 ↔ x ≠ 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioc 0 1)<GOAL>0 < ↑x
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioc 0 1)<GOAL>↑x ≤ 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>t : ↑(Set.Ioc 0 1)<GOAL>t ≤ 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x y : ↑(Set.Ioc 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioc 0 1)<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioo 0 1)<GOAL>0 < ↑x
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x : ↑(Set.Ioo 0 1)<GOAL>↑x < 1
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>x y : ↑(Set.Ioo 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>t : β<VAR>ht : t ∈ Set.Ioo 0 1<GOAL>1 - t ∈ Set.Ioo 0 1
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>t : β<GOAL>t ∈ Set.Ioo 0 1 ↔ 1 - t ∈ Set.Ioo 0 1
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>x : ↑(Set.Ioo 0 1)<GOAL>0 < 1 - ↑x
<VAR>β : Type u_2<VAR>OrderedRing β<VAR>x : ↑(Set.Ioo 0 1)<GOAL>1 - ↑x < 1
<VAR>R : Type u_1<VAR>StrictOrderedSemiring R<VAR>l : List R<VAR>h : ∀ a ∈ l, 0 < a<GOAL>0 < l.prod
<VAR>α : Type u_2<VAR>CanonicallyOrderedCommSemiring α<VAR>Nontrivial α<VAR>l : List α<GOAL>0 < l.prod ↔ ∀ x ∈ l, 0 < x
<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₁ l₂ : List M<VAR>h : List.Forall₂ (fun x x_1 => x ≤ x_1) l₁ l₂<GOAL>l₁.prod ≤ l₂.prod
<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₁ l₂ : List M<VAR>h : List.Forall₂ (fun x x_1 => x ≤ x_1) l₁ l₂<GOAL>l₁.sum ≤ 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₁ l₂ : List M<VAR>h : l₁.Sublist l₂<VAR>h₁ : ∀ a ∈ l₂, 0 ≤ a<GOAL>l₁.sum ≤ 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₁ l₂ : List M<VAR>h : l₁.Sublist l₂<VAR>h₁ : ∀ a ∈ l₂, 1 ≤ a<GOAL>l₁.prod ≤ l₂.prod
<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₁ l₂ : List M<VAR>h : List.SublistForall₂ (fun x x_1 => x ≤ x_1) l₁ l₂<VAR>h₁ : ∀ a ∈ l₂, 0 ≤ a<GOAL>l₁.sum ≤ 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₁ l₂ : List M<VAR>h : List.SublistForall₂ (fun x x_1 => x ≤ x_1) l₁ l₂<VAR>h₁ : ∀ a ∈ l₂, 1 ≤ a<GOAL>l₁.prod ≤ l₂.prod
<VAR>ι : Type u_1<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 ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ l, f i ≤ g i<GOAL>(List.map f l).sum ≤ (List.map g l).sum