ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_5<VAR>Group G<VAR>H : Subgroup G<VAR>hH : H.Normal<VAR>g : ConjAct G<GOAL>g • H = H
<VAR>G : Type u_2<VAR>Group G<VAR>g : G<VAR>H : Subgroup G<VAR>h : H.Normal<GOAL>MulAut.conj g • H = H
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>GroupWithZero α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>ha : a ≠ 0<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>GroupWithZero α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>ha : a ≠ 0<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>GroupWithZero α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>ha : a ≠ 0<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>GroupWithZero α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>ha : a ≠ 0<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>GroupWithZero α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>ha : a ≠ 0<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>GroupWithZero α<VAR>MulDistribMulAction α G<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : Subgroup G<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubgroup A<GOAL>a • S = AddSubgroup.map ((DistribMulAction.toAddMonoidEnd α A) a) S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubgroup A<GOAL>↑(a • S) = a • ↑S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubgroup A<GOAL>(a • S).toAddSubmonoid = a • S.toAddSubmonoid
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>m : A<VAR>a : α<VAR>S : AddSubgroup A<GOAL>m ∈ S → a • m ∈ a • S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>m : A<VAR>a : α<VAR>S : AddSubgroup A<GOAL>m ∈ a • S ↔ ∃ s ∈ S, a • s = m
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubgroup A<VAR>x : A<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubgroup A<VAR>x : A<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubgroup A<VAR>x : A<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubgroup A<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubgroup A<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubgroup A<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : AddSubgroup A<VAR>x : A<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : AddSubgroup A<VAR>x : A<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : AddSubgroup A<VAR>x : A<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : AddSubgroup A<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : AddSubgroup A<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>A : Type u_3<VAR>AddGroup A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : AddSubgroup A<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>α : Type u<VAR>x : α<VAR>hx : ↑x ≠ 0<GOAL>WithZero.unzero hx = x
<VAR>α : Type u<VAR>x : α<VAR>hx : ↑x ≠ 1<GOAL>WithOne.unone hx = x
<VAR>α : Type u<VAR>x : WithZero α<VAR>hx : x ≠ 0<GOAL>↑(WithZero.unzero hx) = x
<VAR>α : Type u<VAR>x : WithOne α<VAR>hx : x ≠ 1<GOAL>↑(WithOne.unone hx) = x
<VAR>α : Type u<VAR>a : α<GOAL>↑a ≠ 0
<VAR>α : Type u<VAR>a : α<GOAL>↑a ≠ 1
<VAR>α : Type u<VAR>a : α<GOAL>0 ≠ ↑a
<VAR>α : Type u<VAR>a : α<GOAL>1 ≠ ↑a
<VAR>α : Type u<VAR>x : WithOne α<GOAL>x ≠ 1 ↔ ∃ a, ↑a = x
<VAR>α : Type u<VAR>x : WithZero α<GOAL>x ≠ 0 ↔ ∃ a, ↑a = x
<VAR>α : Type u<VAR>a b : α<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u<VAR>P : WithOne α → Prop<VAR>x : WithOne α<GOAL>P 1 → (∀ (a : α), P ↑a) → P x
<VAR>α : Type u<VAR>P : WithZero α → Prop<VAR>x : WithZero α<GOAL>P 0 → (∀ (a : α), P ↑a) → P x
<VAR>α : Type u<VAR>Mul α<VAR>a b : α<GOAL>↑(a * b) = ↑a * ↑b
<VAR>α : Type u<VAR>Inv α<VAR>a : α<GOAL>↑a⁻¹ = (↑a)⁻¹
<VAR>α : Type u<VAR>Neg α<VAR>a : α<GOAL>↑(-a) = -↑a
<VAR>M : Type u_1<VAR>B : Type u_3<VAR>AddMonoid M<VAR>SetLike B M<VAR>AddSubmonoidClass B M<VAR>S : B<VAR>l : List ↥S<GOAL>↑l.sum = (List.map Subtype.val l).sum
<VAR>M : Type u_1<VAR>B : Type u_3<VAR>Monoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>S : B<VAR>l : List ↥S<GOAL>↑l.prod = (List.map Subtype.val l).prod
<VAR>B : Type u_3<VAR>S : B<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>SetLike B M<VAR>AddSubmonoidClass B M<VAR>m : Multiset ↥S<GOAL>↑m.sum = (Multiset.map Subtype.val m).sum
<VAR>B : Type u_3<VAR>S : B<VAR>M : Type u_4<VAR>CommMonoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>m : Multiset ↥S<GOAL>↑m.prod = (Multiset.map Subtype.val m).prod
<VAR>B : Type u_3<VAR>S : B<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>SetLike B M<VAR>AddSubmonoidClass B M<VAR>f : ι → ↥S<VAR>s : Finset ι<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>B : Type u_3<VAR>S : B<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>CommMonoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>f : ι → ↥S<VAR>s : Finset ι<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>M : Type u_1<VAR>B : Type u_3<VAR>Monoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>S : B<VAR>l : List M<VAR>hl : ∀ x ∈ l, x ∈ S<GOAL>l.prod ∈ S
<VAR>M : Type u_1<VAR>B : Type u_3<VAR>AddMonoid M<VAR>SetLike B M<VAR>AddSubmonoidClass B M<VAR>S : B<VAR>l : List M<VAR>hl : ∀ x ∈ l, x ∈ S<GOAL>l.sum ∈ S
<VAR>B : Type u_3<VAR>S : B<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>SetLike B M<VAR>AddSubmonoidClass B M<VAR>m : Multiset M<VAR>hm : ∀ a ∈ m, a ∈ S<GOAL>m.sum ∈ S
<VAR>B : Type u_3<VAR>S : B<VAR>M : Type u_4<VAR>CommMonoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>m : Multiset M<VAR>hm : ∀ a ∈ m, a ∈ S<GOAL>m.prod ∈ S
<VAR>B : Type u_3<VAR>S : B<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>SetLike B M<VAR>AddSubmonoidClass B M<VAR>ι : Type u_5<VAR>t : Finset ι<VAR>f : ι → M<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∑ c ∈ t, f c ∈ S
<VAR>B : Type u_3<VAR>S : B<VAR>M : Type u_4<VAR>CommMonoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>ι : Type u_5<VAR>t : Finset ι<VAR>f : ι → M<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∏ c ∈ t, f c ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Submonoid M<VAR>l : List ↥s<GOAL>↑l.prod = (List.map Subtype.val l).prod
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : AddSubmonoid M<VAR>l : List ↥s<GOAL>↑l.sum = (List.map Subtype.val l).sum
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>m : Multiset ↥S<GOAL>↑m.sum = (Multiset.map Subtype.val m).sum
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>m : Multiset ↥S<GOAL>↑m.prod = (Multiset.map Subtype.val m).prod
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>f : ι → ↥S<VAR>s : Finset ι<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>f : ι → ↥S<VAR>s : Finset ι<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Submonoid M<VAR>l : List M<VAR>hl : ∀ x ∈ l, x ∈ s<GOAL>l.prod ∈ s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : AddSubmonoid M<VAR>l : List M<VAR>hl : ∀ x ∈ l, x ∈ s<GOAL>l.sum ∈ s
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>m : Multiset M<VAR>hm : ∀ a ∈ m, a ∈ S<GOAL>m.prod ∈ S
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>m : Multiset M<VAR>hm : ∀ a ∈ m, a ∈ S<GOAL>m.sum ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>m : Multiset M<VAR>comm : {x | x ∈ m}.Pairwise AddCommute<VAR>h : ∀ x ∈ m, x ∈ S<GOAL>m.noncommSum comm ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>m : Multiset M<VAR>comm : {x | x ∈ m}.Pairwise Commute<VAR>h : ∀ x ∈ m, x ∈ S<GOAL>m.noncommProd comm ∈ S
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>ι : Type u_5<VAR>t : Finset ι<VAR>f : ι → M<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∑ c ∈ t, f c ∈ S
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>ι : Type u_5<VAR>t : Finset ι<VAR>f : ι → M<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∏ c ∈ t, f c ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → M<VAR>comm : (↑t).Pairwise fun a b => Commute (f a) (f b)<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>t.noncommProd f comm ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → M<VAR>comm : (↑t).Pairwise fun a b => AddCommute (f a) (f b)<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>t.noncommSum f comm ∈ S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → AddSubmonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>S : ι → AddSubmonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S T : Submonoid M<VAR>x : M<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S T : AddSubmonoid M<VAR>x : M<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S T : Submonoid M<VAR>x : M<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S T : AddSubmonoid M<VAR>x : M<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S T : AddSubmonoid M<VAR>x y : M<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x + y ∈ S ⊔ T
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S T : Submonoid M<VAR>x y : M<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>i : ι<VAR>x : M<GOAL>x ∈ S i → x ∈ iSup S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>S : ι → AddSubmonoid M<VAR>i : ι<VAR>x : M<GOAL>x ∈ S i → x ∈ iSup S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<VAR>s : AddSubmonoid M<VAR>hs : s ∈ S<VAR>x : M<GOAL>x ∈ s → x ∈ sSup S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<VAR>s : Submonoid M<VAR>hs : s ∈ S<VAR>x : M<GOAL>x ∈ s → x ∈ sSup S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>S : ι → AddSubmonoid M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 0<VAR>mul : ∀ (x y : M), C x → C y → C (x + y)<GOAL>C x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<GOAL>C x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 1 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<GOAL>C x hx
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>S : ι → AddSubmonoid M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>one : C 0 ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<GOAL>C x hx
<VAR>α : Type u_4<GOAL>AddSubmonoid.closure (Set.range FreeAddMonoid.of) = ⊤
<VAR>α : Type u_4<GOAL>Submonoid.closure (Set.range FreeMonoid.of) = ⊤
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>Submonoid.closure {x} = MonoidHom.mrange ((powersHom M) x)
<VAR>M : Type u_1<VAR>Monoid M<VAR>x y : M<GOAL>y ∈ Submonoid.closure {x} ↔ ∃ n, x ^ n = y
<VAR>M : Type u_1<VAR>Monoid M<VAR>y : M<GOAL>y ∈ Submonoid.closure {y}
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Submonoid.closure {1} = ⊥
<VAR>M : Type u_1<VAR>Monoid M<GOAL>∀ {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>∀ {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>Fintype ↥S<VAR>h : Fintype.card ↥S ≤ 1<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>Fintype ↥S<VAR>h : Fintype.card ↥S ≤ 1<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>Fintype ↥S<VAR>h : Fintype.card ↥S = 1<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>Fintype ↥S<VAR>h : Fintype.card ↥S = 1<GOAL>S = ⊥
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>Fintype ↥S<GOAL>Fintype.card ↥S ≤ 1 ↔ S = ⊥
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>Fintype ↥S<GOAL>Fintype.card ↥S ≤ 1 ↔ S = ⊥
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>Fintype ↥S<GOAL>S = ⊥ ↔ Fintype.card ↥S = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>Fintype ↥S<GOAL>S = ⊥ ↔ Fintype.card ↥S = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>α : Type u_4<VAR>f : α → M<GOAL>AddMonoidHom.mrange (FreeAddMonoid.lift f) = AddSubmonoid.closure (Set.range f)
<VAR>M : Type u_1<VAR>Monoid M<VAR>α : Type u_4<VAR>f : α → M<GOAL>MonoidHom.mrange (FreeMonoid.lift f) = Submonoid.closure (Set.range f)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>AddSubmonoid.closure s = AddMonoidHom.mrange (FreeAddMonoid.lift Subtype.val)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>Submonoid.closure s = MonoidHom.mrange (FreeMonoid.lift Subtype.val)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>↑(Submonoid.closure s) = List.prod '' {l | ∀ x ∈ l, x ∈ s}
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>↑(AddSubmonoid.closure s) = List.sum '' {l | ∀ x ∈ l, x ∈ s}
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ AddSubmonoid.closure s<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.sum = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ Submonoid.closure s<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ Submonoid.closure s<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ AddSubmonoid.closure s<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.sum = x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>p : (m : M) → m ∈ AddSubmonoid.closure s → Prop<VAR>one : p 0 ⋯<VAR>mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ AddSubmonoid.closure s), p y hy → p (x + y) ⋯<VAR>x : M<VAR>h : x ∈ AddSubmonoid.closure s<GOAL>p x h
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>p : (m : M) → m ∈ Submonoid.closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ Submonoid.closure s), p y hy → p (x * y) ⋯<VAR>x : M<VAR>h : x ∈ Submonoid.closure s<GOAL>p x h
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>p : M → Prop<VAR>hs : Submonoid.closure s = ⊤<VAR>x : M<VAR>one : p 1<VAR>mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>p : M → Prop<VAR>hs : AddSubmonoid.closure s = ⊤<VAR>x : M<VAR>one : p 0<VAR>mul : ∀ x ∈ s, ∀ (y : M), p y → p (x + y)<GOAL>p x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>p : (m : M) → m ∈ AddSubmonoid.closure s → Prop<VAR>one : p 0 ⋯<VAR>mul_right : ∀ (x : M) (hx : x ∈ AddSubmonoid.closure s) (y : M) (hy : y ∈ s), p x hx → p (x + y) ⋯<VAR>x : M<VAR>h : x ∈ AddSubmonoid.closure s<GOAL>p x h
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>p : (m : M) → m ∈ Submonoid.closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_right : ∀ (x : M) (hx : x ∈ Submonoid.closure s) (y : M) (hy : y ∈ s), p x hx → p (x * y) ⋯<VAR>x : M<VAR>h : x ∈ Submonoid.closure s<GOAL>p x h
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>p : M → Prop<VAR>hs : Submonoid.closure s = ⊤<VAR>x : M<VAR>H1 : p 1<VAR>Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>p : M → Prop<VAR>hs : AddSubmonoid.closure s = ⊤<VAR>x : M<VAR>H1 : p 0<VAR>Hmul : ∀ (x y : M), y ∈ s → p x → p (x + y)<GOAL>p x
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : M<GOAL>n ∈ Submonoid.powers n
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>↑(Submonoid.powers x) = Set.range fun n => x ^ n
<VAR>M : Type u_1<VAR>Monoid M<VAR>x z : M<GOAL>x ∈ Submonoid.powers z ↔ ∃ n, z ^ n = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : M<GOAL>Submonoid.powers n = Submonoid.closure {n}
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : M<VAR>P : Submonoid M<GOAL>Submonoid.powers n ≤ P ↔ n ∈ P
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Submonoid.powers 1 = ⊥
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : M<VAR>m : ℕ<GOAL>↑(Submonoid.pow n m) = n ^ m
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : M<VAR>m : ℕ<GOAL>Submonoid.pow n m = ⟨n ^ m, ⋯⟩
<VAR>M : Type u_1<VAR>Monoid M<VAR>DecidableEq M<VAR>n : M<VAR>p : ↥(Submonoid.powers n)<GOAL>Submonoid.pow n (Submonoid.log p) = p
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : M<GOAL>(Function.Injective fun m => n ^ m) ↔ Function.Injective (Submonoid.pow n)
<VAR>M : Type u_1<VAR>Monoid M<VAR>DecidableEq M<VAR>n : M<VAR>h : Function.Injective fun m => n ^ m<VAR>m : ℕ<GOAL>Submonoid.log (Submonoid.pow n m) = m
<VAR>M : Type u_1<VAR>Monoid M<VAR>DecidableEq M<VAR>n : M<VAR>h : Function.Injective fun m => n ^ m<VAR>m : Multiplicative ℕ<GOAL>(Submonoid.powLogEquiv h) m = Submonoid.pow n (Multiplicative.toAdd m)
<VAR>M : Type u_1<VAR>Monoid M<VAR>DecidableEq M<VAR>n : M<VAR>h : Function.Injective fun m => n ^ m<VAR>m : ↥(Submonoid.powers n)<GOAL>(Submonoid.powLogEquiv h).symm m = Multiplicative.ofAdd (Submonoid.log m)
<VAR>M : Type u_1<VAR>Monoid M<VAR>DecidableEq M<VAR>n : M<VAR>h : Function.Injective fun m => n ^ m<VAR>x y : ↥(Submonoid.powers n)<GOAL>Submonoid.log (x * y) = Submonoid.log x + Submonoid.log y
<VAR>x : ℤ<VAR>h : 1 < x.natAbs<VAR>m : ℕ<GOAL>Submonoid.log (Submonoid.pow x m) = m
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_4<VAR>F : Type u_5<VAR>Monoid N<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<VAR>m : M<GOAL>Submonoid.map f (Submonoid.powers m) = Submonoid.powers (f m)
<VAR>M : Type u_1<VAR>N : Type u_4<VAR>α : Type u_5<VAR>Monoid M<VAR>MulAction M N<VAR>SMul N α<VAR>MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z<GOAL>IsScalarTower M N α
<VAR>M : Type u_1<VAR>N : Type u_4<VAR>α : Type u_5<VAR>AddMonoid M<VAR>AddAction M N<VAR>VAdd N α<VAR>AddAction M α<VAR>s : Set M<VAR>htop : AddSubmonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)<GOAL>VAddAssocClass M N α
<VAR>M : Type u_1<VAR>N : Type u_4<VAR>α : Type u_5<VAR>AddMonoid M<VAR>VAdd N α<VAR>AddAction M α<VAR>s : Set M<VAR>htop : AddSubmonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), x +ᵥ (y +ᵥ z) = y +ᵥ (x +ᵥ z)<GOAL>VAddCommClass M N α
<VAR>M : Type u_1<VAR>N : Type u_4<VAR>α : Type u_5<VAR>Monoid M<VAR>SMul N α<VAR>MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z<GOAL>SMulCommClass M N α
<VAR>N : Type u_4<VAR>CommMonoid N<VAR>s t : Submonoid N<GOAL>s ⊔ t = MonoidHom.mrange (s.subtype.coprod t.subtype)
<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>s t : AddSubmonoid N<GOAL>s ⊔ t = AddMonoidHom.mrange (s.subtype.coprod t.subtype)
<VAR>N : Type u_4<VAR>CommMonoid N<VAR>s t : Submonoid N<VAR>x : N<GOAL>x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>s t : AddSubmonoid N<VAR>x : N<GOAL>x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>x : A<GOAL>AddSubmonoid.closure {x} = AddMonoidHom.mrange ((multiplesHom A) x)
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>x y : A<GOAL>y ∈ AddSubmonoid.closure {x} ↔ ∃ n, n • x = y
<VAR>A : Type u_2<VAR>AddMonoid A<GOAL>AddSubmonoid.closure {0} = ⊥
<VAR>M : Type u_1<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>SetLike M R<VAR>MulMemClass M R<VAR>S : M<VAR>a b : R<VAR>ha : a ∈ AddSubmonoid.closure ↑S<VAR>hb : b ∈ S<GOAL>a * b ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>SetLike M R<VAR>MulMemClass M R<VAR>S : M<VAR>a b : R<VAR>ha : a ∈ AddSubmonoid.closure ↑S<VAR>hb : b ∈ AddSubmonoid.closure ↑S<GOAL>a * b ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>SetLike M R<VAR>MulMemClass M R<VAR>S : M<VAR>a b : R<VAR>ha : a ∈ S<VAR>hb : b ∈ AddSubmonoid.closure ↑S<GOAL>a * b ∈ AddSubmonoid.closure ↑S
<VAR>A : Type u_4<VAR>CommMonoid A<VAR>a b c : A<GOAL>c ∈ Submonoid.closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c
<VAR>A : Type u_4<VAR>AddCommMonoid A<VAR>a b c : A<GOAL>c ∈ AddSubmonoid.closure {a, b} ↔ ∃ m n, m • a + n • b = c
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>x : A<GOAL>⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))
<VAR>M : Type u_2<VAR>Mul M<VAR>Pow M ℕ+<VAR>self : PNatPowAssoc M<VAR>x : M<GOAL>x ^ 1 = x
<VAR>M : Type u_2<VAR>Mul M<VAR>Pow M ℕ+<VAR>self : PNatPowAssoc M<VAR>k n : ℕ+<VAR>x : M<GOAL>x ^ (k + n) = x ^ k * x ^ n
<VAR>M : Type u_1<VAR>Mul M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>k n : ℕ+<VAR>x : M<GOAL>x ^ (k + n) = x ^ k * x ^ n
<VAR>M : Type u_1<VAR>Mul M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>x : M<GOAL>x ^ 1 = x
<VAR>M : Type u_1<VAR>Mul M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>k m n : ℕ+<VAR>x : M<GOAL>x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
<VAR>M : Type u_1<VAR>Mul M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>m n : ℕ+<VAR>x : M<GOAL>x ^ m * x ^ n = x ^ n * x ^ m
<VAR>M : Type u_1<VAR>Mul M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>x : M<VAR>m n : ℕ+<GOAL>x ^ (m * n) = (x ^ m) ^ n
<VAR>M : Type u_1<VAR>Mul M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>x : M<VAR>m n : ℕ+<GOAL>x ^ (m * n) = (x ^ n) ^ m
<VAR>M : Type u_1<VAR>Monoid M<VAR>Pow M ℕ+<VAR>PNatPowAssoc M<VAR>x : M<VAR>n : ℕ+<GOAL>x ^ n = x ^ ↑n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>AddZeroClass H<VAR>f : G ≃+ H<VAR>a : Multiplicative H<GOAL>(AddEquiv.toMultiplicative f).symm a = (AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>AddZeroClass H<VAR>f : Multiplicative G ≃* Multiplicative H<VAR>a : H<GOAL>(AddEquiv.toMultiplicative.symm f).symm a = (AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>AddZeroClass H<VAR>f : Multiplicative G ≃* Multiplicative H<VAR>a : G<GOAL>(AddEquiv.toMultiplicative.symm f) a = (AddMonoidHom.toMultiplicative.symm f.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>AddZeroClass H<VAR>f : G ≃+ H<VAR>a : Multiplicative G<GOAL>(AddEquiv.toMultiplicative f) a = (AddMonoidHom.toMultiplicative f.toAddMonoidHom) a