ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ n
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : x ≤ 1<VAR>n : ℕ<GOAL>x ^ n ≤ 1
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : x ≤ 0<VAR>n : ℕ<GOAL>n • x ≤ 0
<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>x : M<VAR>hx : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ n
<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>x : M<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>0 ≤ n • 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>x : M<VAR>hx : x ≤ 1<VAR>n : ℕ<GOAL>x ^ n ≤ 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>x : M<VAR>hx : x ≤ 0<VAR>n : ℕ<GOAL>n • x ≤ 0
<VAR>β : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>Preorder β<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>f : β → M<VAR>hf : StrictMono f<VAR>n : ℕ<GOAL>n ≠ 0 → StrictMono fun x => f x ^ n
<VAR>β : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>Preorder β<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>f : β → M<VAR>hf : StrictMono f<VAR>n : ℕ<GOAL>n ≠ 0 → StrictMono fun x => n • f x
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>StrictMono fun x => x ^ n
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>StrictMono fun x => n • x
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a b : M<VAR>hab : a < b<GOAL>n • a < n • b
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a b : M<VAR>hab : a < b<GOAL>a ^ n < b ^ n
<VAR>β : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>Preorder β<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : β → M<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>Monotone fun a => n • f a
<VAR>β : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>Preorder β<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : β → M<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>Monotone fun a => f a ^ n
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ℕ<GOAL>Monotone fun a => n • a
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>n : ℕ<GOAL>Monotone fun a => a ^ n
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<VAR>h : x < 0<GOAL>n • x < 0
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<VAR>h : x < 1<GOAL>x ^ n < 1
<VAR>M : Type u_3<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<VAR>h : x < 1<GOAL>x ^ n < 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>n : ℕ<VAR>x : M<VAR>hn : 0 < n<VAR>h : x < 0<GOAL>n • x < 0
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>0 ≤ n • x ↔ 0 ≤ x
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 ≤ x ^ n ↔ 1 ≤ x
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • x ≤ 0 ↔ x ≤ 0
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x ^ n ≤ 1 ↔ x ≤ 1
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 < x ^ n ↔ 1 < x
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>0 < n • x ↔ 0 < x
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x ^ n < 1 ↔ x < 1
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • x < 0 ↔ x < 0
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x ^ n = 1 ↔ x = 1
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • x = 0 ↔ x = 0
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>m n : ℕ<VAR>ha : 0 < a<GOAL>m • a ≤ n • a ↔ m ≤ n
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>m n : ℕ<VAR>ha : 1 < a<GOAL>a ^ m ≤ a ^ n ↔ m ≤ n
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>m n : ℕ<VAR>ha : 0 < a<GOAL>m • a < n • a ↔ m < n
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>m n : ℕ<VAR>ha : 1 < a<GOAL>a ^ m < a ^ n ↔ m < n
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : M<VAR>n : ℕ<GOAL>n • a < n • b → a < b
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : M<VAR>n : ℕ<GOAL>a ^ n < b ^ n → a < b
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : M<VAR>h : a + b < 2 • c<GOAL>min a b < c
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : M<VAR>h : a * b < c ^ 2<GOAL>min a b < c
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : M<VAR>h : a ^ 2 < b * c<GOAL>a < max b c
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : M<VAR>h : 2 • a < b + c<GOAL>a < max b c
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • a ≤ n • b → a ≤ b
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n ≤ b ^ n → a ≤ b
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : M<VAR>h : a + b ≤ 2 • c<GOAL>min a b ≤ c
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : M<VAR>h : a * b ≤ c ^ 2<GOAL>min a b ≤ c
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : M<VAR>h : 2 • a ≤ b + c<GOAL>a ≤ max b c
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : M<VAR>h : a ^ 2 ≤ b * c<GOAL>a ≤ max b c
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<GOAL>x ^ n < 1 ↔ x < 1
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<GOAL>n • x < 0 ↔ x < 0
<VAR>M : Type u_3<VAR>Monoid M<VAR>LinearOrder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<GOAL>x ^ n < 1 ↔ x < 1
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>LinearOrder M<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>n : ℕ<VAR>x : M<VAR>hn : 0 < n<GOAL>n • x < 0 ↔ x < 0
<VAR>G : Type u_2<VAR>SubNegMonoid G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x : G<VAR>H : 0 ≤ x<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>0 ≤ n • x
<VAR>G : Type u_2<VAR>DivInvMonoid G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : G<VAR>H : 1 ≤ x<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>1 ≤ x ^ n
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Additive.ofMul a ≤ Additive.ofMul b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Additive.ofMul a < Additive.ofMul b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Additive α<GOAL>Additive.toMul a ≤ Additive.toMul b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Additive α<GOAL>Additive.toMul a < Additive.toMul b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Multiplicative.ofAdd a ≤ Multiplicative.ofAdd b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Multiplicative.ofAdd a < Multiplicative.ofAdd b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Multiplicative α<GOAL>Multiplicative.toAdd a ≤ Multiplicative.toAdd b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Multiplicative α<GOAL>Multiplicative.toAdd a < Multiplicative.toAdd b ↔ a < b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>OrderedCommRing R<VAR>OrderedRing A<VAR>Algebra R A<VAR>OrderedSMul R A<GOAL>Monotone ⇑(algebraMap R A)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One α<VAR>Preorder α<VAR>a : α<VAR>ha : 1 ≤ a<GOAL>1 ≤ Function.const β a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero α<VAR>Preorder α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ Function.const β a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One α<VAR>Preorder α<VAR>a : α<VAR>ha : a ≤ 1<GOAL>Function.const β a ≤ 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero α<VAR>Preorder α<VAR>a : α<VAR>ha : a ≤ 0<GOAL>Function.const β a ≤ 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>1 ≤ Function.const β a ↔ 1 ≤ a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>0 ≤ Function.const β a ↔ 0 ≤ a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>0 < Function.const β a ↔ 0 < a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>1 < Function.const β a ↔ 1 < a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>Function.const β a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>Function.const β a ≤ 1 ↔ a ≤ 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>One α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>Function.const β a < 1 ↔ a < 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Zero α<VAR>Preorder α<VAR>a : α<VAR>Nonempty β<GOAL>Function.const β a < 0 ↔ a < 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>One γ<VAR>LE γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<VAR>hg : 1 ≤ g<VAR>he : 1 ≤ e<GOAL>1 ≤ Function.extend f g e
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Zero γ<VAR>LE γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<VAR>hg : 0 ≤ g<VAR>he : 0 ≤ e<GOAL>0 ≤ Function.extend f g e
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>One γ<VAR>LE γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<VAR>hg : g ≤ 1<VAR>he : e ≤ 1<GOAL>Function.extend f g e ≤ 1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Zero γ<VAR>LE γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<VAR>hg : g ≤ 0<VAR>he : e ≤ 0<GOAL>Function.extend f g e ≤ 0
<VAR>q : ℚ≥0<GOAL>↑q⁻¹ = (↑q)⁻¹
<VAR>p q : ℚ≥0<GOAL>↑(p / q) = ↑p / ↑q
<VAR>q : ℚ≥0<GOAL>q⁻¹ = NNRat.divNat q.den q.num
<VAR>p q : ℚ≥0<GOAL>p / q = NNRat.divNat (p.num * q.den) (p.den * q.num)
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>a : α<VAR>Invertible a<GOAL>0 < ⅟a ↔ 0 < a
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>a : α<VAR>Invertible a<GOAL>⅟a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>a : α<VAR>Invertible a<GOAL>0 ≤ ⅟a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>a : α<VAR>Invertible a<GOAL>⅟a < 0 ↔ a < 0
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>a : α<VAR>Invertible a<VAR>h : 1 ≤ a<GOAL>⅟a ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>Nontrivial α<VAR>n : ℕ<VAR>Invertible ↑n<GOAL>0 < ⅟↑n
<VAR>α : Type u_1<VAR>Add α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>b c : α<VAR>bc : b ≤ c<VAR>a : α<GOAL>a + b ≤ a + c
<VAR>α : Type u_1<VAR>Mul α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>b c : α<VAR>bc : b ≤ c<VAR>a : α<GOAL>a * b ≤ a * c
<VAR>α : Type u_1<VAR>Mul α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>bc : a * b ≤ a * c<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>bc : a + b ≤ a + c<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>LE α<VAR>i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>b c : α<VAR>bc : b ≤ c<VAR>a : α<GOAL>b + a ≤ c + a
<VAR>α : Type u_1<VAR>Mul α<VAR>LE α<VAR>i : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>b c : α<VAR>bc : b ≤ c<VAR>a : α<GOAL>b * a ≤ c * a
<VAR>α : Type u_1<VAR>Add α<VAR>LE α<VAR>i : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>bc : b + a ≤ c + a<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>Mul α<VAR>LE α<VAR>i : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>bc : b * a ≤ c * a<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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 : α<VAR>b c : α<GOAL>a + b ≤ a + c ↔ b ≤ c
<VAR>α : Type u_1<VAR>Mul α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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 : α<VAR>b c : α<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>α : Type u_1<VAR>Mul α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b c : α<GOAL>b * a ≤ c * a ↔ b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b c : α<GOAL>b + a ≤ c + a ↔ b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) 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 : α<VAR>b c : α<GOAL>a + b < a + c ↔ b < c
<VAR>α : Type u_1<VAR>Mul α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) 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 : α<VAR>b c : α<GOAL>a * b < a * c ↔ b < c
<VAR>α : Type u_1<VAR>Add α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b c : α<GOAL>b + a < c + a ↔ b < c
<VAR>α : Type u_1<VAR>Mul α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b c : α<GOAL>b * a < c * a ↔ b < c
<VAR>α : Type u_1<VAR>Add α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>b c : α<VAR>bc : b < c<VAR>a : α<GOAL>a + b < a + c
<VAR>α : Type u_1<VAR>Mul α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>b c : α<VAR>bc : b < c<VAR>a : α<GOAL>a * b < a * c
<VAR>α : Type u_1<VAR>Mul α<VAR>LT α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>bc : a * b < a * c<GOAL>b < c
<VAR>α : Type u_1<VAR>Add α<VAR>LT α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>bc : a + b < a + c<GOAL>b < c
<VAR>α : Type u_1<VAR>Mul α<VAR>LT α<VAR>i : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>b c : α<VAR>bc : b < c<VAR>a : α<GOAL>b * a < c * a
<VAR>α : Type u_1<VAR>Add α<VAR>LT α<VAR>i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>b c : α<VAR>bc : b < c<VAR>a : α<GOAL>b + a < c + a
<VAR>α : Type u_1<VAR>Mul α<VAR>LT α<VAR>i : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>bc : b * a < c * a<GOAL>b < c
<VAR>α : Type u_1<VAR>Add α<VAR>LT α<VAR>i : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>bc : b + a < c + a<GOAL>b < c
<VAR>α : Type u_1<VAR>Add α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>Add α<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>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>α : Type u_1<VAR>Add α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a + c < b + d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>Add α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>Add α<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>a b c d : α<VAR>h₁ : a < b<VAR>h₂ : c < d<GOAL>a + c < b + d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a * c ≤ b * d
<VAR>α : Type u_1<VAR>Add α<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>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a + c ≤ b + d
<VAR>α : Type u_1<VAR>Mul α<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>a b c d e f : α<VAR>h₁ : a ≤ d<VAR>h₂ : b ≤ e<VAR>h₃ : c ≤ f<GOAL>a * b * c ≤ d * e * f
<VAR>α : Type u_1<VAR>Add α<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>a b c d e f : α<VAR>h₁ : a ≤ d<VAR>h₂ : b ≤ e<VAR>h₃ : c ≤ f<GOAL>a + b + c ≤ d + e + f
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a + b < c<VAR>hle : d ≤ b<GOAL>a + d < c
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a * b < c<VAR>hle : d ≤ b<GOAL>a * d < c
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a * b ≤ c<VAR>hle : d ≤ b<GOAL>a * d ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a + b ≤ c<VAR>hle : d ≤ b<GOAL>a + d ≤ c