ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>g : AddHom N M<VAR>h₁ : g.comp f = AddHom.id M<VAR>h₂ : f.comp g = AddHom.id N<GOAL>⇑(f.toAddEquiv g h₁ h₂) = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>g : N →ₙ* M<VAR>h₁ : g.comp f = MulHom.id M<VAR>h₂ : f.comp g = MulHom.id N<GOAL>⇑(f.toMulEquiv g h₁ h₂) = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>g : AddHom N M<VAR>h₁ : g.comp f = AddHom.id M<VAR>h₂ : f.comp g = AddHom.id N<GOAL>⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>g : N →ₙ* M<VAR>h₁ : g.comp f = MulHom.id M<VAR>h₂ : f.comp g = MulHom.id N<GOAL>⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>g : N →+ M<VAR>h₁ : g.comp f = AddMonoidHom.id M<VAR>h₂ : f.comp g = AddMonoidHom.id N<GOAL>⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>g : N →* M<VAR>h₁ : g.comp f = MonoidHom.id M<VAR>h₂ : f.comp g = MonoidHom.id N<GOAL>⇑(f.toMulEquiv g h₁ h₂) = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>g : N →+ M<VAR>h₁ : g.comp f = AddMonoidHom.id M<VAR>h₂ : f.comp g = AddMonoidHom.id N<GOAL>⇑(f.toAddEquiv g h₁ h₂) = ⇑f
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>g : N →* M<VAR>h₁ : g.comp f = MonoidHom.id M<VAR>h₂ : f.comp g = MonoidHom.id N<GOAL>⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
<VAR>G : Type u_10<VAR>InvolutiveInv G<GOAL>⇑(Equiv.inv G) = Inv.inv
<VAR>G : Type u_10<VAR>InvolutiveNeg G<GOAL>⇑(Equiv.neg G) = Neg.neg
<VAR>G : Type u_10<VAR>InvolutiveInv G<GOAL>Equiv.symm (Equiv.inv G) = Equiv.inv G
<VAR>G : Type u_10<VAR>InvolutiveNeg G<GOAL>Equiv.symm (Equiv.neg G) = Equiv.neg G
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → One (α j)<VAR>i : Fin (n + 1)<VAR>x : α i<GOAL>i.insertNth x 1 = Pi.mulSingle i x
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → Zero (α j)<VAR>i : Fin (n + 1)<VAR>x : α i<GOAL>i.insertNth x 0 = Pi.single i x
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → Mul (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p q : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → Add (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p q : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth (x + y) (p + q) = i.insertNth x p + i.insertNth y q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → Div (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p q : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → Sub (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p q : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → AddGroup (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth x p - i.insertNth y p = Pi.single i (x - y)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>(j : Fin (n + 1)) → Group (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>SMul M α<VAR>x : M<VAR>v : Fin 0 → α<GOAL>x • v = ![]
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>SMul M α<VAR>x : M<VAR>y : α<VAR>v : Fin n → α<GOAL>x • Matrix.vecCons y v = Matrix.vecCons (x • y) (x • v)
<VAR>α : Type u_1<VAR>Add α<VAR>v w : Fin 0 → α<GOAL>v + w = ![]
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Add α<VAR>x : α<VAR>v : Fin n → α<VAR>w : Fin n.succ → α<GOAL>Matrix.vecCons x v + w = Matrix.vecCons (x + Matrix.vecHead w) (v + Matrix.vecTail w)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Add α<VAR>v : Fin n.succ → α<VAR>y : α<VAR>w : Fin n → α<GOAL>v + Matrix.vecCons y w = Matrix.vecCons (Matrix.vecHead v + y) (Matrix.vecTail v + w)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Add α<VAR>x : α<VAR>v : Fin n → α<VAR>y : α<VAR>w : Fin n → α<GOAL>Matrix.vecCons x v + Matrix.vecCons y w = Matrix.vecCons (x + y) (v + w)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Add α<VAR>a b : Fin n.succ → α<GOAL>Matrix.vecHead (a + b) = Matrix.vecHead a + Matrix.vecHead b
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Add α<VAR>a b : Fin n.succ → α<GOAL>Matrix.vecTail (a + b) = Matrix.vecTail a + Matrix.vecTail b
<VAR>α : Type u_1<VAR>Sub α<VAR>v w : Fin 0 → α<GOAL>v - w = ![]
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Sub α<VAR>x : α<VAR>v : Fin n → α<VAR>w : Fin n.succ → α<GOAL>Matrix.vecCons x v - w = Matrix.vecCons (x - Matrix.vecHead w) (v - Matrix.vecTail w)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Sub α<VAR>v : Fin n.succ → α<VAR>y : α<VAR>w : Fin n → α<GOAL>v - Matrix.vecCons y w = Matrix.vecCons (Matrix.vecHead v - y) (Matrix.vecTail v - w)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Sub α<VAR>x : α<VAR>v : Fin n → α<VAR>y : α<VAR>w : Fin n → α<GOAL>Matrix.vecCons x v - Matrix.vecCons y w = Matrix.vecCons (x - y) (v - w)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Sub α<VAR>a b : Fin n.succ → α<GOAL>Matrix.vecHead (a - b) = Matrix.vecHead a - Matrix.vecHead b
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Sub α<VAR>a b : Fin n.succ → α<GOAL>Matrix.vecTail (a - b) = Matrix.vecTail a - Matrix.vecTail b
<VAR>α : Type u_1<VAR>Zero α<GOAL>0 = ![]
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Zero α<GOAL>Matrix.vecCons 0 0 = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Zero α<GOAL>Matrix.vecHead 0 = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Zero α<GOAL>Matrix.vecTail 0 = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Zero α<VAR>v : Fin n → α<VAR>x : α<GOAL>Matrix.vecCons x v = 0 ↔ x = 0 ∧ v = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Zero α<VAR>v : Fin n → α<VAR>x : α<GOAL>Matrix.vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0
<VAR>α : Type u_1<VAR>Neg α<VAR>v : Fin 0 → α<GOAL>-v = ![]
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Neg α<VAR>x : α<VAR>v : Fin n → α<GOAL>-Matrix.vecCons x v = Matrix.vecCons (-x) (-v)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Neg α<VAR>a : Fin n.succ → α<GOAL>Matrix.vecHead (-a) = -Matrix.vecHead a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>Neg α<VAR>a : Fin n.succ → α<GOAL>Matrix.vecTail (-a) = -Matrix.vecTail a
<VAR>α : Type u<GOAL>Additive.ofMul.symm = Additive.toMul
<VAR>α : Type u<GOAL>Additive.toMul.symm = Additive.ofMul
<VAR>α : Type u<VAR>p : Additive α → Prop<GOAL>(∀ (a : Additive α), p a) ↔ ∀ (a : α), p (Additive.ofMul a)
<VAR>α : Type u<VAR>p : Additive α → Prop<GOAL>(∃ a, p a) ↔ ∃ a, p (Additive.ofMul a)
<VAR>α : Type u<GOAL>Multiplicative.ofAdd.symm = Multiplicative.toAdd
<VAR>α : Type u<GOAL>Multiplicative.toAdd.symm = Multiplicative.ofAdd
<VAR>α : Type u<VAR>p : Multiplicative α → Prop<GOAL>(∀ (a : Multiplicative α), p a) ↔ ∀ (a : α), p (Multiplicative.ofAdd a)
<VAR>α : Type u<VAR>p : Multiplicative α → Prop<GOAL>(∃ a, p a) ↔ ∃ a, p (Multiplicative.ofAdd a)
<VAR>α : Type u<VAR>x : α<GOAL>Multiplicative.toAdd (Multiplicative.ofAdd x) = x
<VAR>α : Type u<VAR>x : Multiplicative α<GOAL>Multiplicative.ofAdd (Multiplicative.toAdd x) = x
<VAR>α : Type u<VAR>x : α<GOAL>Additive.toMul (Additive.ofMul x) = x
<VAR>α : Type u<VAR>x : Additive α<GOAL>Additive.ofMul (Additive.toMul x) = x
<VAR>α : Type u<VAR>Add α<VAR>x y : α<GOAL>Multiplicative.ofAdd (x + y) = Multiplicative.ofAdd x * Multiplicative.ofAdd y
<VAR>α : Type u<VAR>Add α<VAR>x y : Multiplicative α<GOAL>Multiplicative.toAdd (x * y) = Multiplicative.toAdd x + Multiplicative.toAdd y
<VAR>α : Type u<VAR>Mul α<VAR>x y : α<GOAL>Additive.ofMul (x * y) = Additive.ofMul x + Additive.ofMul y
<VAR>α : Type u<VAR>Mul α<VAR>x y : Additive α<GOAL>Additive.toMul (x + y) = Additive.toMul x * Additive.toMul y
<VAR>α : Type u<VAR>One α<GOAL>Additive.ofMul 1 = 0
<VAR>A : Type u_1<VAR>One A<VAR>x : A<GOAL>Additive.ofMul x = 0 ↔ x = 1
<VAR>α : Type u<VAR>One α<GOAL>Additive.toMul 0 = 1
<VAR>α : Type u_1<VAR>One α<VAR>x : Additive α<GOAL>Additive.toMul x = 1 ↔ x = 0
<VAR>α : Type u<VAR>Zero α<GOAL>Multiplicative.ofAdd 0 = 1
<VAR>A : Type u_1<VAR>Zero A<VAR>x : A<GOAL>Multiplicative.ofAdd x = 1 ↔ x = 0
<VAR>α : Type u<VAR>Zero α<GOAL>Multiplicative.toAdd 1 = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>x : Multiplicative α<GOAL>Multiplicative.toAdd x = 0 ↔ x = 1
<VAR>α : Type u<VAR>Monoid α<VAR>n : ℕ<VAR>a : α<GOAL>Additive.ofMul (a ^ n) = n • Additive.ofMul a
<VAR>α : Type u<VAR>Monoid α<VAR>n : ℕ<VAR>a : Additive α<GOAL>Additive.toMul (n • a) = Additive.toMul a ^ n
<VAR>α : Type u<VAR>AddMonoid α<VAR>n : ℕ<VAR>a : α<GOAL>Multiplicative.ofAdd (n • a) = Multiplicative.ofAdd a ^ n
<VAR>α : Type u<VAR>AddMonoid α<VAR>a : Multiplicative α<VAR>n : ℕ<GOAL>Multiplicative.toAdd (a ^ n) = n • Multiplicative.toAdd a
<VAR>α : Type u<VAR>Inv α<VAR>x : α<GOAL>Additive.ofMul x⁻¹ = -Additive.ofMul x
<VAR>α : Type u<VAR>Inv α<VAR>x : Additive α<GOAL>Additive.toMul (-x) = (Additive.toMul x)⁻¹
<VAR>α : Type u<VAR>Neg α<VAR>x : α<GOAL>Multiplicative.ofAdd (-x) = (Multiplicative.ofAdd x)⁻¹
<VAR>α : Type u<VAR>Neg α<VAR>x : Multiplicative α<GOAL>Multiplicative.toAdd x⁻¹ = -Multiplicative.toAdd x
<VAR>α : Type u<VAR>Sub α<VAR>x y : α<GOAL>Multiplicative.ofAdd (x - y) = Multiplicative.ofAdd x / Multiplicative.ofAdd y
<VAR>α : Type u<VAR>Sub α<VAR>x y : Multiplicative α<GOAL>Multiplicative.toAdd (x / y) = Multiplicative.toAdd x - Multiplicative.toAdd y
<VAR>α : Type u<VAR>Div α<VAR>x y : α<GOAL>Additive.ofMul (x / y) = Additive.ofMul x - Additive.ofMul y
<VAR>α : Type u<VAR>Div α<VAR>x y : Additive α<GOAL>Additive.toMul (x - y) = Additive.toMul x / Additive.toMul y
<VAR>α : Type u<VAR>DivInvMonoid α<VAR>z : ℤ<VAR>a : α<GOAL>Additive.ofMul (a ^ z) = z • Additive.ofMul a
<VAR>α : Type u<VAR>DivInvMonoid α<VAR>z : ℤ<VAR>a : Additive α<GOAL>Additive.toMul (z • a) = Additive.toMul a ^ z
<VAR>α : Type u<VAR>SubNegMonoid α<VAR>z : ℤ<VAR>a : α<GOAL>Multiplicative.ofAdd (z • a) = Multiplicative.ofAdd a ^ z
<VAR>α : Type u<VAR>SubNegMonoid α<VAR>a : Multiplicative α<VAR>z : ℤ<GOAL>Multiplicative.toAdd (a ^ z) = z • Multiplicative.toAdd a
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+ β<VAR>a : Multiplicative α<GOAL>(AddMonoidHom.toMultiplicative f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : Multiplicative α →* Multiplicative β<VAR>a : α<GOAL>(AddMonoidHom.toMultiplicative.symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+ β<GOAL>⇑(AddMonoidHom.toMultiplicative f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Multiplicative.toAdd
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>a : Additive α<GOAL>(MonoidHom.toAdditive f) a = Additive.ofMul (f (Additive.toMul a))
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : Additive α →+ Additive β<VAR>a : α<GOAL>(MonoidHom.toAdditive.symm f) a = Additive.toMul (f (Additive.ofMul a))
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<GOAL>⇑(MonoidHom.toAdditive f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Additive.toMul
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>AddZeroClass β<VAR>f : Additive α →+ β<VAR>a : α<GOAL>(AddMonoidHom.toMultiplicative' f) a = Multiplicative.ofAdd (f (Additive.ofMul a))
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>AddZeroClass β<VAR>f : α →* Multiplicative β<VAR>a : Additive α<GOAL>(AddMonoidHom.toMultiplicative'.symm f) a = Multiplicative.toAdd (f (Additive.toMul a))
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>AddZeroClass β<VAR>f : Additive α →+ β<GOAL>⇑(AddMonoidHom.toMultiplicative' f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>AddZeroClass β<GOAL>∀ (a : α →* Multiplicative β) (a_1 : Additive α), (MonoidHom.toAdditive' a) a_1 = Multiplicative.toAdd (a (Additive.toMul a_1))
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>AddZeroClass β<GOAL>∀ (a : Additive α →+ β) (a_1 : α), (MonoidHom.toAdditive'.symm a) a_1 = Multiplicative.ofAdd (a (Additive.ofMul a_1))
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>AddZeroClass β<VAR>f : α →* Multiplicative β<GOAL>⇑(MonoidHom.toAdditive' f) = ⇑Multiplicative.toAdd ∘ ⇑f ∘ ⇑Additive.toMul
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>MulOneClass β<VAR>f : Multiplicative α →* β<VAR>a : α<GOAL>(AddMonoidHom.toMultiplicative''.symm f) a = Additive.ofMul (f (Multiplicative.ofAdd a))
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>MulOneClass β<VAR>f : α →+ Additive β<VAR>a : Multiplicative α<GOAL>(AddMonoidHom.toMultiplicative'' f) a = Additive.toMul (f (Multiplicative.toAdd a))
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>MulOneClass β<VAR>f : α →+ Additive β<GOAL>⇑(AddMonoidHom.toMultiplicative'' f) = ⇑Additive.toMul ∘ ⇑f ∘ ⇑Multiplicative.toAdd
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>MulOneClass β<GOAL>∀ (a : α →+ Additive β) (a_1 : Multiplicative α), (MonoidHom.toAdditive''.symm a) a_1 = Additive.toMul (a (Multiplicative.toAdd a_1))
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>MulOneClass β<GOAL>∀ (a : Multiplicative α →* β) (a_1 : α), (MonoidHom.toAdditive'' a) a_1 = Additive.ofMul (a (Multiplicative.ofAdd a_1))
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>MulOneClass β<VAR>f : Multiplicative α →* β<GOAL>⇑(MonoidHom.toAdditive'' f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Multiplicative.ofAdd
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a x y : G<GOAL>SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a x y : G<GOAL>AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
<VAR>G : Type u_1<VAR>Group G<VAR>a x y : G<GOAL>SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a x y : G<GOAL>AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a x y : G<GOAL>AddSemiconjBy a (-x) (-y) ↔ AddSemiconjBy a x y
<VAR>G : Type u_1<VAR>Group G<VAR>a x y : G<GOAL>SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
<VAR>G : Type u_1<VAR>Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<VAR>m : ℤ<GOAL>SemiconjBy a (x ^ m) (y ^ m)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a x y : G<VAR>h : AddSemiconjBy a x y<VAR>m : ℤ<GOAL>AddSemiconjBy a (m • x) (m • y)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>x y : G<VAR>h : AddSemiconjBy a x y<GOAL>x = 0 ↔ y = 0
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>x y : G<VAR>h : SemiconjBy a x y<GOAL>x = 1 ↔ y = 1
<VAR>S : Type u_1<VAR>Mul S<VAR>a x y : S<VAR>h : SemiconjBy a x y<GOAL>a * x = y * a
<VAR>S : Type u_1<VAR>Add S<VAR>a x y : S<VAR>h : AddSemiconjBy a x y<GOAL>a + x = y + a
<VAR>S : Type u_1<VAR>AddSemigroup S<VAR>a x y x' y' : S<VAR>h : AddSemiconjBy a x y<VAR>h' : AddSemiconjBy a x' y'<GOAL>AddSemiconjBy a (x + x') (y + y')
<VAR>S : Type u_1<VAR>Semigroup S<VAR>a x y x' y' : S<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x * x') (y * y')
<VAR>S : Type u_1<VAR>AddSemigroup S<VAR>a b x y z : S<VAR>ha : AddSemiconjBy a y z<VAR>hb : AddSemiconjBy b x y<GOAL>AddSemiconjBy (a + b) x z
<VAR>S : Type u_1<VAR>Semigroup S<VAR>a b x y z : S<VAR>ha : SemiconjBy a y z<VAR>hb : SemiconjBy b x y<GOAL>SemiconjBy (a * b) x z
<VAR>S : Type u_1<VAR>Semigroup S<GOAL>Transitive fun a b => ∃ c, SemiconjBy c a b
<VAR>S : Type u_1<VAR>AddSemigroup S<GOAL>Transitive fun a b => ∃ c, AddSemiconjBy c a b
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>a : M<GOAL>SemiconjBy a 1 1
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>a : M<GOAL>AddSemiconjBy a 0 0
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>x : M<GOAL>SemiconjBy 1 x x
<VAR>M : Type u_2<VAR>AddZeroClass M<VAR>x : M<GOAL>AddSemiconjBy 0 x x
<VAR>M : Type u_2<VAR>MulOneClass M<GOAL>Reflexive fun a b => ∃ c, SemiconjBy c a b
<VAR>M : Type u_2<VAR>AddZeroClass M<GOAL>Reflexive fun a b => ∃ c, AddSemiconjBy c a b
<VAR>M : Type u_2<VAR>Monoid M<VAR>a x y : M<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (x ^ n) (y ^ n)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>a x y : M<VAR>h : AddSemiconjBy a x y<VAR>n : ℕ<GOAL>AddSemiconjBy a (n • x) (n • y)
<VAR>G : Type u_3<VAR>Group G<VAR>a x : G<GOAL>SemiconjBy a x (a * x * a⁻¹)
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a x : G<GOAL>AddSemiconjBy a x (a + x + -a)
<VAR>G : Type u_3<VAR>Group G<VAR>a x y b : G<GOAL>SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a x y b : G<GOAL>AddSemiconjBy (b + a + -b) (b + x + -b) (b + y + -b) ↔ AddSemiconjBy a x y
<VAR>M : Type u_2<VAR>CancelCommMonoid M<VAR>a x y : M<GOAL>SemiconjBy a x y ↔ x = y
<VAR>M : Type u_2<VAR>AddCancelCommMonoid M<VAR>a x y : M<GOAL>AddSemiconjBy a x y ↔ x = y
<VAR>M : Type u_2<VAR>Mul M<VAR>e₁ e₂ : MulAut M<GOAL>⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
<VAR>M : Type u_2<VAR>Mul M<GOAL>⇑1 = id
<VAR>M : Type u_2<VAR>Mul M<VAR>e₁ e₂ : MulAut M<GOAL>e₁ * e₂ = MulEquiv.trans e₂ e₁
<VAR>M : Type u_2<VAR>Mul M<GOAL>1 = MulEquiv.refl M
<VAR>M : Type u_2<VAR>Mul M<VAR>e₁ : MulAut M<GOAL>e₁⁻¹ = MulEquiv.symm e₁
<VAR>M : Type u_2<VAR>Mul M<VAR>e₁ e₂ : MulAut M<VAR>m : M<GOAL>(e₁ * e₂) m = e₁ (e₂ m)
<VAR>M : Type u_2<VAR>Mul M<VAR>m : M<GOAL>1 m = m
<VAR>M : Type u_2<VAR>Mul M<VAR>e : MulAut M<VAR>m : M<GOAL>e (e⁻¹ m) = m
<VAR>M : Type u_2<VAR>Mul M<VAR>e : MulAut M<VAR>m : M<GOAL>e⁻¹ (e m) = m
<VAR>M : Type u_4<VAR>Monoid M<VAR>f : MulAut M<VAR>a : M<GOAL>f • a = f a
<VAR>G : Type u_3<VAR>Group G<VAR>g h : G<GOAL>(MulAut.conj g) h = g * h * g⁻¹
<VAR>G : Type u_3<VAR>Group G<VAR>g h : G<GOAL>(MulEquiv.symm (MulAut.conj g)) h = g⁻¹ * h * g
<VAR>G : Type u_3<VAR>Group G<VAR>g h : G<GOAL>(MulAut.conj g)⁻¹ h = g⁻¹ * h * g
<VAR>A : Type u_1<VAR>Add A<VAR>e₁ e₂ : AddAut A<GOAL>⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
<VAR>A : Type u_1<VAR>Add A<GOAL>⇑1 = id
<VAR>A : Type u_1<VAR>Add A<VAR>e₁ e₂ : AddAut A<GOAL>e₁ * e₂ = AddEquiv.trans e₂ e₁
<VAR>A : Type u_1<VAR>Add A<GOAL>1 = AddEquiv.refl A
<VAR>A : Type u_1<VAR>Add A<VAR>e₁ : AddAut A<GOAL>e₁⁻¹ = AddEquiv.symm e₁
<VAR>A : Type u_1<VAR>Add A<VAR>e₁ e₂ : AddAut A<VAR>a : A<GOAL>(e₁ * e₂) a = e₁ (e₂ a)
<VAR>A : Type u_1<VAR>Add A<VAR>a : A<GOAL>1 a = a
<VAR>A : Type u_1<VAR>Add A<VAR>e : AddAut A<VAR>a : A<GOAL>e⁻¹ (e a) = a
<VAR>A : Type u_1<VAR>Add A<VAR>e : AddAut A<VAR>a : A<GOAL>e (e⁻¹ a) = a
<VAR>A : Type u_4<VAR>AddMonoid A<VAR>f : AddAut A<VAR>a : A<GOAL>f • a = f a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>g h : G<GOAL>(Additive.toMul (AddAut.conj g)) h = g + h + -g
<VAR>G : Type u_3<VAR>AddGroup G<VAR>g h : G<GOAL>(AddEquiv.symm (AddAut.conj g)) h = -g + h + g
<VAR>G : Type u_3<VAR>AddGroup G<VAR>g h : G<GOAL>(Additive.toMul (AddAut.conj g))⁻¹ h = -g + h + g
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>x y : AddUnits M<VAR>h : AddSemiconjBy a ↑x ↑y<GOAL>AddSemiconjBy a ↑(-x) ↑(-y)
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>x y : Mˣ<VAR>h : SemiconjBy a ↑x ↑y<GOAL>SemiconjBy a ↑x⁻¹ ↑y⁻¹
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>x y : Mˣ<GOAL>SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a ↑x ↑y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>x y : AddUnits M<GOAL>AddSemiconjBy a ↑(-x) ↑(-y) ↔ AddSemiconjBy a ↑x ↑y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : AddUnits M<VAR>x y : M<VAR>h : AddSemiconjBy (↑a) x y<GOAL>AddSemiconjBy (↑(-a)) y x
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : Mˣ<VAR>x y : M<VAR>h : SemiconjBy (↑a) x y<GOAL>SemiconjBy (↑a⁻¹) y x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : AddUnits M<VAR>x y : M<GOAL>AddSemiconjBy (↑(-a)) y x ↔ AddSemiconjBy (↑a) x y
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : Mˣ<VAR>x y : M<GOAL>SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a x y : AddUnits M<VAR>h : AddSemiconjBy a x y<GOAL>AddSemiconjBy ↑a ↑x ↑y
<VAR>M : Type u_1<VAR>Monoid M<VAR>a x y : Mˣ<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy ↑a ↑x ↑y
<VAR>M : Type u_1<VAR>Monoid M<VAR>a x y : Mˣ<VAR>h : SemiconjBy ↑a ↑x ↑y<GOAL>SemiconjBy a x y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a x y : AddUnits M<VAR>h : AddSemiconjBy ↑a ↑x ↑y<GOAL>AddSemiconjBy a x y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a x y : AddUnits M<GOAL>AddSemiconjBy ↑a ↑x ↑y ↔ AddSemiconjBy a x y
<VAR>M : Type u_1<VAR>Monoid M<VAR>a x y : Mˣ<GOAL>SemiconjBy ↑a ↑x ↑y ↔ SemiconjBy a x y
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>x y : Mˣ<VAR>h : SemiconjBy a ↑x ↑y<VAR>m : ℤ<GOAL>SemiconjBy a ↑(x ^ m) ↑(y ^ m)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : M<VAR>x y : AddUnits M<VAR>h : AddSemiconjBy a ↑x ↑y<VAR>m : ℤ<GOAL>AddSemiconjBy a ↑(m • x) ↑(m • y)
<VAR>M : Type u_1<VAR>Monoid M<VAR>u : Mˣ<VAR>x : M<GOAL>SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>u : AddUnits M<VAR>x : M<GOAL>AddSemiconjBy (↑u) x (↑u + x + ↑(-u))
<VAR>M : Type u_1<VAR>Monoid M<VAR>u : Mˣ<VAR>x : M<VAR>n : ℕ<GOAL>(↑u * x * ↑u⁻¹) ^ n = ↑u * x ^ n * ↑u⁻¹
<VAR>M : Type u_1<VAR>Monoid M<VAR>u : Mˣ<VAR>x : M<VAR>n : ℕ<GOAL>(↑u⁻¹ * x * ↑u) ^ n = ↑u⁻¹ * x ^ n * ↑u
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>p q : M × N<GOAL>(p + q).1 = p.1 + q.1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>p q : M × N<GOAL>(p * q).1 = p.1 * q.1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>p q : M × N<GOAL>(p * q).2 = p.2 * q.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>p q : M × N<GOAL>(p + q).2 = p.2 + q.2
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>a₁ a₂ : M<VAR>b₁ b₂ : N<GOAL>(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>a₁ a₂ : M<VAR>b₁ b₂ : N<GOAL>(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>p q : M × N<GOAL>(p * q).swap = p.swap * q.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>p q : M × N<GOAL>(p + q).swap = p.swap + q.swap
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>Add N<VAR>p q : M × N<GOAL>p + q = (p.1 + q.1, p.2 + q.2)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Mul N<VAR>p q : M × N<GOAL>p * q = (p.1 * q.1, p.2 * q.2)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddMonoid M<VAR>Add N<VAR>b₁ b₂ : N<GOAL>(0, b₁) + (0, b₂) = (0, b₁ + b₂)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Monoid M<VAR>Mul N<VAR>b₁ b₂ : N<GOAL>(1, b₁) * (1, b₂) = (1, b₁ * b₂)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Add M<VAR>AddMonoid N<VAR>a₁ a₂ : M<GOAL>(a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Mul M<VAR>Monoid N<VAR>a₁ a₂ : M<GOAL>(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>One M<VAR>One N<GOAL>1.1 = 1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Zero M<VAR>Zero N<GOAL>0.1 = 0
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>One M<VAR>One N<GOAL>1.2 = 1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Zero M<VAR>Zero N<GOAL>0.2 = 0
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Zero M<VAR>Zero N<GOAL>0 = (0, 0)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>One M<VAR>One N<GOAL>1 = (1, 1)
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>One M<VAR>One N<VAR>x : M<VAR>y : N<GOAL>(x, y) = 1 ↔ x = 1 ∧ y = 1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Zero M<VAR>Zero N<VAR>x : M<VAR>y : N<GOAL>(x, y) = 0 ↔ x = 0 ∧ y = 0
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>One M<VAR>One N<GOAL>Prod.swap 1 = 1
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Zero M<VAR>Zero N<GOAL>Prod.swap 0 = 0
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>p : M × N<GOAL>(p.1, 1) * (1, p.2) = p
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>p : M × N<GOAL>(p.1, 0) + (0, p.2) = p
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Inv G<VAR>Inv H<VAR>p : G × H<GOAL>p⁻¹.1 = p.1⁻¹
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Neg G<VAR>Neg H<VAR>p : G × H<GOAL>(-p).1 = -p.1
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Neg G<VAR>Neg H<VAR>p : G × H<GOAL>(-p).2 = -p.2
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Inv G<VAR>Inv H<VAR>p : G × H<GOAL>p⁻¹.2 = p.2⁻¹
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Neg G<VAR>Neg H<VAR>a : G<VAR>b : H<GOAL>-(a, b) = (-a, -b)
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Inv G<VAR>Inv H<VAR>a : G<VAR>b : H<GOAL>(a, b)⁻¹ = (a⁻¹, b⁻¹)
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Neg G<VAR>Neg H<VAR>p : G × H<GOAL>(-p).swap = -p.swap
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Inv G<VAR>Inv H<VAR>p : G × H<GOAL>p⁻¹.swap = p.swap⁻¹
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Div G<VAR>Div H<VAR>a b : G × H<GOAL>(a / b).1 = a.1 / b.1
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Sub G<VAR>Sub H<VAR>a b : G × H<GOAL>(a - b).1 = a.1 - b.1