ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>Monoid M<VAR>MulAction M α<GOAL>(fun x => 1 • x) = id
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>AddMonoid M<VAR>AddAction M α<GOAL>(fun x => 0 +ᵥ x) = id
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>AddMonoid M<VAR>AddAction M α<VAR>a₁ a₂ : M<GOAL>((fun x => a₁ +ᵥ x) ∘ fun x => a₂ +ᵥ x) = fun x => a₁ + a₂ +ᵥ x
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>Monoid M<VAR>MulAction M α<VAR>a₁ a₂ : M<GOAL>((fun x => a₁ • x) ∘ fun x => a₂ • x) = fun x => (a₁ * a₂) • x
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>AddMonoid M<VAR>AddAction M α<VAR>Add α<VAR>r s : M<VAR>x y : α<VAR>VAddAssocClass M α α<VAR>VAddCommClass M α α<GOAL>r +ᵥ x + (s +ᵥ y) = r + s +ᵥ (x + y)
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>Monoid M<VAR>MulAction M α<VAR>Mul α<VAR>r s : M<VAR>x y : α<VAR>IsScalarTower M α α<VAR>SMulCommClass M α α<GOAL>r • x * s • y = (r * s) • (x * y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>MulAction M N<VAR>IsScalarTower M N N<VAR>SMulCommClass M N N<VAR>r : M<VAR>x : N<VAR>n : ℕ<GOAL>(r • x) ^ n = r ^ n • x ^ n
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>-g +ᵥ (g +ᵥ a) = a
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>g⁻¹ • g • a = a
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>g +ᵥ (-g +ᵥ a) = a
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>g • g⁻¹ • a = a
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a b : α<GOAL>g⁻¹ • a = b ↔ a = g • b
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a b : α<GOAL>-g +ᵥ a = b ↔ a = g +ᵥ b
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a b : α<GOAL>a = g⁻¹ • b ↔ g • a = b
<VAR>G : Type u_3<VAR>α : Type u_7<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a b : α<GOAL>a = -g +ᵥ b ↔ g +ᵥ a = b
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Mul H<VAR>MulAction G H<VAR>SMulCommClass G H H<VAR>IsScalarTower G H H<VAR>g : G<VAR>a b : H<GOAL>Commute a (g • b) ↔ Commute a b
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Mul H<VAR>MulAction G H<VAR>SMulCommClass G H H<VAR>IsScalarTower G H H<VAR>g : G<VAR>a b : H<GOAL>Commute (g • a) b ↔ Commute a b
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Group H<VAR>MulAction G H<VAR>SMulCommClass G H H<VAR>IsScalarTower G H H<VAR>g : G<VAR>a : H<GOAL>(g • a)⁻¹ = g⁻¹ • a⁻¹
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Group H<VAR>MulAction G H<VAR>SMulCommClass G H H<VAR>IsScalarTower G H H<VAR>g : G<VAR>a : H<VAR>n : ℤ<GOAL>(g • a) ^ n = g ^ n • a ^ n
<VAR>A : Type u_11<VAR>B : Type u_12<VAR>G : Type u_13<VAR>CommMonoid G<VAR>SMul A G<VAR>SMul B G<VAR>IsScalarTower A G G<VAR>IsScalarTower B G G<GOAL>SMulCommClass A B G
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>Monoid M<VAR>MulAction M α<VAR>x : M<VAR>y : α<GOAL>(MulAction.toFun M α) y x = x • y
<VAR>M : Type u_1<VAR>α : Type u_7<VAR>AddMonoid M<VAR>AddAction M α<VAR>x : M<VAR>y : α<GOAL>(AddAction.toFun M α) y x = x +ᵥ y
<VAR>E : Type u_11<VAR>F : Type u_12<VAR>G : Type u_13<VAR>AddMonoid E<VAR>AddMonoid F<VAR>AddAction F G<VAR>f : E →+ F<VAR>a : E<VAR>x : G<GOAL>a +ᵥ x = f a +ᵥ x
<VAR>E : Type u_11<VAR>F : Type u_12<VAR>G : Type u_13<VAR>Monoid E<VAR>Monoid F<VAR>MulAction F G<VAR>f : E →* F<VAR>a : E<VAR>x : G<GOAL>a • x = f a • x
<VAR>E : Type u_11<VAR>F : Type u_12<VAR>G : Type u_13<VAR>Monoid E<VAR>Monoid F<VAR>MulAction F G<VAR>MulAction.IsPretransitive F G<VAR>f : E →* F<VAR>hf : Function.Surjective ⇑f<GOAL>MulAction.IsPretransitive E G
<VAR>E : Type u_11<VAR>F : Type u_12<VAR>G : Type u_13<VAR>AddMonoid E<VAR>AddMonoid F<VAR>AddAction F G<VAR>AddAction.IsPretransitive F G<VAR>f : E →+ F<VAR>hf : Function.Surjective ⇑f<GOAL>AddAction.IsPretransitive E G
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>SMul M α<VAR>SMul N α<VAR>MulAction.IsPretransitive M α<VAR>f : M → N<VAR>hf : ∀ {c : M} {x : α}, f c • x = c • x<GOAL>MulAction.IsPretransitive N α
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>VAdd M α<VAR>VAdd N α<VAR>AddAction.IsPretransitive M α<VAR>f : M → N<VAR>hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x<GOAL>AddAction.IsPretransitive N α
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddAction N α<VAR>f : M →+ N<VAR>h : AddAction.IsPretransitive M α<GOAL>AddAction.IsPretransitive N α
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>Monoid M<VAR>Monoid N<VAR>MulAction N α<VAR>f : M →* N<VAR>h : MulAction.IsPretransitive M α<GOAL>MulAction.IsPretransitive N α
<VAR>α : Type u_7<VAR>M : Type u_11<VAR>N : Type u_12<VAR>AddMonoid N<VAR>VAdd M N<VAR>AddAction N α<VAR>VAdd M α<VAR>VAddAssocClass M N α<VAR>x : M<VAR>y : α<GOAL>x +ᵥ 0 +ᵥ y = x +ᵥ y
<VAR>α : Type u_7<VAR>M : Type u_11<VAR>N : Type u_12<VAR>Monoid N<VAR>SMul M N<VAR>MulAction N α<VAR>SMul M α<VAR>IsScalarTower M N α<VAR>x : M<VAR>y : α<GOAL>(x • 1) • y = x • y
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>Monoid N<VAR>SMul M N<VAR>MulAction N α<VAR>SMul M α<VAR>IsScalarTower M N α<VAR>MulAction.IsPretransitive M α<GOAL>MulAction.IsPretransitive N α
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>α : Type u_13<VAR>AddMonoid N<VAR>VAdd M N<VAR>AddAction N α<VAR>VAdd M α<VAR>VAddAssocClass M N α<VAR>AddAction.IsPretransitive M α<GOAL>AddAction.IsPretransitive N α
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>MulOneClass N<VAR>SMul M N<VAR>IsScalarTower M N N<VAR>x : M<VAR>y : N<GOAL>x • 1 * y = x • y
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>AddZeroClass N<VAR>VAdd M N<VAR>VAddAssocClass M N N<VAR>x : M<VAR>y : N<GOAL>x +ᵥ 0 + y = x +ᵥ y
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>MulOneClass N<VAR>SMul M N<VAR>SMulCommClass M N N<VAR>x : M<VAR>y : N<GOAL>y * x • 1 = x • y
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>AddZeroClass N<VAR>VAdd M N<VAR>VAddCommClass M N N<VAR>x : M<VAR>y : N<GOAL>y + (x +ᵥ 0) = x +ᵥ y
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>AddMonoid N<VAR>VAdd M N<VAR>h : ∀ (x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y<GOAL>VAddAssocClass M N N
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>Monoid N<VAR>SMul M N<VAR>h : ∀ (x : M) (y : N), x • 1 * y = x • y<GOAL>IsScalarTower M N N
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>AddMonoid N<VAR>VAdd M N<VAR>H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y<GOAL>VAddCommClass M N N
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>Monoid N<VAR>SMul M N<VAR>H : ∀ (x : M) (y : N), y * x • 1 = x • y<GOAL>SMulCommClass M N N
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>Monoid M<VAR>MulOneClass N<VAR>MulAction M N<VAR>IsScalarTower M N N<VAR>x : M<GOAL>MonoidHom.smulOneHom x = x • 1
<VAR>M : Type u_11<VAR>N : Type u_12<VAR>AddMonoid M<VAR>AddZeroClass N<VAR>AddAction M N<VAR>VAddAssocClass M N N<VAR>x : M<GOAL>AddMonoidHom.vaddZeroHom x = x +ᵥ 0
<VAR>α : Type u_7<VAR>f : Function.End α<VAR>a : α<GOAL>f • a = f a
<VAR>α : Type u_7<VAR>f g : Function.End α<GOAL>f * g = f ∘ g
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul α β<VAR>a : Additive α<VAR>b : β<GOAL>Additive.toMul a • b = a +ᵥ b
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>SMul α β<VAR>a : α<VAR>b : β<GOAL>Additive.ofMul a +ᵥ b = a • b
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd α β<VAR>a : Multiplicative α<VAR>b : β<GOAL>Multiplicative.toAdd a +ᵥ b = a • b
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>VAdd α β<VAR>a : α<VAR>b : β<GOAL>Multiplicative.ofAdd a • b = a +ᵥ b
<VAR>G : Type u_1<VAR>Mul G<VAR>IsLeftCancelMul G<VAR>g h : G<GOAL>(mulLeftEmbedding g) h = g * h
<VAR>G : Type u_1<VAR>Add G<VAR>IsLeftCancelAdd G<VAR>g h : G<GOAL>(addLeftEmbedding g) h = g + h
<VAR>G : Type u_1<VAR>Add G<VAR>IsRightCancelAdd G<VAR>g h : G<GOAL>(addRightEmbedding g) h = h + g
<VAR>G : Type u_1<VAR>Mul G<VAR>IsRightCancelMul G<VAR>g h : G<GOAL>(mulRightEmbedding g) h = h * g
<VAR>G : Type u_1<VAR>CommSemigroup G<VAR>IsCancelMul G<VAR>g : G<GOAL>mulLeftEmbedding g = mulRightEmbedding g
<VAR>G : Type u_1<VAR>AddCommSemigroup G<VAR>IsCancelAdd G<VAR>g : G<GOAL>addLeftEmbedding g = addRightEmbedding g
<VAR>α : Type u<VAR>Add α<GOAL>∀ (a : α), WithZero.coeAddHom a = ↑a
<VAR>α : Type u<VAR>Mul α<GOAL>∀ (a : α), WithOne.coeMulHom a = ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>AddZeroClass β<VAR>f : AddHom α β<VAR>x : α<GOAL>(WithZero.lift f) ↑x = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>MulOneClass β<VAR>f : α →ₙ* β<VAR>x : α<GOAL>(WithOne.lift f) ↑x = f x
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>MulOneClass β<VAR>f : α →ₙ* β<GOAL>(WithOne.lift f) 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>AddZeroClass β<VAR>f : AddHom α β<GOAL>(WithZero.lift f) 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>AddZeroClass β<VAR>f : WithZero α →+ β<GOAL>f = WithZero.lift ((↑f).comp WithZero.coeAddHom)
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>MulOneClass β<VAR>f : WithOne α →* β<GOAL>f = WithOne.lift ((↑f).comp WithOne.coeMulHom)
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>Mul β<VAR>f : α →ₙ* β<VAR>a : α<GOAL>(WithOne.map f) ↑a = ↑(f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>Add β<VAR>f : AddHom α β<VAR>a : α<GOAL>(WithZero.map f) ↑a = ↑(f a)
<VAR>α : Type u<VAR>Add α<GOAL>WithZero.map (AddHom.id α) = AddMonoidHom.id (WithZero α)
<VAR>α : Type u<VAR>Mul α<GOAL>WithOne.map (MulHom.id α) = MonoidHom.id (WithOne α)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Add α<VAR>Add β<VAR>Add γ<VAR>f : AddHom α β<VAR>g : AddHom β γ<VAR>x : WithZero α<GOAL>(WithZero.map g) ((WithZero.map f) x) = (WithZero.map (g.comp f)) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Mul α<VAR>Mul β<VAR>Mul γ<VAR>f : α →ₙ* β<VAR>g : β →ₙ* γ<VAR>x : WithOne α<GOAL>(WithOne.map g) ((WithOne.map f) x) = (WithOne.map (g.comp f)) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Add α<VAR>Add β<VAR>Add γ<VAR>f : AddHom α β<VAR>g : AddHom β γ<GOAL>WithZero.map (g.comp f) = (WithZero.map g).comp (WithZero.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Mul α<VAR>Mul β<VAR>Mul γ<VAR>f : α →ₙ* β<VAR>g : β →ₙ* γ<GOAL>WithOne.map (g.comp f) = (WithOne.map g).comp (WithOne.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>Add β<VAR>e : α ≃+ β<VAR>a : WithZero α<GOAL>e.withZeroCongr a = (WithZero.map e.toAddHom) a
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>Mul β<VAR>e : α ≃* β<VAR>a : WithOne α<GOAL>e.withOneCongr a = (WithOne.map e.toMulHom) a
<VAR>α : Type u<VAR>Add α<GOAL>(AddEquiv.refl α).withZeroCongr = AddEquiv.refl (WithZero α)
<VAR>α : Type u<VAR>Mul α<GOAL>(MulEquiv.refl α).withOneCongr = MulEquiv.refl (WithOne α)
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>Mul β<VAR>e : α ≃* β<GOAL>e.withOneCongr.symm = e.symm.withOneCongr
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>Add β<VAR>e : α ≃+ β<GOAL>e.withZeroCongr.symm = e.symm.withZeroCongr
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Add α<VAR>Add β<VAR>Add γ<VAR>e₁ : α ≃+ β<VAR>e₂ : β ≃+ γ<GOAL>e₁.withZeroCongr.trans e₂.withZeroCongr = (e₁.trans e₂).withZeroCongr
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Mul α<VAR>Mul β<VAR>Mul γ<VAR>e₁ : α ≃* β<VAR>e₂ : β ≃* γ<GOAL>e₁.withOneCongr.trans e₂.withOneCongr = (e₁.trans e₂).withOneCongr
<VAR>α : Type u_2<VAR>Add α<VAR>m : α<GOAL>Even (m + m)
<VAR>α : Type u_2<VAR>Mul α<VAR>m : α<GOAL>IsSquare (m * m)
<VAR>α : Type u_2<VAR>Mul α<VAR>a : α<GOAL>IsSquare (MulOpposite.op a) ↔ IsSquare a
<VAR>α : Type u_2<VAR>Add α<VAR>a : α<GOAL>Even (AddOpposite.op a) ↔ Even a
<VAR>α : Type u_2<VAR>Mul α<VAR>a : αᵐᵒᵖ<GOAL>IsSquare (MulOpposite.unop a) ↔ IsSquare a
<VAR>α : Type u_2<VAR>Add α<VAR>a : αᵃᵒᵖ<GOAL>Even (AddOpposite.unop a) ↔ Even a
<VAR>α : Type u_2<VAR>Mul α<VAR>a : α<GOAL>Even (Additive.ofMul a) ↔ IsSquare a
<VAR>α : Type u_2<VAR>Mul α<VAR>a : Additive α<GOAL>IsSquare (Additive.toMul a) ↔ Even a
<VAR>α : Type u_2<VAR>Add α<VAR>a : α<GOAL>IsSquare (Multiplicative.ofAdd a) ↔ Even a
<VAR>α : Type u_2<VAR>Add α<VAR>a : Multiplicative α<GOAL>Even (Multiplicative.toAdd a) ↔ IsSquare a
<VAR>α : Type u_2<VAR>AddZeroClass α<GOAL>Even 0
<VAR>α : Type u_2<VAR>MulOneClass α<GOAL>IsSquare 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulOneClass α<VAR>MulOneClass β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : α<VAR>f : F<GOAL>IsSquare m → IsSquare (f m)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : α<VAR>f : F<GOAL>Even m → Even (f m)
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>m : α<GOAL>Even m ↔ ∃ c, m = 2 • c
<VAR>α : Type u_2<VAR>Monoid α<VAR>m : α<GOAL>IsSquare m ↔ ∃ c, m = c ^ 2
<VAR>α : Type u_2<VAR>Monoid α<VAR>a : α<VAR>n : ℕ<GOAL>IsSquare a → IsSquare (a ^ n)
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>Even a → Even (n • a)
<VAR>α : Type u_2<VAR>Monoid α<VAR>n : ℕ<GOAL>Even n → ∀ (a : α), IsSquare (a ^ n)
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>n : ℕ<GOAL>Even n → ∀ (a : α), Even (n • a)
<VAR>α : Type u_2<VAR>Monoid α<VAR>a : α<GOAL>IsSquare (a ^ 2)
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>a : α<GOAL>Even (2 • a)
<VAR>α : Type u_2<VAR>AddCommSemigroup α<VAR>a b : α<GOAL>Even a → Even b → Even (a + b)
<VAR>α : Type u_2<VAR>CommSemigroup α<VAR>a b : α<GOAL>IsSquare a → IsSquare b → IsSquare (a * b)
<VAR>α : Type u_2<VAR>SubtractionMonoid α<VAR>a : α<GOAL>Even (-a) ↔ Even a
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>a : α<GOAL>IsSquare a⁻¹ ↔ IsSquare a
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>IsSquare a → IsSquare (a ^ n)
<VAR>α : Type u_2<VAR>SubtractionMonoid α<VAR>a : α<VAR>n : ℤ<GOAL>Even a → Even (n • a)
<VAR>α : Type u_2<VAR>SubtractionCommMonoid α<VAR>a b : α<VAR>ha : Even a<VAR>hb : Even b<GOAL>Even (a - b)
<VAR>α : Type u_2<VAR>DivisionCommMonoid α<VAR>a b : α<VAR>ha : IsSquare a<VAR>hb : IsSquare b<GOAL>IsSquare (a / b)
<VAR>α : Type u_2<VAR>AddGroup α<VAR>n : ℤ<GOAL>Even n → ∀ (a : α), Even (n • a)
<VAR>α : Type u_2<VAR>Group α<VAR>n : ℤ<GOAL>Even n → ∀ (a : α), IsSquare (a ^ n)
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>InvolutiveInv G<VAR>SetLike S G<VAR>InvMemClass S G<VAR>H : S<GOAL>(↑H)⁻¹ = ↑H
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>InvolutiveNeg G<VAR>SetLike S G<VAR>NegMemClass S G<VAR>H : S<GOAL>-↑H = ↑H
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>AddGroup G<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>s : S<VAR>a : G<VAR>ha : a ∈ s<GOAL>a +ᵥ ↑s = ↑s
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>Group G<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>s : S<VAR>a : G<VAR>ha : a ∈ s<GOAL>a • ↑s = ↑s
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>AddGroup G<VAR>SetLike S G<VAR>AddSubgroupClass S G<VAR>s : S<VAR>a : G<VAR>ha : a ∈ s<GOAL>AddOpposite.op a +ᵥ ↑s = ↑s
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>Group G<VAR>SetLike S G<VAR>SubgroupClass S G<VAR>s : S<VAR>a : G<VAR>ha : a ∈ s<GOAL>MulOpposite.op a • ↑s = ↑s
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>SetLike S G<VAR>SubNegMonoid G<VAR>AddSubgroupClass S G<VAR>H : S<GOAL>↑H + ↑H = ↑H
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>SetLike S G<VAR>DivInvMonoid G<VAR>SubgroupClass S G<VAR>H : S<GOAL>↑H * ↑H = ↑H
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>SetLike S G<VAR>SubtractionMonoid G<VAR>AddSubgroupClass S G<VAR>H : S<GOAL>↑H - ↑H = ↑H
<VAR>G : Type u_2<VAR>S : Type u_4<VAR>SetLike S G<VAR>DivisionMonoid G<VAR>SubgroupClass S G<VAR>H : S<GOAL>↑H / ↑H = ↑H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : Set G<GOAL>-S ⊆ ↑(AddSubgroup.closure S)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Set G<GOAL>S⁻¹ ⊆ ↑(Subgroup.closure S)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Set G<GOAL>(Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : Set G<GOAL>(AddSubgroup.closure S).toAddSubmonoid = AddSubmonoid.closure (S ∪ -S)
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<VAR>p : (x : G) → x ∈ Subgroup.closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯<VAR>mul_left_inv : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯<VAR>x : G<VAR>h : x ∈ Subgroup.closure s<GOAL>p x h
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<VAR>p : (x : G) → x ∈ AddSubgroup.closure s → Prop<VAR>one : p 0 ⋯<VAR>mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯<VAR>mul_left_inv : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯<VAR>x : G<VAR>h : x ∈ AddSubgroup.closure s<GOAL>p x h
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<VAR>p : (x : G) → x ∈ AddSubgroup.closure s → Prop<VAR>one : p 0 ⋯<VAR>mul_right : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯<VAR>mul_right_inv : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯<VAR>x : G<VAR>h : x ∈ AddSubgroup.closure s<GOAL>p x h
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<VAR>p : (x : G) → x ∈ Subgroup.closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_right : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯<VAR>mul_right_inv : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯<VAR>x : G<VAR>h : x ∈ Subgroup.closure s<GOAL>p x h
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.closure s⁻¹ = Subgroup.closure s
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<GOAL>AddSubgroup.closure (-s) = AddSubgroup.closure s
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<VAR>p : (g : G) → g ∈ Subgroup.closure s → Prop<VAR>mem : ∀ (x : G) (hx : x ∈ s), p x ⋯<VAR>inv_mem : ∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : G<VAR>h : x ∈ Subgroup.closure s<GOAL>p x h
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<VAR>p : (g : G) → g ∈ AddSubgroup.closure s → Prop<VAR>mem : ∀ (x : G) (hx : x ∈ s), p x ⋯<VAR>inv_mem : ∀ (x : G) (hx : x ∈ s), p (-x) ⋯<VAR>one : p 0 ⋯<VAR>mul : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s), p x hx → p y hy → p (x + y) ⋯<VAR>x : G<VAR>h : x ∈ AddSubgroup.closure s<GOAL>p x h
<VAR>G : Type u_2<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>S : ι → AddSubgroup G<VAR>C : G → Prop<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 0<VAR>mul : ∀ (x y : G), C x → C y → C (x + y)<GOAL>C x
<VAR>G : Type u_2<VAR>Group G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : G → Prop<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : G), C x → C y → C (x * y)<GOAL>C x
<VAR>G : Type u_2<VAR>Group G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 1 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<GOAL>C x hx
<VAR>G : Type u_2<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>S : ι → AddSubgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 0 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<GOAL>C x hx
<VAR>G : Type u_2<VAR>Group G<VAR>S T : Set G<GOAL>Subgroup.closure (S * T) ≤ Subgroup.closure S ⊔ Subgroup.closure T
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S T : Set G<GOAL>AddSubgroup.closure (S + T) ≤ AddSubgroup.closure S ⊔ AddSubgroup.closure T
<VAR>G : Type u_2<VAR>Group G<VAR>H K : Subgroup G<GOAL>H ⊔ K = Subgroup.closure (↑H * ↑K)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H ⊔ K = AddSubgroup.closure (↑H + ↑K)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<VAR>N : AddSubgroup G<VAR>hN : N.Normal<GOAL>s + ↑N = ↑N + s
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<VAR>N : Subgroup G<VAR>hN : N.Normal<GOAL>s * ↑N = ↑N * s
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H N : AddSubgroup G<VAR>hN : N.Normal<GOAL>↑(H ⊔ N) = ↑H + ↑N
<VAR>G : Type u_2<VAR>Group G<VAR>H N : Subgroup G<VAR>hN : N.Normal<GOAL>↑(H ⊔ N) = ↑H * ↑N
<VAR>G : Type u_2<VAR>Group G<VAR>N H : Subgroup G<VAR>N.Normal<GOAL>↑(N ⊔ H) = ↑N * ↑H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>N H : AddSubgroup G<VAR>N.Normal<GOAL>↑(N ⊔ H) = ↑N + ↑H
<VAR>G : Type u_2<VAR>Group G<VAR>A B C : Subgroup G<VAR>h : A ≤ C<GOAL>↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C
<VAR>G : Type u_2<VAR>AddGroup G<VAR>A B C : AddSubgroup G<VAR>h : A ≤ C<GOAL>↑A + ↑(B ⊓ C) = (↑A + ↑B) ∩ ↑C
<VAR>G : Type u_2<VAR>AddGroup G<VAR>A B C : AddSubgroup G<VAR>h : C ≤ A<GOAL>↑(A ⊓ B) + ↑C = ↑A ∩ (↑B + ↑C)
<VAR>G : Type u_2<VAR>Group G<VAR>A B C : Subgroup G<VAR>h : C ≤ A<GOAL>↑(A ⊓ B) * ↑C = ↑A ∩ (↑B * ↑C)
<VAR>G : Type u_2<VAR>Group G<VAR>g : G<VAR>h : Gᵐᵒᵖ<VAR>s : Set G<GOAL>(fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>g : G<VAR>h : Gᵃᵒᵖ<VAR>s : Set G<GOAL>(fun y => h +ᵥ y) '' ((fun x => g + x) ⁻¹' s) = (fun x => g + x) ⁻¹' ((fun y => h +ᵥ y) '' s)
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>h : ↥H.op<VAR>s : Set G<GOAL>(fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<VAR>h : ↥H.op<VAR>s : Set G<GOAL>(fun y => h +ᵥ y) '' ((fun x => g + x) ⁻¹' s) = (fun x => g + x) ⁻¹' ((fun y => h +ᵥ y) '' s)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S : Subgroup G<GOAL>a • S = Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S : Subgroup G<GOAL>↑(a • S) = a • ↑S
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S : Subgroup G<GOAL>(a • S).toSubmonoid = a • S.toSubmonoid
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>m : G<VAR>a : α<VAR>S : Subgroup G<GOAL>m ∈ S → a • m ∈ a • S
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>m : G<VAR>a : α<VAR>S : Subgroup G<GOAL>m ∈ a • S ↔ ∃ s ∈ S, a • s = m
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>a : α<GOAL>a • ⊥ = ⊥
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S T : Subgroup G<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Monoid α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>s : Set G<GOAL>a • Subgroup.closure s = Subgroup.closure (a • s)
<VAR>G : Type u_2<VAR>Group G<VAR>P H : Subgroup G<VAR>hP : P ≤ H<VAR>h : ↥H<GOAL>MulAut.conj ↑h • P ≤ H
<VAR>G : Type u_2<VAR>Group G<VAR>P H : Subgroup G<VAR>hP : P ≤ H<VAR>h : ↥H<GOAL>MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S : Subgroup G<VAR>x : G<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S : Subgroup G<VAR>x : G<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S : Subgroup G<VAR>x : G<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S T : Subgroup G<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S T : Subgroup G<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S T : Subgroup G<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>S T : Subgroup G<GOAL>a • (S ⊓ T) = a • S ⊓ a • T
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>H : Subgroup G<VAR>x : ↑↑H.toSubmonoid<GOAL>↑((Subgroup.equivSMul a H) x) = a • ↑x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>Group α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>H : Subgroup G<VAR>y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid)<GOAL>↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>h : G<VAR>hh : h ∈ H<GOAL>↑H * {h} = ↑H
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>h : G<VAR>hh : h ∈ H<GOAL>{h} * ↑H = ↑H