ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>hn : 0 < a<VAR>hm : 1 < b<GOAL>a < a * b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>MulPosStrictMono α<VAR>hn : 1 < a<GOAL>a < a * a
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<GOAL>StrictMono fun x => a * x
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>MulPosStrictMono α<VAR>ha : 0 < a<GOAL>StrictMono fun x => x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>MulPosStrictMono α<VAR>hf : StrictMono f<VAR>ha : 0 < a<GOAL>StrictMono fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>PosMulStrictMono α<VAR>hf : StrictMono f<VAR>ha : 0 < a<GOAL>StrictMono fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>MulPosStrictMono α<VAR>hf : StrictAnti f<VAR>ha : 0 < a<GOAL>StrictAnti fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>PosMulStrictMono α<VAR>hf : StrictAnti f<VAR>ha : 0 < a<GOAL>StrictAnti fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>Preorder β<VAR>f g : β → α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>hf : StrictMono f<VAR>hg : Monotone g<VAR>hf₀ : ∀ (x : β), 0 ≤ f x<VAR>hg₀ : ∀ (x : β), 0 < g x<GOAL>StrictMono (f * g)
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>Preorder β<VAR>f g : β → α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>hf₀ : ∀ (x : β), 0 < f x<VAR>hg₀ : ∀ (x : β), 0 ≤ g x<GOAL>StrictMono (f * g)
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>Preorder β<VAR>f g : β → α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>hf₀ : ∀ (x : β), 0 ≤ f x<VAR>hg₀ : ∀ (x : β), 0 ≤ g x<GOAL>StrictMono (f * g)
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>MulPosStrictMono α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : 0 < a<GOAL>a < 2 * a
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c : α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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>h : b < a<VAR>hc : c < 0<GOAL>c * a < c * b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c : α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>h : b < a<VAR>hc : c < 0<GOAL>a * c < b * c
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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 b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>0 < a * b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>hb : b < 0<VAR>h : a < 1<GOAL>b < a * b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>hb : b < 0<VAR>h : 1 < a<GOAL>a * b < b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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>ha : a < 0<VAR>h : b < 1<GOAL>a < a * b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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>ha : a < 0<VAR>h : 1 < b<GOAL>a * b < a
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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>ha : a < 0<GOAL>StrictAnti fun x => a * x
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>ha : a < 0<GOAL>StrictAnti fun x => x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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>hf : StrictMono f<VAR>ha : a < 0<GOAL>StrictAnti fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>hf : StrictMono f<VAR>ha : a < 0<GOAL>StrictAnti fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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>hf : StrictAnti f<VAR>ha : a < 0<GOAL>StrictMono fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>hf : StrictAnti f<VAR>ha : a < 0<GOAL>StrictMono fun x => f x * a
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<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>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a * d + b * c ≤ a * c + b * d
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<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>hba : b ≤ a<VAR>hdc : d ≤ c<GOAL>a * d + b * c ≤ a * c + b * d
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>hab : a < b<VAR>hcd : c < d<GOAL>a * d + b * c < a * c + b * d
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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>hba : b < a<VAR>hdc : d < c<GOAL>a * d + b * c < a * c + b * d
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>MulPosStrictMono α<VAR>PosMulStrictMono α<VAR>hab : 0 ≤ a * b<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>MulPosStrictMono α<VAR>h : 0 ≤ a * b<VAR>hb : 0 < b<GOAL>0 ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>h : 0 ≤ a * b<VAR>ha : 0 < a<GOAL>0 ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>h : a * b ≤ 0<VAR>hb : 0 < b<GOAL>a ≤ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>h : a * b ≤ 0<VAR>ha : 0 < a<GOAL>b ≤ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>b c : α<VAR>PosMulStrictMono α<VAR>h : 0 < c<GOAL>0 ≤ c * b ↔ 0 ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>b c : α<VAR>MulPosStrictMono α<VAR>h : 0 < c<GOAL>0 ≤ b * c ↔ 0 ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>MulPosStrictMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a2 : 2 ≤ a<VAR>ab : a ≤ b<GOAL>a + b ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>PosMulStrictMono α<VAR>b2 : 2 ≤ b<VAR>ba : b ≤ a<GOAL>a + b ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>MulPosStrictMono α<VAR>PosMulStrictMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a2 : 2 ≤ a<VAR>b2 : 2 ≤ b<GOAL>a + b ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>MulPosStrictMono α<VAR>PosMulStrictMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a2 : 2 ≤ a<VAR>b2 : 2 ≤ b<GOAL>a + b ≤ b * a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<GOAL>0 ≤ a * b ↔ 0 ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>hb : 0 < b<GOAL>0 ≤ a * b ↔ 0 ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>h : 0 ≤ a * b<VAR>hb : b < 0<GOAL>a ≤ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>MulPosStrictMono α<VAR>h : 0 ≤ a * b<VAR>ha : a < 0<GOAL>b ≤ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>PosMulStrictMono α<VAR>u : αˣ<GOAL>0 < ↑u⁻¹ ↔ 0 < ↑u
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>MulPosMono α<VAR>PosMulMono α<VAR>u : αˣ<GOAL>↑u⁻¹ < 0 ↔ ↑u < 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a : α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>b c : α<GOAL>cmp (a * b) (a * c) = cmp b c
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a : α<VAR>MulPosStrictMono α<VAR>ha : 0 < a<VAR>b c : α<GOAL>cmp (b * a) (c * a) = cmp b c
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a : α<VAR>PosMulMono α<VAR>b c : α<VAR>ha : 0 ≤ a<GOAL>a * max b c = max (a * b) (a * c)
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a : α<VAR>PosMulMono α<VAR>b c : α<VAR>ha : 0 ≤ a<GOAL>a * min b c = min (a * b) (a * c)
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>c : α<VAR>MulPosMono α<VAR>a b : α<VAR>hc : 0 ≤ c<GOAL>max a b * c = max (a * c) (b * c)
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>c : α<VAR>MulPosMono α<VAR>a b : α<VAR>hc : 0 ≤ c<GOAL>min a b * c = min (a * c) (b * c)
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>MulPosStrictMono α<VAR>PosMulMono α<VAR>a b c : α<VAR>h : a * c ≤ b<VAR>hb : 0 ≤ b<VAR>hc : 1 ≤ c<GOAL>a ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>a b : α<VAR>hb : 0 ≤ b<VAR>h : a * a ≤ b * b<GOAL>a ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>a b : α<VAR>h1 : 0 ≤ a<VAR>h2 : 0 ≤ b<GOAL>a ≤ b ↔ a * a ≤ b * b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>a b : α<VAR>h1 : 0 ≤ a<VAR>h2 : 0 ≤ b<GOAL>a < b ↔ a * a < b * b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>a b : α<VAR>h1 : 0 ≤ a<VAR>h2 : 0 ≤ b<GOAL>a * a = b * b ↔ a = b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>h : ∀ (n : ℕ), 0 ≤ a * b ^ n<GOAL>a = 0 ∨ 0 < a ∧ 0 ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<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<GOAL>0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<VAR>PosMulStrictMono α<VAR>ContravariantClass α α (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<GOAL>0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<VAR>PosMulStrictMono α<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 b c : α<GOAL>0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<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<GOAL>0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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 b c : α<VAR>h : c < 0<GOAL>c * a ≤ c * b ↔ b ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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 b c : α<VAR>h : c < 0<GOAL>a * c ≤ b * c ↔ b ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<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 b c : α<VAR>h : c < 0<GOAL>c * a < c * b ↔ b < a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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 b c : α<VAR>h : c < 0<GOAL>a * c < b * c ↔ b < a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b c : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<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>h : c * a < c * b<VAR>hc : c ≤ 0<GOAL>b < a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b c : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<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>h : a * c < b * c<VAR>hc : c ≤ 0<GOAL>b < a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<VAR>ContravariantClass α α (Function.swap 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 : α<VAR>ha : a < 0<VAR>b c : α<GOAL>cmp (a * b) (a * c) = cmp c b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<VAR>ContravariantClass α α (Function.swap 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 : α<VAR>ha : a < 0<VAR>b c : α<GOAL>cmp (b * a) (c * a) = cmp c b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<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 : α<GOAL>0 < a * a ↔ a ≠ 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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 b : α<VAR>h : a * b ≤ 0<VAR>hb : b < 0<GOAL>0 ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<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 b : α<VAR>h : a * b ≤ 0<VAR>ha : a < 0<GOAL>0 ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<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 b : α<VAR>h : a * b < 0<VAR>hb : b ≤ 0<GOAL>0 < a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<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 b : α<VAR>h : a * b < 0<VAR>ha : a ≤ 0<GOAL>0 < b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<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>hab : a * b < 0<GOAL>a < 0 ↔ 0 < b
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<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>hab : a * b < 0<GOAL>0 < a ↔ b < 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>IsRightCancelAdd α<VAR>ZeroLEOneClass α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>0 ≤ a ^ 2
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>IsRightCancelAdd α<VAR>ZeroLEOneClass α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>0 ≤ a * a
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>IsRightCancelAdd α<VAR>NoZeroDivisors α<VAR>ZeroLEOneClass α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (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<GOAL>a * a + b * b = 0 ↔ a = 0 ∧ b = 0
<VAR>α : Type u<VAR>Semiring α<VAR>LinearOrder α<VAR>a b : α<VAR>IsRightCancelAdd α<VAR>NoZeroDivisors α<VAR>ZeroLEOneClass α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (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>h : a * a + b * b = 0<GOAL>a = 0
<VAR>α : Type u<VAR>CommSemiring α<VAR>LinearOrder α<VAR>a d : α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>b c : α<VAR>ha : 0 ≤ a<VAR>hd : 0 ≤ d<GOAL>max (a * b) (d * c) ≤ max a c * max d b
<VAR>α : Type u<VAR>CommSemiring α<VAR>LinearOrder α<VAR>ExistsAddOfLE α<VAR>MulPosStrictMono α<VAR>ContravariantClass α α (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>a b : α<GOAL>2 * a * b ≤ a ^ 2 + b ^ 2
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>ContravariantClass α α (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<GOAL>a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<VAR>MulPosStrictMono α<VAR>PosMulStrictMono α<VAR>ContravariantClass α α (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<GOAL>a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<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<GOAL>0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<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<GOAL>a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<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<GOAL>a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>-1 < 0
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<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 - 1 < a
<VAR>α : Type u<VAR>Ring α<VAR>LinearOrder α<VAR>a b : α<VAR>MulPosMono α<VAR>PosMulMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h₁ : a ≤ b<VAR>h₂ : -a ≤ b<GOAL>a * a ≤ b * b
<VAR>Γ : Type u_1<VAR>PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A B : HVertexOperator Γ R V W<VAR>h : ∀ (v : V), A v = B v<GOAL>A = B
<VAR>Γ : Type u_1<VAR>PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>n : Γ<VAR>v : V<GOAL>(A.coeff n) v = ((HahnModule.of R).symm (A v)).coeff n
<VAR>Γ : Type u_1<VAR>PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>v : V<GOAL>(Function.support ((HahnModule.of R).symm (A v)).coeff).IsPWO
<VAR>Γ : Type u_1<VAR>PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<GOAL>Function.Injective HVertexOperator.coeff
<VAR>Γ : Type u_1<VAR>PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>f : Γ → V →ₗ[R] W<VAR>hf : ∀ (x : V), (Function.support fun x_1 => (f x_1) x).IsPWO<VAR>x : V<GOAL>(HVertexOperator.of_coeff f hf) x = (HahnModule.of R) { coeff := fun g => (f g) x, isPWO_support' := ⋯ }
<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>OrderedCancelAddCommMonoid Γ<VAR>OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>AddCommGroup U<VAR>Module R U<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u : U<VAR>g' : Γ'<GOAL>(A.compHahnSeries B u).coeff g' = A ((B.coeff g') u)
<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>OrderedCancelAddCommMonoid Γ<VAR>OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>AddCommGroup U<VAR>Module R U<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u v : U<GOAL>A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v