ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<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 : α<GOAL>a⁺ᵐ * a⁻ᵐ = mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<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 : α<GOAL>a⁻ᵐ * a⁺ᵐ = mabs a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<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 : α<GOAL>a⁻ + a⁺ = |a|
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<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 : α<GOAL>a⁺ᵐ ⊓ a⁻ᵐ = 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<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 : α<GOAL>a⁺ ⊓ a⁻ = 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊔ b = b * (a / b)⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊔ b = b + (a - b)⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊓ b = a - (a - b)⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊓ b = a / (a / b)⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>mabs a * a = a⁺ᵐ ^ 2
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>|a| + a = 2 • a⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a + |a| = 2 • a⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a * mabs a = a⁺ᵐ ^ 2
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>mabs a / a = a⁻ᵐ ^ 2
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>|a| - a = 2 • a⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a / mabs a = (a⁻ᵐ ^ 2)⁻¹
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a - |a| = -(2 • a⁻)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddGroup α<VAR>a : α<GOAL>a⁺ = if 0 ≤ a then a else 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Group α<VAR>a : α<GOAL>a⁺ᵐ = if 1 ≤ a then a else 1
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Group α<VAR>a : α<GOAL>1 < a⁺ᵐ ↔ 1 < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddGroup α<VAR>a : α<GOAL>0 < a⁺ ↔ 0 < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddGroup α<VAR>a : α<VAR>ha : 0 < a⁺<GOAL>a⁺ = a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Group α<VAR>a : α<VAR>ha : 1 < a⁺ᵐ <GOAL>a⁺ᵐ = a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ = if a ≤ 0 then -a else 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < a⁻ ↔ a < 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>1 < a⁻ᵐ ↔ a < 1
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → AddCommGroup (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<GOAL>f⁺ i = (f i)⁺
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → AddCommGroup (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<GOAL>f⁻ i = (f i)⁻
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → AddCommGroup (α i)<VAR>f : (i : ι) → α i<GOAL>f⁺ = fun i => (f i)⁺
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → AddCommGroup (α i)<VAR>f : (i : ι) → α i<GOAL>f⁻ = fun i => (f i)⁻
<VAR>a b : ℤ<VAR>hb : 0 < b<GOAL>0 ≤ Rat.divInt a b ↔ 0 ≤ a
<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ Rat.divInt a b
<VAR>a : ℤ<VAR>ha : 0 ≤ a<VAR>b : ℕ<GOAL>0 ≤ mkRat a b
<VAR>m : ℕ<VAR>s : Bool<VAR>e : ℕ<GOAL>0 ≤ Rat.ofScientific m s e
<VAR>K : Type u_1<VAR>NNRatCast K<VAR>m : ℕ<VAR>s : Bool<VAR>e : ℕ<GOAL>↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
<VAR>a b : ℚ<GOAL>0 ≤ a → 0 ≤ b → 0 ≤ a + b
<VAR>a b : ℚ<GOAL>0 ≤ a → 0 ≤ b → 0 ≤ a * b
<VAR>a b : ℚ<GOAL>a ≤ b ↔ 0 ≤ b - a
<VAR>a b c d : ℤ<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>Rat.divInt a b ≤ Rat.divInt c d ↔ a * d ≤ c * b
<VAR>a b : ℚ<GOAL>a ≤ b ∨ b ≤ a
<VAR>a b : ℚ<GOAL>¬a ≤ b ↔ b < a
<VAR>p q : ℚ<GOAL>p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den
<VAR>p q : ℚ<GOAL>p < q ↔ p.num * ↑q.den < q.num * ↑p.den
<VAR>a b c : ℚ<GOAL>c + a ≤ c + b ↔ a ≤ b
<VAR>a : ℚ<GOAL>a.num ≤ 0 ↔ a ≤ 0
<VAR>a : ℚ<GOAL>0 < a.num ↔ 0 < a
<VAR>a : ℚ<GOAL>a.num < 0 ↔ a < 0
<VAR>a b c d : ℤ<VAR>b_pos : 0 < b<VAR>d_pos : 0 < d<GOAL>↑a / ↑b < ↑c / ↑d ↔ a * d < c * b
<VAR>q : ℚ<GOAL>q < 1 ↔ q.num < ↑q.den
<VAR>q : ℚ<GOAL>|q| = Rat.divInt ↑q.num.natAbs ↑q.den
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<GOAL>Monotone Int.cast
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<VAR>n : ℤ<GOAL>0 ≤ ↑n ↔ 0 ≤ n
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<VAR>m n : ℤ<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<GOAL>StrictMono fun x => ↑x
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<VAR>m n : ℤ<GOAL>↑m < ↑n ↔ m < n
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<VAR>n : ℤ<GOAL>↑n ≤ 0 ↔ n ≤ 0
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<VAR>n : ℤ<GOAL>0 < ↑n ↔ 0 < n
<VAR>R : Type u_1<VAR>AddCommGroupWithOne R<VAR>PartialOrder R<VAR>CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass R<VAR>NeZero 1<VAR>n : ℤ<GOAL>↑n < 0 ↔ n < 0
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a b : ℤ<GOAL>↑(min a b) = min ↑a ↑b
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a b : ℤ<GOAL>↑(max a b) = max ↑a ↑b
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a : ℤ<GOAL>↑|a| = |↑a|
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a : ℤ<VAR>h : 0 < a<GOAL>1 ≤ ↑a
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>a : ℤ<VAR>h : a < 0<GOAL>↑a ≤ -1
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>↑n ≤ -1 ∨ 1 ≤ ↑n
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>x : R<VAR>n : ℤ<VAR>hx : |x| ≤ 1<GOAL>0 ≤ ↑n * x + ↑n * ↑n
<VAR>R : Type u_1<VAR>LinearOrderedRing R<VAR>n : ℤ<GOAL>↑n.natAbs = ↑|n|
<VAR>R : Type u_1<VAR>IntCast R<VAR>n : ℤ<GOAL>OrderDual.toDual ↑n = ↑n
<VAR>R : Type u_1<VAR>IntCast R<VAR>n : ℤ<GOAL>OrderDual.ofDual ↑n = ↑n
<VAR>R : Type u_1<VAR>IntCast R<VAR>n : ℤ<GOAL>toLex ↑n = ↑n
<VAR>R : Type u_1<VAR>IntCast R<VAR>n : ℤ<GOAL>ofLex ↑n = ↑n
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>-a ≤ 0 ↔ 0 ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>0 ≤ -a ↔ a ≤ 0
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b ≤ a⁻¹ * c ↔ a * b ≤ c
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b ≤ -a + c ↔ a + b ≤ c
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>-b + a ≤ c ↔ a ≤ b + c
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b⁻¹ * a ≤ c ↔ a ≤ b * c
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a⁻¹ ≤ b ↔ 1 ≤ a * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>-a ≤ b ↔ 0 ≤ a + b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b⁻¹ ↔ b * a ≤ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ -b ↔ b + a ≤ 0
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>0 ≤ -b + a ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>1 ≤ b⁻¹ * a ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a⁻¹ * b ≤ 1 ↔ b ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>-a + b ≤ 0 ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>1 < a⁻¹ ↔ a < 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>0 < -a ↔ a < 0
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>-a < 0 ↔ 0 < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b < -a + c ↔ a + b < c
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b < a⁻¹ * c ↔ a * b < c
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b⁻¹ * a < c ↔ a < b * c
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>-b + a < c ↔ a < b + c
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>-a < b ↔ 0 < a + b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a⁻¹ < b ↔ 1 < a * b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a < b⁻¹ ↔ b * a < 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a < -b ↔ b + a < 0
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>0 < -b + a ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>1 < b⁻¹ * a ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a⁻¹ * b < 1 ↔ b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>-a + b < 0 ↔ b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>-a ≤ 0 ↔ 0 ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>0 ≤ -a ↔ a ≤ 0
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a⁻¹ ≤ b ↔ 1 ≤ b * a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>-a ≤ b ↔ 0 ≤ b + a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ -b ↔ a + b ≤ 0
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b⁻¹ ↔ a * b ≤ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a + -b ≤ c ↔ a ≤ c + b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a * b⁻¹ ≤ c ↔ a ≤ c * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>c ≤ a + -b ↔ c + b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>c ≤ a * b⁻¹ ↔ c * b ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a + -b ≤ 0 ↔ a ≤ b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a * b⁻¹ ≤ 1 ↔ a ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>0 ≤ a + -b ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>1 ≤ a * b⁻¹ ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>b * a⁻¹ ≤ 1 ↔ b ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>b + -a ≤ 0 ↔ b ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>-a < 0 ↔ 0 < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>0 < -a ↔ a < 0
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>1 < a⁻¹ ↔ a < 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>-a < b ↔ 0 < b + a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a⁻¹ < b ↔ 1 < b * a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a < b⁻¹ ↔ a * b < 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a < -b ↔ a + b < 0
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a + -b < c ↔ a < c + b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a * b⁻¹ < c ↔ a < c * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>c < a + -b ↔ c + b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>c < a * b⁻¹ ↔ c * b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a + -b < 0 ↔ a < b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a * b⁻¹ < 1 ↔ a < b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>0 < a + -b ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>1 < a * b⁻¹ ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>b * a⁻¹ < 1 ↔ b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>b + -a < 0 ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LE α<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 : α<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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 : α<GOAL>-a ≤ -b ↔ b ≤ a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a + -b ≤ -d + c ↔ d + a ≤ c + b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a / b ≤ a ↔ 1 ≤ b
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a - b ≤ a ↔ 0 ≤ b
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a ≤ a / b ↔ b ≤ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a ≤ a - b ↔ b ≤ 0
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<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 : α<GOAL>-a < -b ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<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 : α<GOAL>a⁻¹ < b⁻¹ ↔ b < a
<VAR>α : Type u<VAR>Group α<VAR>LT α<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 : α<GOAL>a⁻¹ < b ↔ b⁻¹ < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<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 : α<GOAL>-a < b ↔ -b < a
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<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 : α<GOAL>a < -b ↔ b < -a
<VAR>α : Type u<VAR>Group α<VAR>LT α<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 : α<GOAL>a < b⁻¹ ↔ b < a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a + -b < -d + c ↔ d + a < c + b
<VAR>α : Type u<VAR>AddGroup α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a - b < a ↔ 0 < b
<VAR>α : Type u<VAR>Group α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a / b < a ↔ 1 < b
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : 0 ≤ a<GOAL>-a ≤ a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : 1 ≤ a<GOAL>a⁻¹ ≤ a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : a ≤ 1<GOAL>a ≤ a⁻¹
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : a ≤ 0<GOAL>a ≤ -a
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : 0 < a<GOAL>-a < a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : 1 < a<GOAL>a⁻¹ < a
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : a < 0<GOAL>a < -a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : a < 1<GOAL>a < a⁻¹
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : 0 ≤ a<GOAL>-a ≤ a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : 1 ≤ a<GOAL>a⁻¹ ≤ a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : a ≤ 1<GOAL>a ≤ a⁻¹
<VAR>α : Type u<VAR>AddGroup α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : a ≤ 0<GOAL>a ≤ -a
<VAR>α : Type u<VAR>Group α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>h : 1 < a<GOAL>a⁻¹ < a