ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Mul α<VAR>a x y : α<GOAL>SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x) ↔ SemiconjBy a x y
<VAR>α : Type u_1<VAR>Mul α<VAR>a x y : αᵐᵒᵖ<GOAL>SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x) ↔ SemiconjBy a x y
<VAR>α : Type u_1<VAR>Add α<VAR>a x y : αᵃᵒᵖ<GOAL>AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop x) ↔ AddSemiconjBy a x y
<VAR>α : Type u_1<VAR>Mul α<VAR>a x y : α<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x)
<VAR>α : Type u_1<VAR>Add α<VAR>a x y : α<VAR>h : AddSemiconjBy a x y<GOAL>AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x)
<VAR>α : Type u_1<VAR>Add α<VAR>a x y : αᵃᵒᵖ<VAR>h : AddSemiconjBy a x y<GOAL>AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop x)
<VAR>α : Type u_1<VAR>Mul α<VAR>a x y : αᵐᵒᵖ<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x)
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : α<VAR>h : Commute x y<GOAL>Commute (MulOpposite.op x) (MulOpposite.op y)
<VAR>α : Type u_1<VAR>Add α<VAR>x y : α<VAR>h : AddCommute x y<GOAL>AddCommute (AddOpposite.op x) (AddOpposite.op y)
<VAR>α : Type u_1<VAR>Add α<VAR>x y : αᵃᵒᵖ<VAR>h : AddCommute x y<GOAL>AddCommute (AddOpposite.unop x) (AddOpposite.unop y)
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : αᵐᵒᵖ<VAR>h : Commute x y<GOAL>Commute (MulOpposite.unop x) (MulOpposite.unop y)
<VAR>α : Type u_1<VAR>Add α<VAR>x y : α<GOAL>AddCommute (AddOpposite.op x) (AddOpposite.op y) ↔ AddCommute x y
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : α<GOAL>Commute (MulOpposite.op x) (MulOpposite.op y) ↔ Commute x y
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : αᵐᵒᵖ<GOAL>Commute (MulOpposite.unop x) (MulOpposite.unop y) ↔ Commute x y
<VAR>α : Type u_1<VAR>Add α<VAR>x y : αᵃᵒᵖ<GOAL>AddCommute (AddOpposite.unop x) (AddOpposite.unop y) ↔ AddCommute x y
<VAR>α : Type u_1<VAR>Add α<GOAL>⇑MulOpposite.opAddEquiv.symm = MulOpposite.unop
<VAR>α : Type u_1<VAR>Add α<GOAL>⇑MulOpposite.opAddEquiv = MulOpposite.op
<VAR>α : Type u_1<VAR>Add α<GOAL>↑MulOpposite.opAddEquiv = MulOpposite.opEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : β<GOAL>AddOpposite.op (a ^ b) = AddOpposite.op a ^ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : αᵃᵒᵖ<VAR>b : β<GOAL>AddOpposite.unop (a ^ b) = AddOpposite.unop a ^ b
<VAR>α : Type u_1<VAR>Mul α<GOAL>⇑AddOpposite.opMulEquiv.symm = AddOpposite.unop
<VAR>α : Type u_1<VAR>Mul α<GOAL>⇑AddOpposite.opMulEquiv = AddOpposite.op
<VAR>α : Type u_1<VAR>Mul α<GOAL>↑AddOpposite.opMulEquiv = AddOpposite.opEquiv
<VAR>G : Type u_2<VAR>SubtractionMonoid G<GOAL>⇑(AddEquiv.neg' G) = AddOpposite.op ∘ Neg.neg
<VAR>G : Type u_2<VAR>SubtractionMonoid G<GOAL>⇑(AddEquiv.neg' G).symm = Neg.neg ∘ AddOpposite.unop
<VAR>G : Type u_2<VAR>DivisionMonoid G<GOAL>⇑(MulEquiv.inv' G) = MulOpposite.op ∘ Inv.inv
<VAR>G : Type u_2<VAR>DivisionMonoid G<GOAL>⇑(MulEquiv.inv' G).symm = Inv.inv ∘ MulOpposite.unop
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : ∀ (x y : M), Commute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : ∀ (x y : M), AddCommute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : ∀ (x y : M), AddCommute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : ∀ (x y : M), Commute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>hf : ∀ (x y : M), AddCommute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>hf : ∀ (x y : M), Commute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>hf : ∀ (x y : M), Commute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>hf : ∀ (x y : M), AddCommute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop
<VAR>M : Type u_2<VAR>Monoid M<VAR>u : Mᵐᵒᵖˣ<GOAL>↑(MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop ↑u
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>u : AddUnits Mᵃᵒᵖ<GOAL>↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>u : (AddUnits M)ᵃᵒᵖ<GOAL>↑(AddUnits.opEquiv.symm u) = AddOpposite.op ↑(AddOpposite.unop u)
<VAR>M : Type u_2<VAR>Monoid M<VAR>u : Mˣᵐᵒᵖ<GOAL>↑(Units.opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>m : M<VAR>h : IsAddUnit m<GOAL>IsAddUnit (AddOpposite.op m)
<VAR>M : Type u_2<VAR>Monoid M<VAR>m : M<VAR>h : IsUnit m<GOAL>IsUnit (MulOpposite.op m)
<VAR>M : Type u_2<VAR>Monoid M<VAR>m : Mᵐᵒᵖ<VAR>h : IsUnit m<GOAL>IsUnit (MulOpposite.unop m)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>m : Mᵃᵒᵖ<VAR>h : IsAddUnit m<GOAL>IsAddUnit (AddOpposite.unop m)
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>m : M<GOAL>IsAddUnit (AddOpposite.op m) ↔ IsAddUnit m
<VAR>M : Type u_2<VAR>Monoid M<VAR>m : M<GOAL>IsUnit (MulOpposite.op m) ↔ IsUnit m
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>m : Mᵃᵒᵖ<GOAL>IsAddUnit (AddOpposite.unop m) ↔ IsAddUnit m
<VAR>M : Type u_2<VAR>Monoid M<VAR>m : Mᵐᵒᵖ<GOAL>IsUnit (MulOpposite.unop m) ↔ IsUnit m
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>∀ (a : Mᵃᵒᵖ), (AddHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ<GOAL>∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>∀ (a : Mᵐᵒᵖ), (MulHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ<GOAL>∀ (a : M), (AddHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>∀ (a : Mᵐᵒᵖ), (AddHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ<GOAL>∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : Mᵃᵒᵖ →+ Nᵃᵒᵖ<GOAL>∀ (a : M), (AddMonoidHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>∀ (a : Mᵐᵒᵖ), (MonoidHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : Mᵐᵒᵖ →* Nᵐᵒᵖ<GOAL>∀ (a : M), (MonoidHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
<VAR>M : Type u_2<VAR>Mul M<GOAL>∀ (a : Mᵐᵒᵖᵐᵒᵖ), (MulEquiv.opOp M).symm a = MulOpposite.unop (MulOpposite.unop a)
<VAR>M : Type u_2<VAR>Add M<GOAL>∀ (a : M), (AddEquiv.opOp M) a = AddOpposite.op (AddOpposite.op a)
<VAR>M : Type u_2<VAR>Mul M<GOAL>∀ (a : M), (MulEquiv.opOp M) a = MulOpposite.op (MulOpposite.op a)
<VAR>M : Type u_2<VAR>Add M<GOAL>∀ (a : Mᵃᵒᵖᵃᵒᵖ), (AddEquiv.opOp M).symm a = AddOpposite.unop (AddOpposite.unop a)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : Mᵐᵒᵖ →+ Nᵐᵒᵖ<GOAL>∀ (a : M), (AddMonoidHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>∀ (a : Mᵐᵒᵖ), (AddMonoidHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f : α ≃+ β<GOAL>AddEquiv.mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f : αᵐᵒᵖ ≃+ βᵐᵒᵖ<GOAL>AddEquiv.mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>f : α ≃* β<GOAL>∀ (a : βᵐᵒᵖ), (MulEquiv.op f).symm a = (MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>f : αᵐᵒᵖ ≃* βᵐᵒᵖ<GOAL>∀ (a : β), (MulEquiv.op.symm f).symm a = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f : αᵃᵒᵖ ≃+ βᵃᵒᵖ<GOAL>∀ (a : α), (AddEquiv.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f : α ≃+ β<GOAL>∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f : αᵃᵒᵖ ≃+ βᵃᵒᵖ<GOAL>∀ (a : β), (AddEquiv.op.symm f).symm a = (AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>f : α ≃+ β<GOAL>∀ (a : βᵃᵒᵖ), (AddEquiv.op f).symm a = (AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>f : αᵐᵒᵖ ≃* βᵐᵒᵖ<GOAL>∀ (a : α), (MulEquiv.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>f : α ≃* β<GOAL>∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f g : αᵐᵒᵖ →+ β<VAR>h : f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom<GOAL>f = g
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → VAdd M (α i)<VAR>a : M<VAR>x : (i : ι) × α i<GOAL>a +ᵥ x = Sigma.map id (fun x x_1 => a +ᵥ x_1) x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → SMul M (α i)<VAR>a : M<VAR>x : (i : ι) × α i<GOAL>a • x = Sigma.map id (fun x x_1 => a • x_1) x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → SMul M (α i)<VAR>a : M<VAR>i : ι<VAR>b : α i<GOAL>a • ⟨i, b⟩ = ⟨i, a • b⟩
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → VAdd M (α i)<VAR>a : M<VAR>i : ι<VAR>b : α i<GOAL>a +ᵥ ⟨i, b⟩ = ⟨i, a +ᵥ b⟩
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → SMul M (α i)<VAR>i : ι<VAR>FaithfulSMul M (α i)<GOAL>FaithfulSMul M ((i : ι) × α i)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>α : ι → Type u_4<VAR>(i : ι) → VAdd M (α i)<VAR>i : ι<VAR>FaithfulVAdd M (α i)<GOAL>FaithfulVAdd M ((i : ι) × α i)
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>Invertible a<GOAL>↑(unitOfInvertible a) = a
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>Invertible a<GOAL>↑(unitOfInvertible a)⁻¹ = ⅟a
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>Invertible a<GOAL>IsUnit a
<VAR>α : Type u<VAR>Monoid α<VAR>u : αˣ<VAR>Invertible ↑u<GOAL>⅟↑u = ↑u⁻¹
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>h : IsUnit a<GOAL>Nonempty (Invertible a)
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>Nonempty (Invertible a) ↔ IsUnit a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible b<VAR>h : Commute a b<GOAL>Commute a ⅟b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible b<VAR>h : Commute b a<GOAL>Commute (⅟b) a
<VAR>M : Type u_1<VAR>One M<VAR>Mul M<VAR>m : M<VAR>Invertible m<GOAL>Commute m ⅟m
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>∀ (x : Invertible a) (b : α) (x_1 : Invertible b), (x.mulLeft b) x_1 = invertibleMul a b
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>∀ (x : Invertible a) (b : α) (x_1 : Invertible (a * b)), (x.mulLeft b).symm x_1 = invertibleOfInvertibleMul a b
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>b : α<GOAL>∀ (x : Invertible b) (x_1 : Invertible a), (Invertible.mulRight a x) x_1 = invertibleMul a b
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>b : α<GOAL>∀ (x : Invertible b) (x_1 : Invertible (a * b)), (Invertible.mulRight a x).symm x_1 = invertibleOfMulInvertible a b
<VAR>α : Type u<VAR>Monoid α<VAR>m : α<VAR>Invertible m<VAR>n : ℕ<VAR>Invertible (m ^ n)<GOAL>⅟(m ^ n) = ⅟m ^ n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>MulOneClass R<VAR>Monoid S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>f : F<VAR>r : R<VAR>Invertible r<VAR>ifr : Invertible (f r)<GOAL>f ⅟r = ⅟(f r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>G : Type u_3<VAR>MulOneClass R<VAR>MulOneClass S<VAR>FunLike G S R<VAR>MonoidHomClass G S R<VAR>f : R → S<VAR>g : G<VAR>r : R<VAR>h : Function.LeftInverse (⇑g) f<VAR>Invertible (f r)<GOAL>⅟r = ⅟(g (f r))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>FunLike G S R<VAR>MonoidHomClass G S R<VAR>f : F<VAR>g : G<VAR>r : R<VAR>h : Function.LeftInverse ⇑g ⇑f<GOAL>∀ (x : Invertible (f r)), (invertibleEquivOfLeftInverse f g r h) x = Invertible.ofLeftInverse (⇑f) g r h
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>FunLike G S R<VAR>MonoidHomClass G S R<VAR>f : F<VAR>g : G<VAR>r : R<VAR>h : Function.LeftInverse ⇑g ⇑f<GOAL>∀ (x : Invertible r), (invertibleEquivOfLeftInverse f g r h).symm x = Invertible.map f r
<VAR>α : Type u<VAR>Mul α<VAR>One α<VAR>a : α<VAR>self : Invertible a<GOAL>⅟a * a = 1
<VAR>α : Type u<VAR>Mul α<VAR>One α<VAR>a : α<VAR>self : Invertible a<GOAL>a * ⅟a = 1
<VAR>α : Type u<VAR>Mul α<VAR>One α<VAR>a : α<GOAL>∀ {x : Invertible a}, ⅟a * a = 1
<VAR>α : Type u<VAR>Mul α<VAR>One α<VAR>a : α<VAR>Invertible a<GOAL>⅟a * a = 1
<VAR>α : Type u<VAR>Mul α<VAR>One α<VAR>a : α<GOAL>∀ {x : Invertible a}, a * ⅟a = 1
<VAR>α : Type u<VAR>Mul α<VAR>One α<VAR>a : α<VAR>Invertible a<GOAL>a * ⅟a = 1
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>∀ {x : Invertible a}, ⅟a * (a * b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<GOAL>⅟a * (a * b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>∀ {x : Invertible a}, a * (⅟a * b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<GOAL>a * (⅟a * b) = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>∀ {x : Invertible b}, a * ⅟b * b = a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible b<GOAL>a * ⅟b * b = a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>∀ {x : Invertible b}, a * b * ⅟b = a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible b<GOAL>a * b * ⅟b = a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<VAR>hac : a * b = 1<GOAL>⅟a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<VAR>hac : b * a = 1<GOAL>⅟a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<VAR>Invertible b<VAR>h : a = b<GOAL>⅟a = ⅟b
<VAR>α : Type u<VAR>Group α<VAR>a : α<VAR>Invertible a<GOAL>⅟a = a⁻¹
<VAR>α : Type u<VAR>Monoid α<GOAL>∀ {x : Invertible 1}, ⅟1 = 1
<VAR>α : Type u<VAR>Monoid α<VAR>Invertible 1<GOAL>⅟1 = 1
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>Invertible a<VAR>Invertible ⅟a<GOAL>⅟⅟a = a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<VAR>Invertible b<GOAL>⅟a = ⅟b ↔ a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>Invertible a<VAR>Invertible b<VAR>Invertible (a * b)<GOAL>⅟(a * b) = ⅟b * ⅟a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>c : α<VAR>Invertible c<GOAL>a * c = b * c ↔ a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>c : α<VAR>Invertible c<GOAL>c * a = c * b ↔ a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a b c : α<VAR>Invertible c<GOAL>⅟c * a = b ↔ a = c * b
<VAR>α : Type u<VAR>Monoid α<VAR>a b c : α<VAR>Invertible c<GOAL>c * a = b ↔ a = ⅟c * b
<VAR>α : Type u<VAR>Monoid α<VAR>a b c : α<VAR>Invertible c<GOAL>a * ⅟c = b ↔ a = b * c
<VAR>α : Type u<VAR>Monoid α<VAR>a b c : α<VAR>Invertible c<GOAL>a * c = b ↔ a = b * ⅟c
<VAR>G : Type u_11<VAR>P : Type u_12<VAR>VAdd G P<VAR>self : FaithfulVAdd G P<VAR>g₁ g₂ : G<GOAL>(∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>SMul M α<VAR>self : FaithfulSMul M α<VAR>m₁ m₂ : M<GOAL>(∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>VAdd M α<VAR>FaithfulVAdd M α<GOAL>Function.Injective fun x x_1 => x +ᵥ x_1
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>SMul M α<VAR>FaithfulSMul M α<GOAL>Function.Injective fun x x_1 => x • x_1
<VAR>α : Type u_11<VAR>Add α<VAR>a a' : α<GOAL>a +ᵥ a' = a + a'
<VAR>α : Type u_11<VAR>Mul α<VAR>a a' : α<GOAL>a • a' = a * a'
<VAR>G : Type u_11<VAR>P : Type u_12<VAR>AddMonoid G<VAR>self : AddAction G P<VAR>g₁ g₂ : G<VAR>p : P<GOAL>g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
<VAR>G : Type u_11<VAR>P : Type u_12<VAR>AddMonoid G<VAR>self : AddAction G P<VAR>p : P<GOAL>0 +ᵥ p = p
<VAR>α : Type u_11<VAR>β : Type u_12<VAR>Monoid α<VAR>self : MulAction α β<VAR>x y : α<VAR>b : β<GOAL>(x * y) • b = x • y • b
<VAR>α : Type u_11<VAR>β : Type u_12<VAR>Monoid α<VAR>self : MulAction α β<VAR>b : β<GOAL>1 • b = b
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>VAdd M α<VAR>self : AddAction.IsPretransitive M α<VAR>x y : α<GOAL>∃ g, g +ᵥ x = y
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>SMul M α<VAR>self : MulAction.IsPretransitive M α<VAR>x y : α<GOAL>∃ g, g • x = y
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>VAdd M α<VAR>AddAction.IsPretransitive M α<VAR>x y : α<GOAL>∃ m, m +ᵥ x = y
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>SMul M α<VAR>MulAction.IsPretransitive M α<VAR>x y : α<GOAL>∃ m, m • x = y
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>VAdd M α<VAR>AddAction.IsPretransitive M α<VAR>x : α<GOAL>Function.Surjective fun c => c +ᵥ x
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>SMul M α<VAR>MulAction.IsPretransitive M α<VAR>x : α<GOAL>Function.Surjective fun c => c • x
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>VAdd M α<VAR>VAdd N α<VAR>self : VAddCommClass M N α<VAR>m : M<VAR>n : N<VAR>a : α<GOAL>m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>SMul M α<VAR>SMul N α<VAR>self : SMulCommClass M N α<VAR>m : M<VAR>n : N<VAR>a : α<GOAL>m • n • a = n • m • a
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>SMul M α<VAR>SMul N α<VAR>SMulCommClass M N α<GOAL>SMulCommClass N M α
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>VAdd M α<VAR>VAdd N α<VAR>VAddCommClass M N α<GOAL>VAddCommClass N M α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd M α<VAR>VAdd N α<VAR>VAdd M β<VAR>VAdd N β<VAR>VAddCommClass M N β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>h₁ : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x<VAR>h₂ : ∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x<GOAL>VAddCommClass M N α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul M α<VAR>SMul N α<VAR>SMul M β<VAR>SMul N β<VAR>SMulCommClass M N β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x<VAR>h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x<GOAL>SMulCommClass M N α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd M α<VAR>VAdd N α<VAR>VAdd M β<VAR>VAdd N β<VAR>VAddCommClass M N α<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h₁ : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x<VAR>h₂ : ∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x<GOAL>VAddCommClass M N β
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul M α<VAR>SMul N α<VAR>SMul M β<VAR>SMul N β<VAR>SMulCommClass M N α<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x<VAR>h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x<GOAL>SMulCommClass M N β
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>VAdd M N<VAR>VAdd N α<VAR>VAdd M α<VAR>self : VAddAssocClass M N α<VAR>x : M<VAR>y : N<VAR>z : α<GOAL>x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>SMul M N<VAR>SMul N α<VAR>SMul M α<VAR>self : IsScalarTower M N α<VAR>x : M<VAR>y : N<VAR>z : α<GOAL>(x • y) • z = x • y • z
<VAR>α : Type u_7<VAR>M : Type u_11<VAR>N : Type u_12<VAR>SMul M N<VAR>SMul N α<VAR>SMul M α<VAR>IsScalarTower M N α<VAR>x : M<VAR>y : N<VAR>z : α<GOAL>(x • y) • z = x • y • z
<VAR>α : Type u_7<VAR>M : Type u_11<VAR>N : Type u_12<VAR>VAdd M N<VAR>VAdd N α<VAR>VAdd M α<VAR>VAddAssocClass M N α<VAR>x : M<VAR>y : N<VAR>z : α<GOAL>x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>VAdd M α<VAR>VAdd Mᵃᵒᵖ α<VAR>self : IsCentralVAdd M α<VAR>m : M<VAR>a : α<GOAL>AddOpposite.op m +ᵥ a = m +ᵥ a
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>SMul M α<VAR>SMul Mᵐᵒᵖ α<VAR>self : IsCentralScalar M α<VAR>m : M<VAR>a : α<GOAL>MulOpposite.op m • a = m • a
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>VAdd M α<VAR>VAdd Mᵃᵒᵖ α<VAR>IsCentralVAdd M α<VAR>m : Mᵃᵒᵖ<VAR>a : α<GOAL>AddOpposite.unop m +ᵥ a = m +ᵥ a
<VAR>M : Type u_11<VAR>α : Type u_12<VAR>SMul M α<VAR>SMul Mᵐᵒᵖ α<VAR>IsCentralScalar M α<VAR>m : Mᵐᵒᵖ<VAR>a : α<GOAL>MulOpposite.unop m • a = m • a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul M α<VAR>SMul M β<VAR>SMul α β<VAR>IsScalarTower M α β<VAR>g : N → M<GOAL>IsScalarTower N α β
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd M α<VAR>VAdd M β<VAR>VAdd α β<VAR>VAddAssocClass M α β<VAR>g : N → M<GOAL>VAddAssocClass N α β
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd M α<VAR>VAdd β α<VAR>VAddCommClass M β α<VAR>g : N → M<GOAL>VAddCommClass N β α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul M α<VAR>SMul β α<VAR>SMulCommClass M β α<VAR>g : N → M<GOAL>SMulCommClass N β α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd M α<VAR>VAdd β α<VAR>VAddCommClass β M α<VAR>g : N → M<GOAL>VAddCommClass β N α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul M α<VAR>SMul β α<VAR>SMulCommClass β M α<VAR>g : N → M<GOAL>SMulCommClass β N α
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Add β<VAR>VAdd α β<VAR>VAddCommClass α β β<VAR>s : α<VAR>x y : β<GOAL>x + (s +ᵥ y) = s +ᵥ (x + y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Mul β<VAR>SMul α β<VAR>SMulCommClass α β β<VAR>s : α<VAR>x y : β<GOAL>x * s • y = s • (x * y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Add β<VAR>VAdd α β<VAR>VAddAssocClass α β β<VAR>r : α<VAR>x y : β<GOAL>r +ᵥ x + y = r +ᵥ (x + y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Mul β<VAR>SMul α β<VAR>IsScalarTower α β β<VAR>r : α<VAR>x y : β<GOAL>r • x * y = r • (x * y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SubNegMonoid β<VAR>VAdd α β<VAR>VAddAssocClass α β β<VAR>r : α<VAR>x y : β<GOAL>r +ᵥ x - y = r +ᵥ (x - y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>DivInvMonoid β<VAR>SMul α β<VAR>IsScalarTower α β β<VAR>r : α<VAR>x y : β<GOAL>r • x / y = r • (x / y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>VAdd α β<VAR>VAdd α γ<VAR>VAdd β δ<VAR>VAdd α δ<VAR>VAdd γ δ<VAR>VAddAssocClass α β δ<VAR>VAddAssocClass α γ δ<VAR>VAddCommClass β γ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<GOAL>a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>SMul α β<VAR>SMul α γ<VAR>SMul β δ<VAR>SMul α δ<VAR>SMul γ δ<VAR>IsScalarTower α β δ<VAR>IsScalarTower α γ δ<VAR>SMulCommClass β γ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<GOAL>(a • b) • c • d = (a • c) • b • d
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>VAdd M α<VAR>Add α<VAR>VAddCommClass M α α<VAR>VAddAssocClass M α α<VAR>a b : α<VAR>h : AddCommute a b<VAR>r : M<GOAL>AddCommute a (r +ᵥ b)
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>SMul M α<VAR>Mul α<VAR>SMulCommClass M α α<VAR>IsScalarTower M α α<VAR>a b : α<VAR>h : Commute a b<VAR>r : M<GOAL>Commute a (r • b)
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>VAdd M α<VAR>Add α<VAR>VAddCommClass M α α<VAR>VAddAssocClass M α α<VAR>a b : α<VAR>h : AddCommute a b<VAR>r : M<GOAL>AddCommute (r +ᵥ a) b
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>SMul M α<VAR>Mul α<VAR>SMulCommClass M α α<VAR>IsScalarTower M α α<VAR>a b : α<VAR>h : Commute a b<VAR>r : M<GOAL>Commute (r • a) b
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>AddMonoid M<VAR>AddAction M α<VAR>a₁ a₂ : M<VAR>b : α<GOAL>a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>Monoid M<VAR>MulAction M α<VAR>a₁ a₂ : M<VAR>b : α<GOAL>a₁ • a₂ • b = (a₁ * a₂) • b
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>Monoid M<VAR>MulAction M α<VAR>b : α<GOAL>1 • b = b
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>AddMonoid M<VAR>AddAction M α<VAR>b : α<GOAL>0 +ᵥ b = b