ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>MulPosReflectLT α<VAR>h : 0 < b<GOAL>0 < a * b ↔ 0 < a
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a * b ≤ 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a * b ≤ 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulReflectLT α<VAR>h : 0 < a * b<VAR>ha : 0 ≤ a<GOAL>0 < b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>MulPosReflectLT α<VAR>h : 0 < a * b<VAR>hb : 0 ≤ b<GOAL>0 < a
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulReflectLT α<VAR>MulPosReflectLT α<VAR>hab : 0 < a * b<GOAL>0 < a ↔ 0 < b
<VAR>α : Type u_1<VAR>a b c d : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>h₁ : a < b<VAR>h₂ : c < d<VAR>a0 : 0 ≤ a<VAR>c0 : 0 ≤ c<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>h₁ : a < b<VAR>h₂ : c < d<VAR>a0 : 0 ≤ a<VAR>c0 : 0 ≤ c<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<GOAL>a * a ≤ b * b
<VAR>α : Type u_1<VAR>MulZeroClass α<VAR>PartialOrder α<GOAL>PosMulMono α ↔ CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x ≤ x_1
<VAR>α : Type u_1<VAR>MulZeroClass α<VAR>PartialOrder α<GOAL>MulPosMono α ↔ CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x ≤ x_1
<VAR>α : Type u_1<VAR>MulZeroClass α<VAR>PartialOrder α<GOAL>PosMulReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>MulZeroClass α<VAR>PartialOrder α<GOAL>MulPosReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulZeroClass α<VAR>PartialOrder α<VAR>PosMulReflectLE α<VAR>a0 : 0 < a<GOAL>a * b = a * c ↔ b = c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulZeroClass α<VAR>PartialOrder α<VAR>MulPosReflectLE α<VAR>b0 : 0 < b<GOAL>a * b = c * b ↔ a = c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>MulZeroClass α<VAR>PartialOrder α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>a0 : 0 < a<VAR>d0 : 0 < d<GOAL>a * c = b * d ↔ a = b ∧ c = d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>MulZeroClass α<VAR>PartialOrder α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>b0 : 0 < b<VAR>c0 : 0 < c<GOAL>a * c = b * d ↔ a = b ∧ c = d
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>hab : 0 < a * b<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>h : 0 < a * b<VAR>ha : a ≤ 0<GOAL>b < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>h : 0 < a * b<VAR>ha : b ≤ 0<GOAL>a < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>hab : 0 < a * b<GOAL>a < 0 ↔ b < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>PosMulMono α<VAR>h : a * b < 0<VAR>a0 : 0 ≤ a<GOAL>b < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>MulPosMono α<VAR>h : a * b < 0<VAR>a0 : 0 ≤ a<GOAL>b < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>PosMulMono α<VAR>h : a * b < 0<VAR>b0 : 0 ≤ b<GOAL>a < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>LinearOrder α<VAR>MulPosMono α<VAR>h : a * b < 0<VAR>b0 : 0 ≤ b<GOAL>a < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>PosMulReflectLE α<VAR>a0 : 0 < a<GOAL>a ≤ a * b ↔ 1 ≤ b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>PosMulReflectLT α<VAR>a0 : 0 < a<GOAL>a < a * b ↔ 1 < b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>PosMulReflectLE α<VAR>a0 : 0 < a<GOAL>a * b ≤ a ↔ b ≤ 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>PosMulReflectLT α<VAR>a0 : 0 < a<GOAL>a * b < a ↔ b < 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>MulPosReflectLE α<VAR>a0 : 0 < a<GOAL>a ≤ b * a ↔ 1 ≤ b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>MulPosReflectLT α<VAR>a0 : 0 < a<GOAL>a < b * a ↔ 1 < b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>MulPosReflectLE α<VAR>b0 : 0 < b<GOAL>a * b ≤ b ↔ a ≤ 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>MulPosReflectLT α<VAR>b0 : 0 < b<GOAL>a * b < b ↔ a < 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>hb : 0 ≤ b<VAR>h : a ≤ 1<GOAL>a * b ≤ b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>hb : 0 ≤ b<VAR>h : 1 ≤ a<GOAL>b ≤ a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>h : b ≤ 1<GOAL>a * b ≤ a
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>h : 1 ≤ b<GOAL>a ≤ a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>hb : 0 < b<VAR>h : a < 1<GOAL>a * b < b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>hb : 0 < b<VAR>h : 1 < a<GOAL>b < a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>h : b < 1<GOAL>a * b < a
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>h : 1 < b<GOAL>a < a * b
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : b ≤ c<VAR>ha : a ≤ 1<VAR>hb : 0 ≤ b<GOAL>b * a ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>bc : b ≤ c<VAR>ha : a < 1<VAR>b0 : 0 < b<GOAL>b * a < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : b < c<VAR>ha : a ≤ 1<VAR>hb : 0 ≤ b<GOAL>b * a < c
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<VAR>a0 : 0 ≤ a<GOAL>a * b ≤ 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>ha : a ≤ 1<VAR>hb : b < 1<VAR>a0 : 0 < a<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : a < 1<VAR>hb : b ≤ 1<VAR>a0 : 0 ≤ a<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>bc : b ≤ c<VAR>ha : a ≤ 1<VAR>a0 : 0 ≤ a<VAR>c0 : 0 ≤ c<GOAL>b * a ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>bc : b < c<VAR>ha : a ≤ 1<VAR>a0 : 0 < a<VAR>c0 : 0 ≤ c<GOAL>b * a < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>bc : b ≤ c<VAR>ha : a < 1<VAR>a0 : 0 ≤ a<VAR>c0 : 0 < c<GOAL>b * a < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : b ≤ c<VAR>ha : 1 ≤ a<VAR>hc : 0 ≤ c<GOAL>b ≤ c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>bc : b ≤ c<VAR>ha : 1 < a<VAR>c0 : 0 < c<GOAL>b < c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : b < c<VAR>ha : 1 ≤ a<VAR>hc : 0 ≤ c<GOAL>b < c * a
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<VAR>a0 : 0 ≤ a<GOAL>1 ≤ a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>ha : 1 ≤ a<VAR>hb : 1 < b<VAR>a0 : 0 < a<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>ha : 1 < a<VAR>hb : 1 ≤ b<VAR>a0 : 0 ≤ a<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>bc : b ≤ c<VAR>ha : 1 ≤ a<VAR>a0 : 0 ≤ a<VAR>b0 : 0 ≤ b<GOAL>b ≤ c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>bc : b ≤ c<VAR>ha : 1 < a<VAR>a0 : 0 ≤ a<VAR>b0 : 0 < b<GOAL>b < c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>bc : b < c<VAR>ha : 1 ≤ a<VAR>a0 : 0 < a<VAR>b0 : 0 ≤ b<GOAL>b < c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>bc : b < c<VAR>ha : 1 < a<VAR>a0 : 0 < a<VAR>b0 : 0 < b<GOAL>b < c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>h : b ≤ c<VAR>hb : 0 ≤ b<GOAL>a * b ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : a < 1<VAR>h : b ≤ c<VAR>hb : 0 < b<GOAL>a * b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>h : b < c<VAR>hb : 0 ≤ b<GOAL>a * b < c
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : a < 1<VAR>hb : b ≤ 1<VAR>b0 : 0 < b<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>hb : b < 1<VAR>b0 : 0 ≤ b<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>ha : a < 1<VAR>bc : b < c<VAR>a0 : 0 < a<VAR>c0 : 0 < c<GOAL>a * b < c
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<VAR>b0 : 0 ≤ b<GOAL>a * b ≤ 1
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>bc : b ≤ c<VAR>a0 : 0 ≤ a<VAR>c0 : 0 ≤ c<GOAL>a * b ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>ha : a < 1<VAR>bc : b ≤ c<VAR>a0 : 0 ≤ a<VAR>c0 : 0 < c<GOAL>a * b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>bc : b < c<VAR>a0 : 0 < a<VAR>c0 : 0 ≤ c<GOAL>a * b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : 1 < a<VAR>h : b ≤ c<VAR>hc : 0 < c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : 1 ≤ a<VAR>h : b < c<VAR>hc : 0 ≤ c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : 1 < a<VAR>h : b < c<VAR>hc : 0 < c<GOAL>b < a * c
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : 1 < a<VAR>hb : 1 ≤ b<VAR>b0 : 0 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : 1 ≤ a<VAR>hb : 1 < b<VAR>b0 : 0 ≤ b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : 1 < a<VAR>hb : 1 < b<VAR>b0 : 0 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a * b < c<VAR>hle : 1 ≤ b<VAR>ha : 0 ≤ a<GOAL>a < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a < b * c<VAR>hc : c ≤ 1<VAR>hb : 0 ≤ b<GOAL>a < b
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a < b * c<VAR>hb : b ≤ 1<VAR>hc : 0 ≤ c<GOAL>a < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : 1 ≤ a<VAR>bc : b ≤ c<VAR>c0 : 0 ≤ c<GOAL>b ≤ a * c
<VAR>α : Type u_1<VAR>a b : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<VAR>b0 : 0 ≤ b<GOAL>1 ≤ a * b
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a * b ≤ c<VAR>hb : 1 ≤ b<VAR>ha : 0 ≤ a<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a ≤ b * c<VAR>hc : c ≤ 1<VAR>hb : 0 ≤ b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a * b ≤ c<VAR>ha : 1 ≤ a<VAR>hb : 0 ≤ b<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>MulOneClass α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a ≤ b * c<VAR>hb : b ≤ 1<VAR>hc : 0 ≤ c<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>a : α<VAR>MulOneClass α<VAR>Zero α<VAR>LinearOrder α<VAR>PosMulStrictMono α<VAR>a0 : 0 < a<GOAL>∃ b, b * b ≤ a
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<VAR>PosMulMono α<GOAL>PosMulStrictMono α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<GOAL>PosMulMono α ↔ PosMulStrictMono α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<VAR>MulPosMono α<GOAL>MulPosStrictMono α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<GOAL>MulPosMono α ↔ MulPosStrictMono α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<VAR>PosMulReflectLT α<GOAL>PosMulReflectLE α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<GOAL>PosMulReflectLE α ↔ PosMulReflectLT α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<VAR>MulPosReflectLT α<GOAL>MulPosReflectLE α
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>PartialOrder α<GOAL>MulPosReflectLE α ↔ MulPosReflectLT α
<VAR>α : Type u_1<VAR>Mul α<VAR>IsSymmOp α α fun x x_1 => x * x_1<VAR>Zero α<VAR>Preorder α<GOAL>PosMulStrictMono α ↔ MulPosStrictMono α
<VAR>α : Type u_1<VAR>Mul α<VAR>IsSymmOp α α fun x x_1 => x * x_1<VAR>Zero α<VAR>Preorder α<GOAL>PosMulReflectLT α ↔ MulPosReflectLT α
<VAR>α : Type u_1<VAR>Mul α<VAR>IsSymmOp α α fun x x_1 => x * x_1<VAR>Zero α<VAR>Preorder α<GOAL>PosMulMono α ↔ MulPosMono α
<VAR>α : Type u_1<VAR>Mul α<VAR>IsSymmOp α α fun x x_1 => x * x_1<VAR>Zero α<VAR>Preorder α<GOAL>PosMulReflectLE α ↔ MulPosReflectLE α
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>OrderedSemiring 𝕜<VAR>SMul 𝕜 𝕜'<VAR>a : 𝕜≥0<VAR>x : 𝕜'<GOAL>↑a • x = a • x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>OrderedSemiring 𝕜<VAR>SMul 𝕜 𝕜'<VAR>a : 𝕜<VAR>ha : 0 ≤ a<VAR>x : 𝕜'<GOAL>⟨a, ha⟩ • x = a • x
<VAR>α : Type u_2<VAR>self : LinearOrderedCommMonoidWithZero α<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoidWithZero α<VAR>a : α<GOAL>0 ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoidWithZero α<VAR>a : α<GOAL>¬a < 0
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoidWithZero α<VAR>a : α<GOAL>a ≤ 0 ↔ a = 0
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoidWithZero α<VAR>a : α<GOAL>0 < a ↔ a ≠ 0
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoidWithZero α<VAR>a b : α<VAR>h : b < a<GOAL>a ≠ 0
<VAR>α : Type u_1<VAR>LinearOrderedCommMonoidWithZero α<VAR>a : α<VAR>n : ℕ<VAR>NoZeroDivisors α<VAR>hn : n ≠ 0<GOAL>0 < a ^ n ↔ 0 < a
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<GOAL>a * b ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>1 ≤ a * b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>h : c ≠ 0<VAR>hab : a * c ≤ b * c<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>h : c ≠ 0<VAR>hab : a * c ≤ b<GOAL>a ≤ b * c⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hab : a ≤ b * c<GOAL>a * c⁻¹ ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a ≤ b * c⁻¹ ↔ a * c ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a * c⁻¹ ≤ b ↔ a ≤ b * c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>u : αˣ<GOAL>0 < ↑u
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hb : b ≠ 0<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>h : a < b * c<GOAL>a * c⁻¹ < b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>h : a < b * c<GOAL>b⁻¹ * a < c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b : α<VAR>c : α<VAR>h : a < b<VAR>hc : c ≠ 0<GOAL>a * c < b * c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>1 < a⁻¹ ↔ a < 1
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ < b⁻¹ ↔ b < a
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>h : a * b < c * d<VAR>hc : 0 < c<VAR>hh : c ≤ a<GOAL>b < d
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a * c ≤ b * c ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>ha : a ≠ 0<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a / c ≤ b / c ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<GOAL>a / b ≤ a / c ↔ c ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a ≤ b / c ↔ a * c ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<GOAL>a / c ≤ b ↔ a ≤ b * c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>(OrderIso.mulLeft₀' ha).toEquiv = Equiv.mulLeft₀ a ha
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(OrderIso.mulLeft₀' ha) x = a * x
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>(OrderIso.mulLeft₀' ha).symm = OrderIso.mulLeft₀' ⋯
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>(OrderIso.mulRight₀' ha).toEquiv = Equiv.mulRight₀ a ha
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(OrderIso.mulRight₀' ha) x = x * a
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>(OrderIso.mulRight₀' ha).symm = OrderIso.mulRight₀' ⋯
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>n : ℕ<VAR>ha : 1 < a<GOAL>a ^ n < a ^ n.succ
<VAR>α : Type u_1<VAR>LinearOrderedCommGroupWithZero α<VAR>a : α<VAR>m n : ℕ<VAR>ha : 1 < a<VAR>hmn : m < n<GOAL>a ^ m < a ^ n
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : WithZero α<GOAL>0 ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>0 < ↑a
<VAR>α : Type u_1<VAR>Preorder α<GOAL>0 = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>One α<GOAL>1 < ↑a ↔ 1 < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>One α<GOAL>1 ≤ ↑a ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>One α<GOAL>↑a < 1 ↔ a < 1
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>One α<GOAL>↑a ≤ 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>x : WithZero α<GOAL>↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddZeroClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : ∀ (a : α), 0 ≤ a<GOAL>CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>↑a ≤ max ↑b ↑c ↔ a ≤ max b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>min ↑a ↑b ≤ ↑c ↔ min a b ≤ c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<GOAL>Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f g : R →+* S<VAR>s t : S<VAR>φ ψ : R[X]<GOAL>f = g → s = t → φ = ψ → Polynomial.eval₂ f s φ = Polynomial.eval₂ g t ψ
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>f : R →+* S<GOAL>Polynomial.eval₂ f 0 p = f (p.coeff 0)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a : R<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (Polynomial.C a) = f a
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x Polynomial.X = x
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<VAR>r : R<GOAL>Polynomial.eval₂ f x ((Polynomial.monomial n) r) = f r * x ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<GOAL>Polynomial.eval₂ f x (Polynomial.X ^ n) = x ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p q : R[X]<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x (p + q) = Polynomial.eval₂ f x p + Polynomial.eval₂ f x q
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f x 1 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>g : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>s : R<GOAL>Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>Polynomial.eval₂ Polynomial.C Polynomial.X p = p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<GOAL>(Polynomial.eval₂AddMonoidHom f x) p = Polynomial.eval₂ f x p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<GOAL>Polynomial.eval₂ f x ↑n = ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>S : Type u_1<VAR>Semiring S<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>f : R →+* S<VAR>a : S<GOAL>Polynomial.eval₂ f a (OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>Semiring T<VAR>p : T[X]<VAR>g : ℕ → T → R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x (p.sum g) = p.sum fun n a => Polynomial.eval₂ f x (g n a)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>l : List R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x l.sum = (List.map (Polynomial.eval₂ f x) l).sum
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>s : Multiset R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x s.sum = (Multiset.map (Polynomial.eval₂ f x) s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type y<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>s : Finset ι<VAR>g : ι → R[X]<VAR>x : S<GOAL>Polynomial.eval₂ f x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval₂ f x (g i)