ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - (a + b) = 0
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>0 < a - b ↔ ¬a ≤ b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>h : a < b<GOAL>0 < b - a
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h : a < b<GOAL>a - c < b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<GOAL>a - b ≤ a - c ↔ c ≤ b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>hb : AddLECancellable b<VAR>hc : AddLECancellable c<VAR>hba : b ≤ a<VAR>hca : c ≤ a<GOAL>a - b = a - c ↔ b = c
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ a<GOAL>a - b ≤ a - c ↔ c ≤ b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hba : b ≤ a<VAR>hca : c ≤ a<GOAL>a - b = a - c ↔ b = c
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>0 < a - b ↔ b < a
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - b = a - min a b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<GOAL>a < b - c ↔ a + c < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<GOAL>a < b - c ↔ c + a < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<GOAL>a - c < b - c ↔ a < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ha : AddLECancellable a<VAR>h₁ : 0 < a<VAR>h₂ : 0 < b<GOAL>a - b < a
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ha : AddLECancellable a<GOAL>a - b < a ↔ 0 < a ∧ 0 < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>hb : AddLECancellable b<VAR>h : b ≤ a<GOAL>a - b < a - c ↔ c < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ a<GOAL>a - c < b - c ↔ a < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < a → 0 < b → a - b < a
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a - b < a ↔ 0 < a ∧ 0 < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<GOAL>a - b < a - c ↔ c < b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a - (a - b) = min a b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - b + b = max a b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a + (b - a) = max a b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - min a b = a - b
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - b + min a b = a
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>m n : α<VAR>hm : Even m<VAR>hn : Even n<GOAL>Even (m - n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>AddCommSemigroup β<VAR>f : α → β<VAR>a b : α<GOAL>f (min a b) + f (max a b) = f a + f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>CommSemigroup β<VAR>f : α → β<VAR>a b : α<GOAL>f (min a b) * f (max a b) = f a * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>CommSemigroup β<VAR>f : α → β<VAR>a b : α<GOAL>f (max a b) * f (min a b) = f a * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>AddCommSemigroup β<VAR>f : α → β<VAR>a b : α<GOAL>f (max a b) + f (min a b) = f a + f b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>a b : α<GOAL>min a b + max a b = a + b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>CommSemigroup α<VAR>a b : α<GOAL>min a b * max a b = a * b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>a b : α<GOAL>max a b + min a b = a + b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>CommSemigroup α<VAR>a b : α<GOAL>max a b * min a b = a * b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>min (a * b) (a * c) = a * min b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>min (a + b) (a + c) = a + min b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>max (a * b) (a * c) = a * max b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>max (a + b) (a + c) = a + max b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>min (a + c) (b + c) = min a b + c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>min (a * c) (b * c) = min a b * c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>max (a * c) (b * c) = max a b * c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>max (a + c) (b + c) = max a b + c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ + b₁ < a₂ + b₂ → a₁ < a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ + b₁ ≤ a₂ + b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<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₁ a₂ b₁ b₂ : α<GOAL>a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Mul α<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>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₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<GOAL>a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Add α<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>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₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<GOAL>a₁ + b₁ < a₂ + b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>MulOneClass α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>hb : 1 ≤ b<GOAL>min a b ≤ a * b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddZeroClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>hb : 0 ≤ b<GOAL>min a b ≤ a + b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>MulOneClass α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<GOAL>min a b ≤ a * b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddZeroClass α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<GOAL>min a b ≤ a + b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>MulOneClass α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>max a b ≤ a * b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddZeroClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>max a b ≤ a + b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>self : CovariantClass M N μ r<GOAL>Covariant M N μ r
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>self : ContravariantClass M N μ r<GOAL>Contravariant M N μ r
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>CovariantClass M N μ r<VAR>ContravariantClass M N μ r<VAR>m : M<VAR>a b : N<GOAL>r (μ m a) (μ m b) ↔ r a b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>h : Covariant M N μ r<GOAL>Covariant M N μ (flip r)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>h : Contravariant M N μ r<GOAL>Contravariant M N μ (flip r)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>CovariantClass M N μ r<VAR>m : M<VAR>a b : N<VAR>ab : r a b<GOAL>r (μ m a) (μ m b)
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>Group N<GOAL>Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>AddGroup N<GOAL>Covariant N N (fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>AddGroup N<GOAL>Covariant N N (Function.swap fun x x_1 => x + x_1) r ↔ Contravariant N N (Function.swap fun x x_1 => x + x_1) r
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>Group N<GOAL>Covariant N N (Function.swap fun x x_1 => x * x_1) r ↔ Contravariant N N (Function.swap fun x x_1 => x * x_1) r
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>CovariantClass M N μ r<VAR>IsTrans N r<VAR>m : M<VAR>a b c : N<VAR>ab : r a b<VAR>rl : r (μ m b) c<GOAL>r (μ m a) c
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>CovariantClass M N μ r<VAR>IsTrans N r<VAR>m : M<VAR>a b c : N<VAR>ab : r a b<VAR>rr : r c (μ m a)<GOAL>r c (μ m b)
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>mu : N → N → N<VAR>IsTrans N r<VAR>i : CovariantClass N N mu r<VAR>i' : CovariantClass N N (Function.swap mu) r<VAR>a b c d : N<VAR>ab : r a b<VAR>cd : r c d<GOAL>r (mu a c) (mu b d)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>ContravariantClass M N μ r<VAR>m : M<VAR>a b : N<VAR>ab : r (μ m a) (μ m b)<GOAL>r a b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>ContravariantClass M N μ r<VAR>IsTrans N r<VAR>m : M<VAR>a b c : N<VAR>ab : r (μ m a) b<VAR>rl : r (μ m b) (μ m c)<GOAL>r (μ m a) c
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>ContravariantClass M N μ r<VAR>IsTrans N r<VAR>m : M<VAR>a b c : N<VAR>ab : r (μ m a) (μ m b)<VAR>rr : r b (μ m c)<GOAL>r a (μ m c)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>Preorder N<VAR>CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>m : M<GOAL>Monotone (μ m)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>α : Type u_3<VAR>Preorder α<VAR>Preorder N<VAR>f : N → α<VAR>CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>m : M<GOAL>Monotone fun x => f (μ m x)
<VAR>N : Type u_2<VAR>α : Type u_3<VAR>Preorder α<VAR>Preorder N<VAR>f : N → α<VAR>μ : N → N → N<VAR>CovariantClass N N (Function.swap μ) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>m : N<GOAL>Monotone fun x => f (μ x m)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>α : Type u_3<VAR>Preorder α<VAR>Preorder N<VAR>f : N → α<VAR>CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>m : M<GOAL>Antitone fun x => f (μ m x)
<VAR>N : Type u_2<VAR>α : Type u_3<VAR>Preorder α<VAR>Preorder N<VAR>f : N → α<VAR>μ : N → N → N<VAR>CovariantClass N N (Function.swap μ) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>m : N<GOAL>Antitone fun x => f (μ x m)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>PartialOrder N<GOAL>(Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>PartialOrder N<VAR>CovariantClass M N μ fun x x_1 => x < x_1<GOAL>CovariantClass M N μ fun x x_1 => x ≤ x_1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>PartialOrder N<GOAL>(Contravariant M N μ fun x x_1 => x ≤ x_1) ↔ (Contravariant M N μ fun x x_1 => x < x_1) ∧ Contravariant M N μ fun x x_1 => x = x_1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>PartialOrder N<GOAL>(Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>LinearOrder N<GOAL>(Covariant M N μ fun x x_1 => x ≤ x_1) ↔ Contravariant M N μ fun x x_1 => x < x_1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>LinearOrder N<GOAL>(Covariant M N μ fun x x_1 => x < x_1) ↔ Contravariant M N μ fun x x_1 => x ≤ x_1
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>mu : N → N → N<VAR>IsSymmOp N N mu<GOAL>Covariant N N (flip mu) r ↔ Covariant N N mu r
<VAR>N : Type u_2<VAR>r : N → N → Prop<VAR>mu : N → N → N<VAR>IsSymmOp N N mu<GOAL>Contravariant N N (flip mu) r ↔ Contravariant N N mu r
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>ContravariantClass M N μ fun x x_1 => x = x_1<VAR>PartialOrder N<VAR>CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>CovariantClass M N μ fun x x_1 => x < x_1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>PartialOrder N<VAR>ContravariantClass M N μ fun x x_1 => x = x_1<VAR>ContravariantClass M N μ fun x x_1 => x < x_1<GOAL>ContravariantClass M N μ fun x x_1 => x ≤ x_1
<VAR>α : Type u<VAR>Add α<GOAL>WithZero.toMulBot 0 = Multiplicative.ofAdd ⊥
<VAR>α : Type u<VAR>Add α<VAR>x : Multiplicative α<GOAL>WithZero.toMulBot ↑x = Multiplicative.ofAdd ↑(Multiplicative.toAdd x)
<VAR>α : Type u<VAR>Add α<GOAL>WithZero.toMulBot.symm (Multiplicative.ofAdd ⊥) = 0
<VAR>α : Type u<VAR>Add α<VAR>x : α<GOAL>WithZero.toMulBot.symm (Multiplicative.ofAdd ↑x) = ↑(Multiplicative.ofAdd x)
<VAR>α : Type u<VAR>Add α<VAR>Preorder α<GOAL>StrictMono ⇑WithZero.toMulBot
<VAR>α : Type u<VAR>Add α<VAR>Preorder α<VAR>a b : WithZero (Multiplicative α)<GOAL>WithZero.toMulBot a ≤ WithZero.toMulBot b ↔ a ≤ b
<VAR>α : Type u<VAR>Add α<VAR>Preorder α<VAR>a b : WithZero (Multiplicative α)<GOAL>WithZero.toMulBot a < WithZero.toMulBot b ↔ a < b
<VAR>α : Type u_3<VAR>self : OrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ b → ∀ (c : α), c + a ≤ c + b
<VAR>α : Type u_3<VAR>self : OrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ b → ∀ (c : α), c * a ≤ c * b
<VAR>M : Type u_3<VAR>OrderedCommMonoid M<GOAL>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
<VAR>M : Type u_3<VAR>OrderedAddCommMonoid M<GOAL>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
<VAR>α : Type u_3<VAR>self : OrderedCancelAddCommMonoid α<VAR>a b c : α<GOAL>a + b ≤ a + c → b ≤ c
<VAR>α : Type u_3<VAR>self : OrderedCancelCommMonoid α<VAR>a b c : α<GOAL>a * b ≤ a * c → b ≤ c
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<GOAL>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<GOAL>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoid α<VAR>a : α<GOAL>1 ≤ a * a ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommMonoid α<VAR>a : α<GOAL>0 ≤ a + a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoid α<VAR>a : α<GOAL>1 < a * a ↔ 1 < a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommMonoid α<VAR>a : α<GOAL>0 < a + a ↔ 0 < a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommMonoid α<VAR>a : α<GOAL>a + a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoid α<VAR>a : α<GOAL>a * a ≤ 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommMonoid α<VAR>a : α<GOAL>a + a < 0 ↔ a < 0
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoid α<VAR>a : α<GOAL>a * a < 1 ↔ a < 1
<VAR>α : Type u_1<VAR>One α<VAR>AddZeroClass α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>a < a + 1
<VAR>α : Type u_1<VAR>One α<VAR>AddZeroClass α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>a < 1 + a
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 2
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 3
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>Preorder α<VAR>ZeroLEOneClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 4
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>LE α<VAR>ZeroLEOneClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>1 ≤ 2
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>LE α<VAR>ZeroLEOneClass α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>1 ≤ 2
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 2
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 3
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 4
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>1 < 2
<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>a b : M<VAR>hab : a ≤ b<VAR>i : ℕ<GOAL>i • a ≤ i • 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>a b : M<VAR>hab : a ≤ b<VAR>i : ℕ<GOAL>a ^ i ≤ b ^ i
<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>a : M<VAR>H : 1 ≤ a<VAR>n : ℕ<GOAL>1 ≤ 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>a : M<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ 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>a : M<VAR>H : a ≤ 1<VAR>n : ℕ<GOAL>a ^ 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>a : M<VAR>H : a ≤ 0<VAR>n : ℕ<GOAL>n • a ≤ 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>a : M<VAR>n m : ℕ<VAR>ha : 1 ≤ a<VAR>h : n ≤ m<GOAL>a ^ n ≤ a ^ m
<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>a : M<VAR>n m : ℕ<VAR>ha : 0 ≤ a<VAR>h : n ≤ m<GOAL>n • a ≤ m • 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>a : M<VAR>n m : ℕ<VAR>ha : a ≤ 1<VAR>h : n ≤ m<GOAL>a ^ m ≤ 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>a : M<VAR>n m : ℕ<VAR>ha : a ≤ 0<VAR>h : n ≤ m<GOAL>m • a ≤ n • a
<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>a : M<VAR>ha : 0 < a<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>0 < k • 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>a : M<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>1 < a ^ k
<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>a : M<VAR>ha : a < 0<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>k • a < 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>a : M<VAR>ha : a < 1<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>a ^ k < 1
<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 (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>n m : ℕ<VAR>ha : 1 < a<VAR>h : n < m<GOAL>a ^ n < a ^ m
<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 (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>n m : ℕ<VAR>ha : 0 < a<VAR>h : n < m<GOAL>n • a < m • a
<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 (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>ha : 0 < a<GOAL>StrictMono fun x => x • 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 (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>ha : 1 < a<GOAL>StrictMono fun x => a ^ 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>x : M<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>0 ≤ n • x