ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>Monoid α<VAR>self : αˣ<GOAL>↑self * self.inv = 1
<VAR>α : Type u<VAR>Monoid α<VAR>self : αˣ<GOAL>self.inv * ↑self = 1
<VAR>α : Type u<VAR>AddMonoid α<VAR>self : AddUnits α<GOAL>↑self + self.neg = 0
<VAR>α : Type u<VAR>AddMonoid α<VAR>self : AddUnits α<GOAL>self.neg + ↑self = 0
<VAR>α : Type u_1<VAR>Unique α<VAR>Zero α<GOAL>default = 0
<VAR>α : Type u_1<VAR>Unique α<VAR>One α<GOAL>default = 1
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>h₁ : a * b = 1<VAR>h₂ : b * a = 1<GOAL>↑{ val := a, inv := b, val_inv := h₁, inv_val := h₂ } = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>a b : α<VAR>h₁ : a + b = 0<VAR>h₂ : b + a = 0<GOAL>↑{ val := a, neg := b, val_neg := h₁, neg_val := h₂ } = a
<VAR>α : Type u<VAR>Monoid α<GOAL>Function.Injective Units.val
<VAR>α : Type u<VAR>AddMonoid α<GOAL>Function.Injective AddUnits.val
<VAR>α : Type u<VAR>AddMonoid α<VAR>a b : AddUnits α<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : αˣ<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u<VAR>AddMonoid α<VAR>a b : AddUnits α<GOAL>a = b ↔ ↑a = ↑b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : αˣ<GOAL>a = b ↔ ↑a = ↑b
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>y : α<VAR>h₁ : ↑u * y = 1<VAR>h₂ : y * ↑u = 1<GOAL>{ val := ↑u, inv := y, val_inv := h₁, inv_val := h₂ } = u
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>y : α<VAR>h₁ : ↑u + y = 0<VAR>h₂ : y + ↑u = 0<GOAL>{ val := ↑u, neg := y, val_neg := h₁, neg_val := h₂ } = u
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>val : α<VAR>hv : val = ↑u<VAR>inv : α<VAR>hi : inv = ↑u⁻¹<GOAL>↑(u.copy val hv inv hi)⁻¹ = inv
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>val : α<VAR>hv : val = ↑u<VAR>inv : α<VAR>hi : inv = ↑u⁻¹<GOAL>↑(u.copy val hv inv hi) = val
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>val : α<VAR>hv : val = ↑u<VAR>inv : α<VAR>hi : inv = ↑(-u)<GOAL>↑(-u.copy val hv inv hi) = inv
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>val : α<VAR>hv : val = ↑u<VAR>inv : α<VAR>hi : inv = ↑(-u)<GOAL>↑(u.copy val hv inv hi) = val
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>val : α<VAR>hv : val = ↑u<VAR>inv : α<VAR>hi : inv = ↑(-u)<GOAL>u.copy val hv inv hi = u
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>val : α<VAR>hv : val = ↑u<VAR>inv : α<VAR>hi : inv = ↑u⁻¹<GOAL>u.copy val hv inv hi = u
<VAR>α : Type u<VAR>Monoid α<VAR>a b : αˣ<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u<VAR>AddMonoid α<VAR>a b : AddUnits α<GOAL>↑(a + b) = ↑a + ↑b
<VAR>α : Type u<VAR>AddMonoid α<GOAL>↑0 = 0
<VAR>α : Type u<VAR>Monoid α<GOAL>↑1 = 1
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<GOAL>↑a = 0 ↔ a = 0
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<GOAL>↑a = 1 ↔ a = 1
<VAR>α : Type u<VAR>AddMonoid α<VAR>x y : α<VAR>h₁ : x + y = 0<VAR>h₂ : y + x = 0<GOAL>-{ val := x, neg := y, val_neg := h₁, neg_val := h₂ } = { val := y, neg := x, val_neg := h₂, neg_val := h₁ }
<VAR>α : Type u<VAR>Monoid α<VAR>x y : α<VAR>h₁ : x * y = 1<VAR>h₂ : y * x = 1<GOAL>{ val := x, inv := y, val_inv := h₁, inv_val := h₂ }⁻¹ = { val := y, inv := x, val_inv := h₂, inv_val := h₁ }
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<GOAL>a.inv = ↑a⁻¹
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<GOAL>a.neg = ↑(-a)
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<GOAL>↑a⁻¹ * ↑a = 1
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<GOAL>↑(-a) + ↑a = 0
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<GOAL>↑a * ↑a⁻¹ = 1
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<GOAL>↑a + ↑(-a) = 0
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<GOAL>Commute ↑a ↑a⁻¹
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<GOAL>AddCommute ↑a ↑(-a)
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<GOAL>Commute ↑a⁻¹ ↑a
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<GOAL>AddCommute ↑(-a) ↑a
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<VAR>h : ↑u = a<GOAL>↑(-u) + a = 0
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<VAR>h : ↑u = a<GOAL>↑u⁻¹ * a = 1
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<VAR>h : ↑u = a<GOAL>a * ↑u⁻¹ = 1
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<VAR>h : ↑u = a<GOAL>a + ↑(-u) = 0
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<VAR>b : α<GOAL>↑a + (↑(-a) + b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>↑a * (↑a⁻¹ * b) = b
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<VAR>b : α<GOAL>↑(-a) + (↑a + b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>↑a⁻¹ * (↑a * b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>b : αˣ<GOAL>a * ↑b * ↑b⁻¹ = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : α<VAR>b : AddUnits α<GOAL>a + ↑b + ↑(-b) = a
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>b : αˣ<GOAL>a * ↑b⁻¹ * ↑b = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : α<VAR>b : AddUnits α<GOAL>a + ↑(-b) + ↑b = a
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<VAR>b c : α<GOAL>↑a * b = ↑a * c ↔ b = c
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<VAR>b c : α<GOAL>↑a + b = ↑a + c ↔ b = c
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<VAR>b c : α<GOAL>b * ↑a = c * ↑a ↔ b = c
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<VAR>b c : α<GOAL>b + ↑a = c + ↑a ↔ b = c
<VAR>α : Type u<VAR>Monoid α<VAR>c : αˣ<VAR>a b : α<GOAL>a = b * ↑c⁻¹ ↔ a * ↑c = b
<VAR>α : Type u<VAR>AddMonoid α<VAR>c : AddUnits α<VAR>a b : α<GOAL>a = b + ↑(-c) ↔ a + ↑c = b
<VAR>α : Type u<VAR>Monoid α<VAR>b : αˣ<VAR>a c : α<GOAL>a = ↑b⁻¹ * c ↔ ↑b * a = c
<VAR>α : Type u<VAR>AddMonoid α<VAR>b : AddUnits α<VAR>a c : α<GOAL>a = ↑(-b) + c ↔ ↑b + a = c
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<VAR>b c : α<GOAL>↑a⁻¹ * b = c ↔ b = ↑a * c
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<VAR>b c : α<GOAL>↑(-a) + b = c ↔ b = ↑a + c
<VAR>α : Type u<VAR>Monoid α<VAR>b : αˣ<VAR>a c : α<GOAL>a * ↑b⁻¹ = c ↔ a = c * ↑b
<VAR>α : Type u<VAR>AddMonoid α<VAR>b : AddUnits α<VAR>a c : α<GOAL>a + ↑(-b) = c ↔ a = c + ↑b
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<VAR>h : a + ↑u = 0<GOAL>↑(-u) = a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<VAR>h : a * ↑u = 1<GOAL>↑u⁻¹ = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<VAR>h : ↑u + a = 0<GOAL>↑(-u) = a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<VAR>h : ↑u * a = 1<GOAL>↑u⁻¹ = a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<VAR>h : ↑u * a = 1<GOAL>a = ↑u⁻¹
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<VAR>h : ↑u + a = 0<GOAL>a = ↑(-u)
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<VAR>h : a * ↑u = 1<GOAL>a = ↑u⁻¹
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<VAR>h : a + ↑u = 0<GOAL>a = ↑(-u)
<VAR>α : Type u<VAR>Monoid α<VAR>a : αˣ<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : AddUnits α<VAR>n : ℕ<GOAL>↑(n • a) = n • ↑a
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<GOAL>a + ↑(-u) = 0 ↔ a = ↑u
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<GOAL>a * ↑u⁻¹ = 1 ↔ a = ↑u
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<GOAL>↑(-u) + a = 0 ↔ ↑u = a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<GOAL>↑u⁻¹ * a = 1 ↔ ↑u = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<GOAL>a + ↑u = 0 ↔ a = ↑(-u)
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<GOAL>a * ↑u = 1 ↔ a = ↑u⁻¹
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a : α<GOAL>↑u * a = 1 ↔ ↑u⁻¹ = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>u : AddUnits α<VAR>a : α<GOAL>↑u + a = 0 ↔ ↑(-u) = a
<VAR>α : Type u<VAR>AddMonoid α<VAR>u₁ u₂ : AddUnits α<VAR>h : ↑u₁ = ↑u₂<GOAL>↑(-u₁) = ↑(-u₂)
<VAR>α : Type u<VAR>Monoid α<VAR>u₁ u₂ : αˣ<VAR>h : ↑u₁ = ↑u₂<GOAL>↑u₁⁻¹ = ↑u₂⁻¹
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>u : αˣ<GOAL>↑u⁻¹ = (↑u)⁻¹
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>u : AddUnits α<GOAL>↑(-u) = -↑u
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>u₁ u₂ : AddUnits α<GOAL>↑(u₁ - u₂) = ↑u₁ - ↑u₂
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>u₁ u₂ : αˣ<GOAL>↑(u₁ / u₂) = ↑u₁ / ↑u₂
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>a b : α<VAR>h : a + b = 0<GOAL>↑(AddUnits.mkOfAddEqZero a b h) = a
<VAR>α : Type u<VAR>CommMonoid α<VAR>a b : α<VAR>h : a * b = 1<GOAL>↑(Units.mkOfMulEqOne a b h) = a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<GOAL>↑u /ₚ u = 1
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>a /ₚ 1 = a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a * b /ₚ u = a * (b /ₚ u)
<VAR>α : Type u<VAR>Monoid α<VAR>x y : α<VAR>u : αˣ<GOAL>x * (y /ₚ u) = x * y /ₚ u
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>u : αˣ<GOAL>a /ₚ u⁻¹ = a * ↑u
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>u : αˣ<GOAL>a /ₚ u * ↑u = a
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>u : αˣ<GOAL>a * ↑u /ₚ u = a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>a b : α<GOAL>a /ₚ u = b /ₚ u ↔ a = b
<VAR>α : Type u<VAR>Monoid α<VAR>x : α<VAR>u₁ u₂ : αˣ<GOAL>x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
<VAR>α : Type u<VAR>Monoid α<VAR>x : α<VAR>u : αˣ<VAR>y : α<GOAL>x /ₚ u = y ↔ y * ↑u = x
<VAR>α : Type u<VAR>Monoid α<VAR>x : α<VAR>u : αˣ<VAR>y : α<GOAL>x = y /ₚ u ↔ x * ↑u = y
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>u : αˣ<GOAL>a /ₚ u = 1 ↔ a = ↑u
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<GOAL>1 /ₚ u = ↑u⁻¹
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<GOAL>↑u⁻¹ = 1 /ₚ u
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<GOAL>↑(1 / u) = 1 /ₚ u
<VAR>α : Type u<VAR>Monoid α<VAR>u₁ u₂ : αˣ<GOAL>↑(u₁ / u₂) = ↑u₁ /ₚ u₂
<VAR>α : Type u<VAR>CommMonoid α<VAR>x y : α<VAR>u : αˣ<GOAL>x /ₚ u * y = x * y /ₚ u
<VAR>α : Type u<VAR>CommMonoid α<VAR>x y : α<VAR>ux uy : αˣ<GOAL>x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
<VAR>α : Type u<VAR>CommMonoid α<VAR>x y : α<VAR>ux uy : αˣ<GOAL>x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Subsingleton (AddUnits α)<VAR>a b : α<VAR>h : a + b = 0<GOAL>a = 0
<VAR>α : Type u<VAR>CommMonoid α<VAR>Subsingleton αˣ<VAR>a b : α<VAR>h : a * b = 1<GOAL>a = 1
<VAR>α : Type u<VAR>CommMonoid α<VAR>Subsingleton αˣ<VAR>a b : α<VAR>h : a * b = 1<GOAL>b = 1
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Subsingleton (AddUnits α)<VAR>a b : α<VAR>h : a + b = 0<GOAL>b = 0
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Subsingleton (AddUnits α)<VAR>a b : α<GOAL>a + b = 0 ↔ a = 0 ∧ b = 0
<VAR>α : Type u<VAR>CommMonoid α<VAR>Subsingleton αˣ<VAR>a b : α<GOAL>a * b = 1 ↔ a = 1 ∧ b = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : M<GOAL>IsAddUnit x ↔ ∃ b, x + b = 0 ∧ b + x = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<GOAL>IsUnit a ↔ (∃ b, a * b = 1) ∧ ∃ c, c * a = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<GOAL>IsAddUnit a ↔ (∃ b, a + b = 0) ∧ ∃ c, c + a = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>Subsingleton M<VAR>a : M<GOAL>IsUnit a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>Subsingleton M<VAR>a : M<GOAL>IsAddUnit a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>u : AddUnits M<GOAL>IsAddUnit ↑u
<VAR>M : Type u_1<VAR>Monoid M<VAR>u : Mˣ<GOAL>IsUnit ↑u
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>IsAddUnit 0
<VAR>M : Type u_1<VAR>Monoid M<GOAL>IsUnit 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>a b : M<VAR>h : a * b = 1<GOAL>IsUnit a
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>a b : M<VAR>h : a + b = 0<GOAL>IsAddUnit a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>a b : M<VAR>h : a * b = 1<GOAL>IsUnit b
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>a b : M<VAR>h : a + b = 0<GOAL>IsAddUnit b
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>h : IsUnit a<GOAL>∃ b, a * b = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>h : IsAddUnit a<GOAL>∃ b, a + b = 0
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>h : IsAddUnit a<GOAL>∃ b, b + a = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>h : IsUnit a<GOAL>∃ b, b * a = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a b : M<GOAL>IsAddUnit a → IsAddUnit b → IsAddUnit (a + b)
<VAR>M : Type u_1<VAR>Monoid M<VAR>a b : M<GOAL>IsUnit a → IsUnit b → IsUnit (a * b)
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>n : ℕ<GOAL>IsUnit a → IsUnit (a ^ n)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>n : ℕ<GOAL>IsAddUnit a → IsAddUnit (n • a)
<VAR>M : Type u_1<VAR>Monoid M<VAR>Unique Mˣ<VAR>u : Mˣ<GOAL>u = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>Unique Mˣ<VAR>x : M<GOAL>IsUnit x ↔ x = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>Unique (AddUnits M)<VAR>x : M<GOAL>IsAddUnit x ↔ x = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>a : M<GOAL>IsUnit a ↔ ∃ b, a * b = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>a : M<GOAL>IsAddUnit a ↔ ∃ b, a + b = 0
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>a : M<GOAL>IsAddUnit a ↔ ∃ b, b + a = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>a : M<GOAL>IsUnit a ↔ ∃ b, b * a = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>u : Mˣ<GOAL>IsUnit (a * ↑u) ↔ IsUnit a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>u : AddUnits M<GOAL>IsAddUnit (a + ↑u) ↔ IsAddUnit a
<VAR>M : Type u_3<VAR>Monoid M<VAR>u : Mˣ<VAR>a : M<GOAL>IsUnit (↑u * a) ↔ IsUnit a
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>u : AddUnits M<VAR>a : M<GOAL>IsAddUnit (↑u + a) ↔ IsAddUnit a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>x y : M<VAR>hu : IsUnit (x * y)<GOAL>IsUnit x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>x y : M<VAR>hu : IsAddUnit (x + y)<GOAL>IsAddUnit x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>x y : M<VAR>hu : IsUnit (x * y)<GOAL>IsUnit y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>x y : M<VAR>hu : IsAddUnit (x + y)<GOAL>IsAddUnit y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>x y : M<GOAL>IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>x y : M<GOAL>IsAddUnit (x + y) ↔ IsAddUnit x ∧ IsAddUnit y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : AddUnits M<VAR>h : IsAddUnit ↑a<GOAL>h.addUnit = a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : Mˣ<VAR>h : IsUnit ↑a<GOAL>h.unit = a
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>h : IsUnit a<GOAL>↑h.unit = a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>h : IsAddUnit a<GOAL>↑h.addUnit = a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>h : IsAddUnit 0<GOAL>h.addUnit = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>h : IsUnit 1<GOAL>h.unit = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>h : IsAddUnit a<GOAL>↑(-h.addUnit) + a = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>h : IsUnit a<GOAL>↑h.unit⁻¹ * a = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>h : IsAddUnit a<GOAL>a + ↑(-h.addUnit) = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>h : IsUnit a<GOAL>a * ↑h.unit⁻¹ = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>a b c : M<VAR>h : IsUnit a<GOAL>b * a = c * a ↔ b = c
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a b c : M<VAR>h : IsAddUnit a<GOAL>b + a = c + a ↔ b = c
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a b c : M<VAR>h : IsAddUnit a<GOAL>a + b = a + c ↔ b = c
<VAR>M : Type u_1<VAR>Monoid M<VAR>a b c : M<VAR>h : IsUnit a<GOAL>a * b = a * c ↔ b = c
<VAR>M : Type u_1<VAR>Monoid M<VAR>a b c : M<VAR>h : IsUnit a<GOAL>a * b = a * c → b = c
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a b c : M<VAR>h : IsAddUnit a<GOAL>a + b = a + c → b = c
<VAR>M : Type u_1<VAR>Monoid M<VAR>a b c : M<VAR>h : IsUnit b<GOAL>a * b = c * b → a = c
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a b c : M<VAR>h : IsAddUnit b<GOAL>a + b = c + b → a = c
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>h : IsUnit a<GOAL>Function.Injective fun x => a * x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>h : IsAddUnit a<GOAL>Function.Injective fun x => a + x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>b : M<VAR>h : IsAddUnit b<GOAL>Function.Injective fun x => x + b
<VAR>M : Type u_1<VAR>Monoid M<VAR>b : M<VAR>h : IsUnit b<GOAL>Function.Injective fun x => x * b
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<GOAL>IsUnit a ↔ Function.Bijective fun x => a * x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<GOAL>IsAddUnit a ↔ Function.Bijective fun x => a + x
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<GOAL>IsUnit a ↔ Function.Bijective fun x => x * a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<GOAL>IsAddUnit a ↔ Function.Bijective fun x => x + a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<GOAL>IsUnit a → a⁻¹ * a = 1
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<GOAL>IsAddUnit a → -a + a = 0
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<GOAL>IsUnit a → a * a⁻¹ = 1
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<GOAL>IsAddUnit a → a + -a = 0
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>↑h.unit' = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>↑h.addUnit' = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>↑(-h.addUnit') = -a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>↑h.unit'⁻¹ = a⁻¹
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<VAR>b : α<GOAL>a + (-a + b) = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a * (a⁻¹ * b) = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a⁻¹ * (a * b) = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<VAR>b : α<GOAL>-a + (a + b) = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>b : α<VAR>h : IsAddUnit b<VAR>a : α<GOAL>a + b + -b = a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>b : α<VAR>h : IsUnit b<VAR>a : α<GOAL>a * b * b⁻¹ = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>b : α<VAR>h : IsAddUnit b<VAR>a : α<GOAL>a + -b + b = a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>b : α<VAR>h : IsUnit b<VAR>a : α<GOAL>a * b⁻¹ * b = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>a - a = 0
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>a / a = 1
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit c<GOAL>a = b + -c ↔ a + c = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a = b * c⁻¹ ↔ a * c = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit b<GOAL>a = -b + c ↔ b + a = c
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit b<GOAL>a = b⁻¹ * c ↔ b * a = c
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit a<GOAL>-a + b = c ↔ b = a + c
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit a<GOAL>a⁻¹ * b = c ↔ b = a * c
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit b<GOAL>a + -b = c ↔ a = c + b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit b<GOAL>a * b⁻¹ = c ↔ a = c * b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : IsUnit b<GOAL>a * b⁻¹ = 1 ↔ a = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : IsAddUnit b<GOAL>a + -b = 0 ↔ a = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : IsUnit a<GOAL>a⁻¹ * b = 1 ↔ a = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : IsAddUnit a<GOAL>-a + b = 0 ↔ a = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : IsUnit b<GOAL>a * b = 1 ↔ a = b⁻¹
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : IsAddUnit b<GOAL>a + b = 0 ↔ a = -b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : IsAddUnit a<GOAL>a + b = 0 ↔ -a = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : IsUnit a<GOAL>a * b = 1 ↔ a⁻¹ = b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>b : α<VAR>h : IsUnit b<VAR>a : α<GOAL>a / b * b = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>b : α<VAR>h : IsAddUnit b<VAR>a : α<GOAL>a - b + b = a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>b : α<VAR>h : IsUnit b<VAR>a : α<GOAL>a * b / b = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>b : α<VAR>h : IsAddUnit b<VAR>a : α<GOAL>a + b - b = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>a + (0 - a) = 0
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>a * (1 / a) = 1
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>1 / a * a = 1
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>0 - a + a = 0
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a : α<VAR>h : IsAddUnit a<GOAL>IsAddUnit (-a)
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>IsUnit a⁻¹
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>ha : IsUnit a<VAR>hb : IsUnit b<GOAL>IsUnit (a / b)
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>ha : IsAddUnit a<VAR>hb : IsAddUnit b<GOAL>IsAddUnit (a - b)
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a / c = b / c ↔ a = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit c<GOAL>a - c = b - c ↔ a = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit b<GOAL>a - b = c ↔ a = c + b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit b<GOAL>a / b = c ↔ a = c * b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a = b / c ↔ a * c = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit c<GOAL>a = b - c ↔ a + c = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit b<GOAL>a = c + b → a - b = c
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit b<GOAL>a = c * b → a / b = c
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a * c = b → a = b / c
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b c : α<VAR>h : IsAddUnit c<GOAL>a + c = b → a = b - c
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : IsUnit b<GOAL>a / b = 1 ↔ a = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : IsAddUnit b<GOAL>a - b = 0 ↔ a = b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>b : α<VAR>h : IsAddUnit b<VAR>a : α<GOAL>b - (a + b) = -a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>b : α<VAR>h : IsUnit b<VAR>a : α<GOAL>b / (a * b) = a⁻¹
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>a b : α<VAR>h : IsAddUnit b<GOAL>b - (a + b) = 0 - a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a b : α<VAR>h : IsUnit b<GOAL>b / (a * b) = 1 / a
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>c : α<VAR>h : IsUnit c<VAR>a b : α<GOAL>a * c / (b * c) = a / b
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>c : α<VAR>h : IsAddUnit c<VAR>a b : α<GOAL>a + c - (b + c) = a - b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>b : α<VAR>a : α<VAR>h : IsUnit b<GOAL>a * b * (1 / b) = a
<VAR>α : Type u<VAR>SubtractionMonoid α<VAR>b : α<VAR>a : α<VAR>h : IsAddUnit b<GOAL>a + b + (0 - b) = a
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a / (a * b) = b⁻¹
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a : α<VAR>h : IsAddUnit a<VAR>b : α<GOAL>a - (a + b) = -b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a / (a * b) = 1 / b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a : α<VAR>h : IsAddUnit a<VAR>b : α<GOAL>a - (a + b) = 0 - b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a * b / a = b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a : α<VAR>h : IsAddUnit a<VAR>b : α<GOAL>a + b - a = b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a * (b / a) = b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a : α<VAR>h : IsAddUnit a<VAR>b : α<GOAL>a + (b - a) = b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>c : α<VAR>h : IsUnit c<VAR>a b : α<GOAL>c * a / (c * b) = a / b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>c : α<VAR>h : IsAddUnit c<VAR>a b : α<GOAL>c + a - (c + b) = a - b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>b d : α<VAR>hb : IsAddUnit b<VAR>hd : IsAddUnit d<VAR>a c : α<VAR>h : a - b = c - d<GOAL>a + d = c + b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>b d : α<VAR>hb : IsUnit b<VAR>hd : IsUnit d<VAR>a c : α<VAR>h : a / b = c / d<GOAL>a * d = c * b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a b c d : α<VAR>hb : IsUnit b<VAR>hd : IsUnit d<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a b c d : α<VAR>hb : IsAddUnit b<VAR>hd : IsAddUnit d<GOAL>a - b = c - d ↔ a + d = c + b
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a b : α<VAR>h : IsAddUnit a<GOAL>a - (a - b) = b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a b : α<VAR>h : IsUnit a<GOAL>a / (a / b) = b
<VAR>α : Type u<VAR>DivisionCommMonoid α<VAR>a b : α<VAR>h : IsUnit a<GOAL>a / b / a = b⁻¹
<VAR>α : Type u<VAR>SubtractionCommMonoid α<VAR>a b : α<VAR>h : IsAddUnit a<GOAL>a - b - a = -b
<VAR>α : Type u<VAR>DivisionMonoid α<VAR>a : α<VAR>u : αˣ<GOAL>a /ₚ u = a / ↑u
<VAR>α : Type u<VAR>AddGroup α<VAR>a : α<GOAL>IsAddUnit a
<VAR>α : Type u<VAR>Group α<VAR>a : α<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Field R<VAR>CommSemiring A<VAR>Nontrivial A<VAR>Algebra R A<VAR>a b : R<GOAL>↑a = ↑b ↔ a = b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Field R<VAR>CommSemiring A<VAR>Nontrivial A<VAR>Algebra R A<VAR>a : R<GOAL>↑a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semifield R<VAR>DivisionSemiring A<VAR>Algebra R A<VAR>r : R<GOAL>↑r⁻¹ = (↑r)⁻¹