ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictAntiOn f s<VAR>hg : StrictAntiOn g s<GOAL>StrictAntiOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<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>f g : β → α<VAR>hf : Monotone f<VAR>hg : StrictMono g<GOAL>StrictMono fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<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>f g : β → α<VAR>hf : Monotone f<VAR>hg : StrictMono g<GOAL>StrictMono fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>s : Set β<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>f g : β → α<VAR>hf : MonotoneOn f s<VAR>hg : StrictMonoOn g s<GOAL>StrictMonoOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>s : Set β<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>f g : β → α<VAR>hf : MonotoneOn f s<VAR>hg : StrictMonoOn g s<GOAL>StrictMonoOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<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>f g : β → α<VAR>hf : Antitone f<VAR>hg : StrictAnti g<GOAL>StrictAnti fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<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>f g : β → α<VAR>hf : Antitone f<VAR>hg : StrictAnti g<GOAL>StrictAnti fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>s : Set β<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>f g : β → α<VAR>hf : AntitoneOn f s<VAR>hg : StrictAntiOn g s<GOAL>StrictAntiOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>s : Set β<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>f g : β → α<VAR>hf : AntitoneOn f s<VAR>hg : StrictAntiOn g s<GOAL>StrictAntiOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictMono f<VAR>hg : Monotone g<GOAL>StrictMono fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictMono f<VAR>hg : Monotone g<GOAL>StrictMono fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictMonoOn f s<VAR>hg : MonotoneOn g s<GOAL>StrictMonoOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictMonoOn f s<VAR>hg : MonotoneOn g s<GOAL>StrictMonoOn (fun x => f x + g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictAnti f<VAR>hg : Antitone g<GOAL>StrictAnti fun x => f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<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>hf : StrictAnti f<VAR>hg : Antitone g<GOAL>StrictAnti fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictAntiOn f s<VAR>hg : AntitoneOn g s<GOAL>StrictAntiOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>s : Set β<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>hf : StrictAntiOn f s<VAR>hg : AntitoneOn g s<GOAL>StrictAntiOn (fun x => f x + g x) s
<VAR>α : Type u_3<VAR>Add α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>cmp (a + b) (a + c) = cmp b c
<VAR>α : Type u_3<VAR>Mul α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>cmp (a * b) (a * c) = cmp b c
<VAR>α : Type u_3<VAR>Add α<VAR>LinearOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>cmp (a + c) (b + c) = cmp a b
<VAR>α : Type u_3<VAR>Mul α<VAR>LinearOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>cmp (a * c) (b * c) = cmp a b
<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 : α<GOAL>AddLECancellable a
<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 : α<GOAL>MulLECancellable a
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>LE α<GOAL>AddLECancellable 0
<VAR>α : Type u_1<VAR>Monoid α<VAR>LE α<GOAL>MulLECancellable 1
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>a : α<VAR>ha : AddLECancellable a<GOAL>Function.Injective fun x => a + x
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>a : α<VAR>ha : MulLECancellable a<GOAL>Function.Injective fun x => a * x
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>a b c : α<VAR>ha : AddLECancellable a<GOAL>a + b = a + c ↔ b = c
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>a b c : α<VAR>ha : MulLECancellable a<GOAL>a * b = a * c ↔ b = c
<VAR>α : Type u_1<VAR>Add α<VAR>i : IsSymmOp α α fun x x_1 => x + x_1<VAR>PartialOrder α<VAR>a : α<VAR>ha : AddLECancellable a<GOAL>Function.Injective fun x => x + a
<VAR>α : Type u_1<VAR>Mul α<VAR>i : IsSymmOp α α fun x x_1 => x * x_1<VAR>PartialOrder α<VAR>a : α<VAR>ha : MulLECancellable a<GOAL>Function.Injective fun x => x * a
<VAR>α : Type u_1<VAR>Add α<VAR>IsSymmOp α α fun x x_1 => x + x_1<VAR>PartialOrder α<VAR>a b c : α<VAR>hc : AddLECancellable c<GOAL>a + c = b + c ↔ a = b
<VAR>α : Type u_1<VAR>Mul α<VAR>IsSymmOp α α fun x x_1 => x * x_1<VAR>PartialOrder α<VAR>a b c : α<VAR>hc : MulLECancellable c<GOAL>a * c = b * c ↔ a = b
<VAR>α : Type u_1<VAR>LE α<VAR>Mul α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : MulLECancellable a<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>α : Type u_1<VAR>LE α<VAR>Add α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : AddLECancellable a<GOAL>a + b ≤ a + c ↔ b ≤ c
<VAR>α : Type u_1<VAR>LE α<VAR>Add α<VAR>i : IsSymmOp α α 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 c : α<VAR>ha : AddLECancellable a<GOAL>b + a ≤ c + a ↔ b ≤ c
<VAR>α : Type u_1<VAR>LE α<VAR>Mul α<VAR>i : IsSymmOp α α 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 c : α<VAR>ha : MulLECancellable a<GOAL>b * a ≤ c * a ↔ b ≤ c
<VAR>α : Type u_1<VAR>LE α<VAR>MulOneClass α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : MulLECancellable a<GOAL>a ≤ a * b ↔ 1 ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>AddZeroClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : AddLECancellable a<GOAL>a ≤ a + b ↔ 0 ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>MulOneClass α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : MulLECancellable a<GOAL>a * b ≤ a ↔ b ≤ 1
<VAR>α : Type u_1<VAR>LE α<VAR>AddZeroClass α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : AddLECancellable a<GOAL>a + b ≤ a ↔ b ≤ 0
<VAR>α : Type u_1<VAR>LE α<VAR>AddZeroClass α<VAR>i : IsSymmOp α α 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 : α<VAR>ha : AddLECancellable a<GOAL>a ≤ b + a ↔ 0 ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>MulOneClass α<VAR>i : IsSymmOp α α 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 : α<VAR>ha : MulLECancellable a<GOAL>a ≤ b * a ↔ 1 ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>MulOneClass α<VAR>i : IsSymmOp α α 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 : α<VAR>ha : MulLECancellable a<GOAL>b * a ≤ a ↔ b ≤ 1
<VAR>α : Type u_1<VAR>LE α<VAR>AddZeroClass α<VAR>i : IsSymmOp α α 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 : α<VAR>ha : AddLECancellable a<GOAL>b + a ≤ a ↔ b ≤ 0
<VAR>α : Type u<VAR>Zero α<GOAL>↑0 = 0
<VAR>α : Type u<VAR>One α<GOAL>↑1 = 1
<VAR>α : Type u<VAR>Zero α<VAR>a : α<GOAL>↑a = 0 ↔ a = 0
<VAR>α : Type u<VAR>One α<VAR>a : α<GOAL>↑a = 1 ↔ a = 1
<VAR>α : Type u<VAR>One α<VAR>a : α<GOAL>1 = ↑a ↔ a = 1
<VAR>α : Type u<VAR>Zero α<VAR>a : α<GOAL>0 = ↑a ↔ a = 0
<VAR>α : Type u<VAR>Zero α<GOAL>⊤ ≠ 0
<VAR>α : Type u<VAR>One α<GOAL>⊤ ≠ 1
<VAR>α : Type u<VAR>One α<GOAL>1 ≠ ⊤
<VAR>α : Type u<VAR>Zero α<GOAL>0 ≠ ⊤
<VAR>α : Type u<VAR>One α<GOAL>WithTop.untop 1 ⋯ = 1
<VAR>α : Type u<VAR>Zero α<GOAL>WithTop.untop 0 ⋯ = 0
<VAR>α : Type u<VAR>One α<VAR>d : α<GOAL>WithTop.untop' d 1 = 1
<VAR>α : Type u<VAR>Zero α<VAR>d : α<GOAL>WithTop.untop' d 0 = 0
<VAR>α : Type u<VAR>One α<VAR>LE α<VAR>a : α<GOAL>1 ≤ ↑a ↔ 1 ≤ a
<VAR>α : Type u<VAR>Zero α<VAR>LE α<VAR>a : α<GOAL>0 ≤ ↑a ↔ 0 ≤ a
<VAR>α : Type u<VAR>One α<VAR>LE α<VAR>a : α<GOAL>↑a ≤ 1 ↔ a ≤ 1
<VAR>α : Type u<VAR>Zero α<VAR>LE α<VAR>a : α<GOAL>↑a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u<VAR>Zero α<VAR>LT α<VAR>a : α<GOAL>0 < ↑a ↔ 0 < a
<VAR>α : Type u<VAR>One α<VAR>LT α<VAR>a : α<GOAL>1 < ↑a ↔ 1 < a
<VAR>α : Type u<VAR>One α<VAR>LT α<VAR>a : α<GOAL>↑a < 1 ↔ a < 1
<VAR>α : Type u<VAR>Zero α<VAR>LT α<VAR>a : α<GOAL>↑a < 0 ↔ a < 0
<VAR>α : Type u<VAR>Zero α<VAR>β : Type u_1<VAR>f : α → β<GOAL>WithTop.map f 0 = ↑(f 0)
<VAR>α : Type u<VAR>One α<VAR>β : Type u_1<VAR>f : α → β<GOAL>WithTop.map f 1 = ↑(f 1)
<VAR>α : Type u<VAR>Add α<VAR>a b : α<GOAL>↑(a + b) = ↑a + ↑b
<VAR>α : Type u<VAR>Add α<VAR>a : WithTop α<GOAL>⊤ + a = ⊤
<VAR>α : Type u<VAR>Add α<VAR>a : WithTop α<GOAL>a + ⊤ = ⊤
<VAR>α : Type u<VAR>Add α<VAR>a b : WithTop α<GOAL>a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>α : Type u<VAR>Add α<VAR>a b : WithTop α<GOAL>a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
<VAR>α : Type u<VAR>Add α<VAR>LT α<VAR>a b : WithTop α<GOAL>a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
<VAR>α : Type u<VAR>Add α<VAR>a b : WithTop α<VAR>c : α<GOAL>a + b = ↑c ↔ ∃ a' b', ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
<VAR>α : Type u<VAR>Add α<VAR>x : WithTop α<VAR>y : α<GOAL>x + ↑y = ⊤ ↔ x = ⊤
<VAR>α : Type u<VAR>Add α<VAR>x : α<VAR>y : WithTop α<GOAL>↑x + y = ⊤ ↔ y = ⊤
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>IsRightCancelAdd α<VAR>ha : a ≠ ⊤<GOAL>b + a = c + a ↔ b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>IsRightCancelAdd α<VAR>ha : a ≠ ⊤<VAR>h : b + a = c + a<GOAL>b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>IsLeftCancelAdd α<VAR>ha : a ≠ ⊤<GOAL>a + b = a + c ↔ b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>IsLeftCancelAdd α<VAR>ha : a ≠ ⊤<VAR>h : a + b = a + c<GOAL>b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≠ ⊤<VAR>h : a + b ≤ a + c<GOAL>b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>LE α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≠ ⊤<VAR>h : b + a ≤ c + a<GOAL>b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : a ≠ ⊤<VAR>h : b < c<GOAL>a + b < a + c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : a ≠ ⊤<VAR>h : b < c<GOAL>b + a < c + a
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<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>ha : a ≠ ⊤<GOAL>a + b ≤ a + c ↔ b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<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>ha : a ≠ ⊤<GOAL>b + a ≤ c + a ↔ b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<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>ha : a ≠ ⊤<GOAL>a + b < a + c ↔ b < c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithTop α<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>ha : a ≠ ⊤<GOAL>b + a < c + a ↔ b < c
<VAR>α : Type u<VAR>Add α<VAR>a b c d : WithTop α<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>ha : a ≠ ⊤<VAR>hab : a ≤ b<VAR>hcd : c < d<GOAL>a + c < b + d
<VAR>α : Type u<VAR>Add α<VAR>a b c d : WithTop α<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>hc : c ≠ ⊤<VAR>hab : a < b<VAR>hcd : c ≤ d<GOAL>a + c < b + d
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>F : Type u_1<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>f : F<VAR>a b : WithTop α<GOAL>WithTop.map (⇑f) (a + b) = WithTop.map (⇑f) a + WithTop.map (⇑f) b
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>↑(n • a) = n • ↑a
<VAR>α : Type u<VAR>AddMonoid α<GOAL>⇑WithTop.addHom = WithTop.some
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑n ≠ ⊤
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>⊤ ≠ ↑n
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>m : α<GOAL>↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>m : α<GOAL>OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≠ ⊤
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⊤ ≠ OfNat.ofNat n
<VAR>α : Type u<VAR>Zero α<VAR>LT α<GOAL>0 < ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<GOAL>⇑f.withTopMap = WithTop.map ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>One M<VAR>One N<VAR>f : OneHom M N<GOAL>⇑f.withTopMap = WithTop.map ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>⇑f.withTopMap = WithTop.map ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>⇑f.withTopMap = WithTop.map ⇑f
<VAR>α : Type u<VAR>One α<GOAL>⊥ ≠ 1
<VAR>α : Type u<VAR>Zero α<GOAL>⊥ ≠ 0
<VAR>α : Type u<VAR>Zero α<GOAL>0 ≠ ⊥
<VAR>α : Type u<VAR>One α<GOAL>1 ≠ ⊥
<VAR>α : Type u<VAR>Zero α<GOAL>WithBot.unbot 0 ⋯ = 0
<VAR>α : Type u<VAR>One α<GOAL>WithBot.unbot 1 ⋯ = 1
<VAR>α : Type u<VAR>One α<VAR>d : α<GOAL>WithBot.unbot' d 1 = 1
<VAR>α : Type u<VAR>Zero α<VAR>d : α<GOAL>WithBot.unbot' d 0 = 0
<VAR>α : Type u<VAR>Zero α<VAR>a : α<VAR>LE α<GOAL>0 ≤ ↑a ↔ 0 ≤ a
<VAR>α : Type u<VAR>One α<VAR>a : α<VAR>LE α<GOAL>1 ≤ ↑a ↔ 1 ≤ a
<VAR>α : Type u<VAR>One α<VAR>a : α<VAR>LE α<GOAL>↑a ≤ 1 ↔ a ≤ 1
<VAR>α : Type u<VAR>Zero α<VAR>a : α<VAR>LE α<GOAL>↑a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u<VAR>One α<VAR>a : α<VAR>LT α<GOAL>1 < ↑a ↔ 1 < a
<VAR>α : Type u<VAR>Zero α<VAR>a : α<VAR>LT α<GOAL>0 < ↑a ↔ 0 < a
<VAR>α : Type u<VAR>One α<VAR>a : α<VAR>LT α<GOAL>↑a < 1 ↔ a < 1
<VAR>α : Type u<VAR>Zero α<VAR>a : α<VAR>LT α<GOAL>↑a < 0 ↔ a < 0
<VAR>α : Type u<VAR>One α<VAR>β : Type u_1<VAR>f : α → β<GOAL>WithBot.map f 1 = ↑(f 1)
<VAR>α : Type u<VAR>Zero α<VAR>β : Type u_1<VAR>f : α → β<GOAL>WithBot.map f 0 = ↑(f 0)
<VAR>α : Type u<VAR>AddMonoid α<GOAL>⇑WithBot.addHom = WithBot.some
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑n ≠ ⊥
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>⊥ ≠ ↑n
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≠ ⊥
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⊥ ≠ OfNat.ofNat n
<VAR>α : Type u<VAR>Add α<VAR>a : WithBot α<GOAL>⊥ + a = ⊥
<VAR>α : Type u<VAR>Add α<VAR>a : WithBot α<GOAL>a + ⊥ = ⊥
<VAR>α : Type u<VAR>Add α<VAR>a b : WithBot α<GOAL>a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥
<VAR>α : Type u<VAR>Add α<VAR>a b : WithBot α<GOAL>a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥
<VAR>α : Type u<VAR>Add α<VAR>LT α<VAR>a b : WithBot α<GOAL>⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b
<VAR>α : Type u<VAR>Add α<VAR>a b : WithBot α<VAR>x : α<GOAL>a + b = ↑x ↔ ∃ a' b', ↑a' = a ∧ ↑b' = b ∧ a' + b' = x
<VAR>α : Type u<VAR>Add α<VAR>a : WithBot α<VAR>y : α<GOAL>a + ↑y = ⊥ ↔ a = ⊥
<VAR>α : Type u<VAR>Add α<VAR>b : WithBot α<VAR>x : α<GOAL>↑x + b = ⊥ ↔ b = ⊥
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>IsRightCancelAdd α<VAR>ha : a ≠ ⊥<GOAL>b + a = c + a ↔ b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>IsRightCancelAdd α<VAR>ha : a ≠ ⊥<VAR>h : b + a = c + a<GOAL>b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>IsLeftCancelAdd α<VAR>ha : a ≠ ⊥<GOAL>a + b = a + c ↔ b = c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>IsLeftCancelAdd α<VAR>ha : a ≠ ⊥<VAR>h : a + b = a + c<GOAL>b = c
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>F : Type u_1<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>f : F<VAR>a b : WithBot α<GOAL>WithBot.map (⇑f) (a + b) = WithBot.map (⇑f) a + WithBot.map (⇑f) b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Zero M<VAR>Zero N<VAR>f : ZeroHom M N<GOAL>⇑f.withBotMap = WithBot.map ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>One M<VAR>One N<VAR>f : OneHom M N<GOAL>⇑f.withBotMap = WithBot.map ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>⇑f.withBotMap = WithBot.map ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>⇑f.withBotMap = WithBot.map ⇑f
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≠ ⊥<VAR>h : a + b ≤ a + c<GOAL>b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≠ ⊥<VAR>h : b + a ≤ c + a<GOAL>b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : a ≠ ⊥<VAR>h : b < c<GOAL>a + b < a + c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : a ≠ ⊥<VAR>h : b < c<GOAL>b + a < c + a
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<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>ha : a ≠ ⊥<GOAL>a + b ≤ a + c ↔ b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<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 ≠ ⊥<GOAL>b + a ≤ c + a ↔ b ≤ c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<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>ha : a ≠ ⊥<GOAL>a + b < a + c ↔ b < c
<VAR>α : Type u<VAR>Add α<VAR>a b c : WithBot α<VAR>Preorder α<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 ≠ ⊥<GOAL>b + a < c + a ↔ b < c
<VAR>α : Type u<VAR>Add α<VAR>a b c d : WithBot α<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>hb : b ≠ ⊥<VAR>hab : a ≤ b<VAR>hcd : c < d<GOAL>a + c < b + d
<VAR>α : Type u<VAR>Add α<VAR>a b c d : WithBot α<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>hd : d ≠ ⊥<VAR>hab : a < b<VAR>hcd : c ≤ d<GOAL>a + c < b + d
<VAR>α : Type u_1<VAR>CanonicallyLinearOrderedSemifield α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>(a - b) / c = a / c - b / c
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>0 < a⁻¹ ↔ 0 < a
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>0 ≤ a⁻¹ ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>a⁻¹ < 0 ↔ a < 0
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>a⁻¹ ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>0 < 1 / a ↔ 0 < a
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>1 / a < 0 ↔ a < 0
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>0 ≤ 1 / a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<GOAL>1 / a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a / b
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a b : α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a / b
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a b : α<VAR>MulPosMono α<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a / b ≤ 0
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a b : α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a / b ≤ 0
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<VAR>n : ℤ<GOAL>0 ≤ a ^ n
<VAR>α : Type u_1<VAR>Semifield α<VAR>LinearOrder α<VAR>PosMulReflectLT α<VAR>ZeroLEOneClass α<VAR>a : α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>n : ℤ<GOAL>0 < a ^ n