ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul β α<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>c : β<GOAL>(c • if h : p then a h else b h) = if h : p then c • a h else c • b h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul β α<VAR>p : Prop<VAR>Decidable p<VAR>a : α<VAR>b c : β<GOAL>(if p then b else c) • a = if p then b • a else c • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>p : Prop<VAR>Decidable p<VAR>a : α<VAR>b c : β<GOAL>(a ^ if p then b else c) = if p then a ^ b else a ^ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>c : β<GOAL>(if p then a else b) ^ c = if p then a ^ c else b ^ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul β α<VAR>p : Prop<VAR>Decidable p<VAR>a b : α<VAR>c : β<GOAL>(c • if p then a else b) = if p then c • a else c • b
<VAR>G : Type u_3<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>a : G<GOAL>Function.Injective fun x => a + x
<VAR>G : Type u_3<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>a : G<GOAL>Function.Injective fun x => a * x
<VAR>G : Type u_3<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>a : G<VAR>b c : G<GOAL>a + b = a + c ↔ b = c
<VAR>G : Type u_3<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>a : G<VAR>b c : G<GOAL>a * b = a * c ↔ b = c
<VAR>G : Type u_3<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>a : G<VAR>b c : G<GOAL>a * b ≠ a * c ↔ b ≠ c
<VAR>G : Type u_3<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>a : G<VAR>b c : G<GOAL>a + b ≠ a + c ↔ b ≠ c
<VAR>G : Type u_3<VAR>Add G<VAR>IsRightCancelAdd G<VAR>a : G<GOAL>Function.Injective fun x => x + a
<VAR>G : Type u_3<VAR>Mul G<VAR>IsRightCancelMul G<VAR>a : G<GOAL>Function.Injective fun x => x * a
<VAR>G : Type u_3<VAR>Add G<VAR>IsRightCancelAdd G<VAR>a : G<VAR>b c : G<GOAL>b + a = c + a ↔ b = c
<VAR>G : Type u_3<VAR>Mul G<VAR>IsRightCancelMul G<VAR>a : G<VAR>b c : G<GOAL>b * a = c * a ↔ b = c
<VAR>G : Type u_3<VAR>Add G<VAR>IsRightCancelAdd G<VAR>a : G<VAR>b c : G<GOAL>b + a ≠ c + a ↔ b ≠ c
<VAR>G : Type u_3<VAR>Mul G<VAR>IsRightCancelMul G<VAR>a : G<VAR>b c : G<GOAL>b * a ≠ c * a ↔ b ≠ c
<VAR>α : Type u_1<VAR>AddSemigroup α<VAR>x y : α<GOAL>((fun x_1 => x + x_1) ∘ fun x => y + x) = fun x_1 => x + y + x_1
<VAR>α : Type u_1<VAR>Semigroup α<VAR>x y : α<GOAL>((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1
<VAR>α : Type u_1<VAR>Semigroup α<VAR>x y : α<GOAL>((fun x_1 => x_1 * x) ∘ fun x => x * y) = fun x_1 => x_1 * (y * x)
<VAR>α : Type u_1<VAR>AddSemigroup α<VAR>x y : α<GOAL>((fun x_1 => x_1 + x) ∘ fun x => x + y) = fun x_1 => x_1 + (y + x)
<VAR>M : Type u<VAR>AddZeroClass M<VAR>P : Prop<VAR>Decidable P<VAR>a b : M<GOAL>(if P then a + b else 0) = (if P then a else 0) + if P then b else 0
<VAR>M : Type u<VAR>MulOneClass M<VAR>P : Prop<VAR>Decidable P<VAR>a b : M<GOAL>(if P then a * b else 1) = (if P then a else 1) * if P then b else 1
<VAR>M : Type u<VAR>AddZeroClass M<VAR>P : Prop<VAR>Decidable P<VAR>a b : M<GOAL>(if P then 0 else a + b) = (if P then 0 else a) + if P then 0 else b
<VAR>M : Type u<VAR>MulOneClass M<VAR>P : Prop<VAR>Decidable P<VAR>a b : M<GOAL>(if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
<VAR>M : Type u<VAR>AddZeroClass M<VAR>a b : M<VAR>h : a + b = 0<GOAL>a = 0 ↔ b = 0
<VAR>M : Type u<VAR>MulOneClass M<VAR>a b : M<VAR>h : a * b = 1<GOAL>a = 1 ↔ b = 1
<VAR>M : Type u<VAR>AddZeroClass M<GOAL>(fun x => 0 + x) = id
<VAR>M : Type u<VAR>MulOneClass M<GOAL>(fun x => 1 * x) = id
<VAR>M : Type u<VAR>MulOneClass M<GOAL>(fun x => x * 1) = id
<VAR>M : Type u<VAR>AddZeroClass M<GOAL>(fun x => x + 0) = id
<VAR>G : Type u_3<VAR>AddCommSemigroup G<VAR>a b c : G<GOAL>a + (b + c) = b + (a + c)
<VAR>G : Type u_3<VAR>CommSemigroup G<VAR>a b c : G<GOAL>a * (b * c) = b * (a * c)
<VAR>G : Type u_3<VAR>CommSemigroup G<VAR>a b c : G<GOAL>a * b * c = a * c * b
<VAR>G : Type u_3<VAR>AddCommSemigroup G<VAR>a b c : G<GOAL>a + b + c = a + c + b
<VAR>G : Type u_3<VAR>CommSemigroup G<VAR>a b c d : G<GOAL>a * b * (c * d) = a * c * (b * d)
<VAR>G : Type u_3<VAR>AddCommSemigroup G<VAR>a b c d : G<GOAL>a + b + (c + d) = a + c + (b + d)
<VAR>G : Type u_3<VAR>AddCommSemigroup G<VAR>a b c : G<GOAL>a + b + c = b + c + a
<VAR>G : Type u_3<VAR>CommSemigroup G<VAR>a b c : G<GOAL>a * b * c = b * c * a
<VAR>G : Type u_3<VAR>CommSemigroup G<VAR>a b c : G<GOAL>a * (b * c) = b * (c * a)
<VAR>G : Type u_3<VAR>AddCommSemigroup G<VAR>a b c : G<GOAL>a + (b + c) = b + (c + a)
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>P : Prop<VAR>Decidable P<VAR>a : M<GOAL>(if P then 1 else 0) • a = if P then a else 0
<VAR>M : Type u_4<VAR>Monoid M<VAR>P : Prop<VAR>Decidable P<VAR>a : M<GOAL>(a ^ if P then 1 else 0) = if P then a else 1
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>m n : ℕ<VAR>a : M<VAR>h : m ≤ n<GOAL>m • a + (n - m) • a = n • a
<VAR>M : Type u_4<VAR>Monoid M<VAR>m n : ℕ<VAR>a : M<VAR>h : m ≤ n<GOAL>a ^ m * a ^ (n - m) = a ^ n
<VAR>M : Type u_4<VAR>Monoid M<VAR>m n : ℕ<VAR>a : M<VAR>h : m ≤ n<GOAL>a ^ (n - m) * a ^ m = a ^ n
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>m n : ℕ<VAR>a : M<VAR>h : m ≤ n<GOAL>(n - m) • a + m • a = n • a
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : M<GOAL>a + (n - 1) • a = n • a
<VAR>M : Type u_4<VAR>Monoid M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : M<GOAL>a * a ^ (n - 1) = a ^ n
<VAR>M : Type u_4<VAR>Monoid M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : M<GOAL>a ^ (n - 1) * a = a ^ n
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : M<GOAL>(n - 1) • a + a = n • a
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<VAR>m : ℕ<VAR>ha : n • a = 0<GOAL>m • a = (m % n) • a
<VAR>M : Type u_4<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<VAR>m : ℕ<VAR>ha : a ^ n = 1<GOAL>a ^ m = a ^ (m % n)
<VAR>M : Type u_4<VAR>Monoid M<VAR>a b : M<VAR>n : ℕ<GOAL>a * b = 1 → a ^ n * b ^ n = 1
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>a b : M<VAR>n : ℕ<GOAL>a + b = 0 → n • a + n • b = 0
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>x y z : M<VAR>hy : x * y = 1<VAR>hz : x * z = 1<GOAL>y = z
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>x y z : M<VAR>hy : x + y = 0<VAR>hz : x + z = 0<GOAL>y = z
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>a b : M<VAR>n : ℕ<GOAL>(a * b) ^ n = a ^ n * b ^ n
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>a b : M<VAR>n : ℕ<GOAL>n • (a + b) = n • a + n • b
<VAR>M : Type u<VAR>LeftCancelMonoid M<VAR>a b : M<GOAL>a * b = a ↔ b = 1
<VAR>M : Type u<VAR>AddLeftCancelMonoid M<VAR>a b : M<GOAL>a + b = a ↔ b = 0
<VAR>M : Type u<VAR>LeftCancelMonoid M<VAR>a b : M<GOAL>a = a * b ↔ b = 1
<VAR>M : Type u<VAR>AddLeftCancelMonoid M<VAR>a b : M<GOAL>a = a + b ↔ b = 0
<VAR>M : Type u<VAR>LeftCancelMonoid M<VAR>a b : M<GOAL>a * b ≠ a ↔ b ≠ 1
<VAR>M : Type u<VAR>AddLeftCancelMonoid M<VAR>a b : M<GOAL>a + b ≠ a ↔ b ≠ 0
<VAR>M : Type u<VAR>AddLeftCancelMonoid M<VAR>a b : M<GOAL>a ≠ a + b ↔ b ≠ 0
<VAR>M : Type u<VAR>LeftCancelMonoid M<VAR>a b : M<GOAL>a ≠ a * b ↔ b ≠ 1
<VAR>M : Type u<VAR>RightCancelMonoid M<VAR>a b : M<GOAL>a * b = b ↔ a = 1
<VAR>M : Type u<VAR>AddRightCancelMonoid M<VAR>a b : M<GOAL>a + b = b ↔ a = 0
<VAR>M : Type u<VAR>AddRightCancelMonoid M<VAR>a b : M<GOAL>b = a + b ↔ a = 0
<VAR>M : Type u<VAR>RightCancelMonoid M<VAR>a b : M<GOAL>b = a * b ↔ a = 1
<VAR>M : Type u<VAR>RightCancelMonoid M<VAR>a b : M<GOAL>a * b ≠ b ↔ a ≠ 1
<VAR>M : Type u<VAR>AddRightCancelMonoid M<VAR>a b : M<GOAL>a + b ≠ b ↔ a ≠ 0
<VAR>M : Type u<VAR>AddRightCancelMonoid M<VAR>a b : M<GOAL>b ≠ a + b ↔ a ≠ 0
<VAR>M : Type u<VAR>RightCancelMonoid M<VAR>a b : M<GOAL>b ≠ a * b ↔ a ≠ 1
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>a b c d : α<VAR>h : a + b = c + d<GOAL>a = c ↔ b = d
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>a b c d : α<VAR>h : a * b = c * d<GOAL>a = c ↔ b = d
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>a b c d : α<VAR>h : a + b = c + d<GOAL>a ≠ c ↔ b ≠ d
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>a b c d : α<VAR>h : a * b = c * d<GOAL>a ≠ c ↔ b ≠ d
<VAR>G : Type u_3<VAR>InvolutiveInv G<GOAL>Function.Involutive Inv.inv
<VAR>G : Type u_3<VAR>InvolutiveNeg G<GOAL>Function.Involutive Neg.neg
<VAR>G : Type u_3<VAR>InvolutiveInv G<GOAL>Function.Surjective Inv.inv
<VAR>G : Type u_3<VAR>InvolutiveNeg G<GOAL>Function.Surjective Neg.neg
<VAR>G : Type u_3<VAR>InvolutiveNeg G<GOAL>Function.Injective Neg.neg
<VAR>G : Type u_3<VAR>InvolutiveInv G<GOAL>Function.Injective Inv.inv
<VAR>G : Type u_3<VAR>InvolutiveNeg G<VAR>a b : G<GOAL>-a = -b ↔ a = b
<VAR>G : Type u_3<VAR>InvolutiveInv G<VAR>a b : G<GOAL>a⁻¹ = b⁻¹ ↔ a = b
<VAR>G : Type u_3<VAR>InvolutiveInv G<VAR>a b : G<GOAL>a⁻¹ = b ↔ a = b⁻¹
<VAR>G : Type u_3<VAR>InvolutiveNeg G<VAR>a b : G<GOAL>-a = b ↔ a = -b
<VAR>G : Type u_3<VAR>InvolutiveInv G<GOAL>Inv.inv ∘ Inv.inv = id
<VAR>G : Type u_3<VAR>InvolutiveNeg G<GOAL>Neg.neg ∘ Neg.neg = id
<VAR>G : Type u_3<VAR>InvolutiveInv G<GOAL>Function.LeftInverse (fun a => a⁻¹) fun a => a⁻¹
<VAR>G : Type u_3<VAR>InvolutiveNeg G<GOAL>Function.LeftInverse (fun a => -a) fun a => -a
<VAR>G : Type u_3<VAR>InvolutiveNeg G<GOAL>Function.RightInverse (fun a => -a) fun a => -a
<VAR>G : Type u_3<VAR>InvolutiveInv G<GOAL>Function.RightInverse (fun a => a⁻¹) fun a => a⁻¹
<VAR>G : Type u_3<VAR>SubNegMonoid G<VAR>x : G<GOAL>-x = 0 - x
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x : G<GOAL>x⁻¹ = 1 / x
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>x y : G<GOAL>x * (1 / y) = x / y
<VAR>G : Type u_3<VAR>SubNegMonoid G<VAR>x y : G<GOAL>x + (0 - y) = x - y
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>a b c : G<GOAL>a * b / c = a * (b / c)
<VAR>G : Type u_3<VAR>SubNegMonoid G<VAR>a b c : G<GOAL>a + b - c = a + (b - c)
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>a b c : G<GOAL>a * (b / c) = a * b / c
<VAR>G : Type u_3<VAR>SubNegMonoid G<VAR>a b c : G<GOAL>a + (b - c) = a + b - c
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>a : G<GOAL>1 / a = a⁻¹
<VAR>G : Type u_3<VAR>SubNegMonoid G<VAR>a : G<GOAL>0 - a = -a
<VAR>G : Type u_3<VAR>SubNegMonoid G<VAR>a b : G<GOAL>a - b = a + (0 - b)
<VAR>G : Type u_3<VAR>DivInvMonoid G<VAR>a b : G<GOAL>a / b = a * (1 / b)
<VAR>G : Type u_3<VAR>SubNegZeroMonoid G<VAR>a : G<GOAL>a - 0 = a
<VAR>G : Type u_3<VAR>DivInvOneMonoid G<VAR>a : G<GOAL>a / 1 = a
<VAR>G : Type u_3<VAR>DivInvOneMonoid G<GOAL>1 / 1 = 1
<VAR>G : Type u_3<VAR>SubNegZeroMonoid G<GOAL>0 - 0 = 0
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : a * b = 1<GOAL>b = a⁻¹
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : a + b = 0<GOAL>b = -a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : b * a = 1<GOAL>b = 1 / a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : b + a = 0<GOAL>b = 0 - a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : a * b = 1<GOAL>b = 1 / a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : a + b = 0<GOAL>b = 0 - a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : a / b = 1<GOAL>a = b
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : a - b = 0<GOAL>a = b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : a⁻¹ * b = 1<GOAL>a = b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : a * b⁻¹ = 1<GOAL>a = b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>a ≠ b → a / b ≠ 1
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>a ≠ b → a - b ≠ 0
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>0 - a + (0 - b) = 0 - (b + a)
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>1 / a * (1 / b) = 1 / (b * a)
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>-a - b = -(b + a)
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>a⁻¹ / b = (b * a)⁻¹
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>(a / b)⁻¹ = b / a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>-(a - b) = b - a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>1 / (a / b) = b / a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>0 - (a - b) = b - a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<GOAL>1 / (1 / a) = a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<GOAL>0 - (0 - a) = a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b c : α<VAR>d : α<GOAL>a / b = c / d ↔ b / a = d / c
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>d : α<GOAL>a - b = c - d ↔ b - a = d - c
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>n • -a = -(n • a)
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>a⁻¹ ^ n = (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>n : ℤ<GOAL>n • 0 = 0
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>n : ℤ<GOAL>1 ^ n = 1
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>-n • a = -(n • a)
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>a ^ (-n) = (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>-1 • (a + b) = -1 • b + -1 • a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>(a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>n • -a = -(n • a)
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>a⁻¹ ^ n = (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>a⁻¹ ^ n = a ^ (-n)
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>n • -a = -n • a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>n • (0 - a) = 0 - n • a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>(1 / a) ^ n = 1 / a ^ n
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>(1 / a) ^ n = 1 / a ^ n
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>n • (0 - a) = 0 - n • a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<GOAL>a⁻¹ = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<GOAL>-a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<GOAL>1 = a⁻¹ ↔ a = 1
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<GOAL>0 = -a ↔ a = 0
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<GOAL>a⁻¹ ≠ 1 ↔ a ≠ 1
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<GOAL>-a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : 0 - a = 0 - b<GOAL>a = b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : 1 / a = 1 / b<GOAL>a = b
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>m n : ℤ<GOAL>(m * n) • a = n • m • a
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>m n : ℤ<GOAL>a ^ (m * n) = (a ^ m) ^ n
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a : α<VAR>m n : ℤ<GOAL>a ^ (m * n) = (a ^ n) ^ m
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a : α<VAR>m n : ℤ<GOAL>(m * n) • a = m • n • a
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b c : α<GOAL>a - (b - c) = a + c - b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b c : α<GOAL>a / (b / c) = a * c / b
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b : α<GOAL>a - -b = a + b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b : α<GOAL>a / b⁻¹ = a * b
<VAR>α : Type u_1<VAR>SubtractionMonoid α<VAR>a b c : α<GOAL>a - (b + c) = a - c - b
<VAR>α : Type u_1<VAR>DivisionMonoid α<VAR>a b c : α<GOAL>a / (b * c) = a / c / b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>-(a + b) = -a + -b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>(a * b)⁻¹ = a⁻¹ * b⁻¹
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>-(a - b) = -a - -b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>(a / b)⁻¹ = a⁻¹ / b⁻¹
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>a - b = -b + a
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>a / b = b⁻¹ * a
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>-a + b = b - a
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>a⁻¹ * b = b / a
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>(a * b)⁻¹ = a⁻¹ / b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>-(a + b) = -a - b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>-a - -b = b - a
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>a⁻¹ / b⁻¹ = b / a
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>-(-a - -b) = a - b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>(a⁻¹ / b⁻¹)⁻¹ = a / b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>0 - a + (0 - b) = 0 - (a + b)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>1 / a * (1 / b) = 1 / (a * b)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - b - c = a - c - b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / b / c = a / c / b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / b / c = a / (b * c)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - b - c = a - (b + c)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / b * c = a / (b / c)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - b + c = a - (b - c)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a * (b / c) = b * (a / c)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a + (b - c) = b + (a - c)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a * b / c = a / c * b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a + b - c = a - c + b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / (b * c) = a / b / c
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - (b + c) = a - b - c
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / b * c = a * c / b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - b + c = a + c - b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<GOAL>0 - a + b = b - a
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<GOAL>1 / a * b = b / a
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / b * c = a * (c / b)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - b + c = a + (c - b)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / b * c = c / b * a
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - b + c = c - b + a
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c : α<GOAL>a - (b + c) = a - b + (0 - c)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c : α<GOAL>a / (b * c) = a / b * (1 / c)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c d : α<GOAL>a - b - (c - d) = a + d - (b + c)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c d : α<GOAL>a / b / (c / d) = a * d / (b * c)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c d : α<GOAL>a - b - (c - d) = a - c - (b - d)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c d : α<GOAL>a / b / (c / d) = a / c / (b / d)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c d : α<GOAL>a / b * (c / d) = a * c / (b * d)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c d : α<GOAL>a - b + (c - d) = a + c - (b + d)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b c d : α<GOAL>a * b / (c * d) = a / c * (b / d)
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b c d : α<GOAL>a + b - (c + d) = a - c + (b - d)
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<VAR>n : ℤ<GOAL>(a * b) ^ n = a ^ n * b ^ n
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<VAR>n : ℤ<GOAL>n • (a + b) = n • a + n • b
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<VAR>n : ℕ<GOAL>n • (a - b) = n • a - n • b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<VAR>n : ℕ<GOAL>(a / b) ^ n = a ^ n / b ^ n
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>a b : α<VAR>n : ℤ<GOAL>n • (a - b) = n • a - n • b
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a b : α<VAR>n : ℤ<GOAL>(a / b) ^ n = a ^ n / b ^ n
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a - b = -b ↔ a = 0
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a / b = b⁻¹ ↔ a = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<GOAL>Function.Surjective fun x => a + x
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<GOAL>Function.Surjective fun x => a * x
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<GOAL>Function.Surjective fun x => x * a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<GOAL>Function.Surjective fun x => x + a
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a * c = b<GOAL>a = b * c⁻¹
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a + c = b<GOAL>a = b + -c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : b * a = c<GOAL>a = b⁻¹ * c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : b + a = c<GOAL>a = -b + c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : b = a * c<GOAL>a⁻¹ * b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : b = a + c<GOAL>-a + b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a = c * b<GOAL>a * b⁻¹ = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a = c + b<GOAL>a + -b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a + -c = b<GOAL>a = b + c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a * c⁻¹ = b<GOAL>a = b * c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : b⁻¹ * a = c<GOAL>a = b * c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : -b + a = c<GOAL>a = b + c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : b = -a + c<GOAL>a + b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : b = a⁻¹ * c<GOAL>a * b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a = c + -b<GOAL>a + b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a = c * b⁻¹<GOAL>a * b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a + b = 0 ↔ a = -b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a * b = 1 ↔ a = b⁻¹
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a * b = 1 ↔ a⁻¹ = b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a + b = 0 ↔ -a = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a = b⁻¹ ↔ a * b = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a = -b ↔ a + b = 0
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a⁻¹ = b ↔ a * b = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>-a = b ↔ a + b = 0
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a = b + -c ↔ a + c = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a = b * c⁻¹ ↔ a * c = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a = b⁻¹ * c ↔ b * a = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a = -b + c ↔ b + a = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>-a + b = c ↔ b = a + c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a⁻¹ * b = c ↔ b = a * c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a * b⁻¹ = c ↔ a = c * b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a + -b = c ↔ a = c + b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a * b⁻¹ = 1 ↔ a = b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a + -b = 0 ↔ a = b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>-a + b = 0 ↔ a = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a⁻¹ * b = 1 ↔ a = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a * b * a⁻¹ = 1 ↔ b = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a + b + -a = 0 ↔ b = 0
<VAR>G : Type u_3<VAR>AddGroup G<VAR>b : G<GOAL>Function.Injective fun a => a - b
<VAR>G : Type u_3<VAR>Group G<VAR>b : G<GOAL>Function.Injective fun a => a / b
<VAR>G : Type u_3<VAR>Group G<VAR>b : G<GOAL>Function.Injective fun a => b / a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>b : G<GOAL>Function.Injective fun a => b - a
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a / b * b = a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a - b + b = a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<GOAL>a / a = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<GOAL>a - a = 0
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a * b / b = a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a + b - b = a
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a / (b * a) = b⁻¹
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a - (b + a) = -b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a + c - (b + c) = a - b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a * c / (b * c) = a / b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a * c = b<GOAL>a = b / c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a + c = b<GOAL>a = b - c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a = c + b<GOAL>a - b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a = c * b<GOAL>a / b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a / c = b<GOAL>a = b * c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a - c = b<GOAL>a = b + c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<VAR>h : a = c / b<GOAL>a * b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<VAR>h : a = c - b<GOAL>a + b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a / b = a / c ↔ b = c