ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite ↥H<GOAL>Nat.card ↥H = Nat.card G ↔ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite ↥H<GOAL>Nat.card ↥H = Nat.card G ↔ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite G<VAR>h : Nat.card G ≤ Nat.card ↥H<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite G<VAR>h : Nat.card G ≤ Nat.card ↥H<GOAL>H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite ↥H<VAR>h : Nat.card ↥H ≤ 1<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite ↥H<VAR>h : Nat.card ↥H ≤ 1<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>h : Nat.card ↥H = 1<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>h : Nat.card ↥H = 1<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite ↥H<GOAL>Nat.card ↥H ≤ 1 ↔ H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite ↥H<GOAL>Nat.card ↥H ≤ 1 ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H = ⊥ ↔ Nat.card ↥H = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H = ⊥ ↔ Nat.card ↥H = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite ↥H<GOAL>1 < Nat.card ↥H ↔ H ≠ ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite ↥H<GOAL>1 < Nat.card ↥H ↔ H ≠ ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Finite G<GOAL>Nat.card ↥H ≤ Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Finite G<GOAL>Nat.card ↥H ≤ Nat.card G
<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>(i : η) → Group (f i)<VAR>DecidableEq η<VAR>I : Finset η<VAR>H : Subgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h1 : ∀ i ∉ I, x i = 1<VAR>h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H<GOAL>x ∈ H
<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>(i : η) → AddGroup (f i)<VAR>DecidableEq η<VAR>I : Finset η<VAR>H : AddSubgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h1 : ∀ i ∉ I, x i = 0<VAR>h2 : ∀ i ∈ I, Pi.single i (x i) ∈ H<GOAL>x ∈ H
<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>(i : η) → AddGroup (f i)<VAR>Finite η<VAR>DecidableEq η<VAR>H : AddSubgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h : ∀ (i : η), Pi.single i (x i) ∈ H<GOAL>x ∈ H
<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>(i : η) → Group (f i)<VAR>Finite η<VAR>DecidableEq η<VAR>H : Subgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H<GOAL>x ∈ H
<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>(i : η) → AddGroup (f i)<VAR>DecidableEq η<VAR>Finite η<VAR>H : (i : η) → AddSubgroup (f i)<VAR>J : AddSubgroup ((i : η) → f i)<GOAL>AddSubgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubgroup.map (AddMonoidHom.single f i) (H i) ≤ J
<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>(i : η) → Group (f i)<VAR>DecidableEq η<VAR>Finite η<VAR>H : (i : η) → Subgroup (f i)<VAR>J : Subgroup ((i : η) → f i)<GOAL>Subgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), Subgroup.map (MonoidHom.mulSingle f i) (H i) ≤ J
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>Finite ↑S<VAR>x : G<VAR>h : ∀ n ∈ S, x * n * x⁻¹ ∈ S<GOAL>x ∈ Subgroup.setNormalizer S
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>ifp_n : GenContFract.IntFractPair K<VAR>nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n<GOAL>0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>ifp_n : GenContFract.IntFractPair K<VAR>nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n<GOAL>0 ≤ ifp_n.fr
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>ifp_n : GenContFract.IntFractPair K<VAR>nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n<GOAL>ifp_n.fr < 1
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>ifp_succ_n : GenContFract.IntFractPair K<VAR>succ_nth_stream_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>1 ≤ ifp_succ_n.b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>ifp_n ifp_succ_n : GenContFract.IntFractPair K<VAR>nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n<VAR>succ_nth_stream_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>↑ifp_succ_n.b ≤ ifp_n.fr⁻¹
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b<GOAL>1 ≤ b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>gp : GenContFract.Pair K<VAR>nth_s_eq : (GenContFract.of v).s.get? n = some gp<GOAL>gp.a = 1 ∧ ∃ z, gp.b = ↑z
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>a : K<VAR>nth_partNum_eq : (GenContFract.of v).partNums.get? n = some a<GOAL>a = 1
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b<GOAL>∃ z, b = ↑z
<VAR>K : Type u_1<VAR>v : K<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>(GenContFract.of v).IsSimpContFract
<VAR>K : Type u_1<VAR>v : K<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>(SimpContFract.of v).IsContFract
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>n ≤ 1 ∨ ¬(GenContFract.of v).TerminatedAt (n - 2) → ↑(Nat.fib n) ≤ ((GenContFract.of v).contsAux n).b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>hyp : n = 0 ∨ ¬(GenContFract.of v).TerminatedAt (n - 1)<GOAL>↑(Nat.fib (n + 1)) ≤ (GenContFract.of v).dens n
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>0 ≤ ((GenContFract.of v).contsAux n).b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>0 ≤ (GenContFract.of v).dens n
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b<GOAL>b * ((GenContFract.of v).contsAux (n + 1)).b ≤ ((GenContFract.of v).contsAux (n + 2)).b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>b : K<VAR>nth_partDenom_eq : (GenContFract.of v).partDens.get? n = some b<GOAL>b * (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>(GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>ifp : GenContFract.IntFractPair K<VAR>stream_nth_eq : GenContFract.IntFractPair.stream v n = some ifp<GOAL>let g := GenContFract.of v;
v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>not_terminatedAt_n : ¬(GenContFract.of v).TerminatedAt n<GOAL>|v - (GenContFract.of v).convs n| ≤ 1 / ((GenContFract.of v).dens n * (GenContFract.of v).dens (n + 1))
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b<GOAL>|v - (GenContFract.of v).convs n| ≤ 1 / (b * (GenContFract.of v).dens n * (GenContFract.of v).dens n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>One γ<VAR>f : α × β → γ<VAR>a : α<VAR>h : (Function.mulSupport f).Finite<GOAL>(Function.mulSupport fun b => f (a, b)).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Zero γ<VAR>f : α × β → γ<VAR>a : α<VAR>h : (Function.support f).Finite<GOAL>(Function.support fun b => f (a, b)).Finite
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>x : α × β<GOAL>(a • x).1 = a • x.1
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>x : α × β<GOAL>(a +ᵥ x).1 = a +ᵥ x.1
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>x : α × β<GOAL>(a • x).2 = a • x.2
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>x : α × β<GOAL>(a +ᵥ x).2 = a +ᵥ x.2
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>b : α<VAR>c : β<GOAL>a • (b, c) = (a • b, a • c)
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>b : α<VAR>c : β<GOAL>a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>x : α × β<GOAL>a +ᵥ x = (a +ᵥ x.1, a +ᵥ x.2)
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>x : α × β<GOAL>a • x = (a • x.1, a • x.2)
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>VAdd M α<VAR>VAdd M β<VAR>a : M<VAR>x : α × β<GOAL>(a +ᵥ x).swap = a +ᵥ x.swap
<VAR>M : Type u_1<VAR>α : Type u_5<VAR>β : Type u_6<VAR>SMul M α<VAR>SMul M β<VAR>a : M<VAR>x : α × β<GOAL>(a • x).swap = a • x.swap
<VAR>E : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Pow α E<VAR>Pow β E<VAR>p : α × β<VAR>c : E<GOAL>(p ^ c).1 = p.1 ^ c
<VAR>E : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Pow α E<VAR>Pow β E<VAR>p : α × β<VAR>c : E<GOAL>(p ^ c).2 = p.2 ^ c
<VAR>E : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Pow α E<VAR>Pow β E<VAR>c : E<VAR>a : α<VAR>b : β<GOAL>(a, b) ^ c = (a ^ c, b ^ c)
<VAR>E : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Pow α E<VAR>Pow β E<VAR>p : α × β<VAR>c : E<GOAL>p ^ c = (p.1 ^ c, p.2 ^ c)
<VAR>E : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Pow α E<VAR>Pow β E<VAR>p : α × β<VAR>c : E<GOAL>(p ^ c).swap = p.swap ^ c
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Monoid α<VAR>Mul β<VAR>MulAction α β<VAR>IsScalarTower α β β<VAR>SMulCommClass α β β<VAR>a : α × β<GOAL>smulMulHom a = a.1 • a.2
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Monoid α<VAR>MulOneClass β<VAR>MulAction α β<VAR>IsScalarTower α β β<VAR>SMulCommClass α β β<GOAL>∀ (a : α × β), smulMonoidHom a = smulMulHom.toFun a
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>s t : Set M<VAR>S : AddSubmonoid M<VAR>hs : s ⊆ ↑S<VAR>ht : t ⊆ ↑S<GOAL>s + t ⊆ ↑S
<VAR>M : Type u_3<VAR>Monoid M<VAR>s t : Set M<VAR>S : Submonoid M<VAR>hs : s ⊆ ↑S<VAR>ht : t ⊆ ↑S<GOAL>s * t ⊆ ↑S
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>s t u : Set M<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>s + t ⊆ ↑(AddSubmonoid.closure u)
<VAR>M : Type u_3<VAR>Monoid M<VAR>s t u : Set M<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>s * t ⊆ ↑(Submonoid.closure u)
<VAR>M : Type u_3<VAR>Monoid M<VAR>s : Submonoid M<GOAL>↑s * ↑s = ↑s
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>s : AddSubmonoid M<GOAL>↑s + ↑s = ↑s
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>S T : Set M<GOAL>AddSubmonoid.closure (S + T) ≤ AddSubmonoid.closure S ⊔ AddSubmonoid.closure T
<VAR>M : Type u_3<VAR>Monoid M<VAR>S T : Set M<GOAL>Submonoid.closure (S * T) ≤ Submonoid.closure S ⊔ Submonoid.closure T
<VAR>M : Type u_3<VAR>Monoid M<VAR>H K : Submonoid M<GOAL>H ⊔ K = Submonoid.closure (↑H * ↑K)
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>H K : AddSubmonoid M<GOAL>H ⊔ K = AddSubmonoid.closure (↑H + ↑K)
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>N : Type u_6<VAR>AddCommMonoid N<VAR>AddAction M N<VAR>VAddAssocClass M N N<VAR>r : M<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ AddSubmonoid.closure s<GOAL>∃ n, n • r +ᵥ x ∈ AddSubmonoid.closure (r +ᵥ s)
<VAR>M : Type u_3<VAR>Monoid M<VAR>N : Type u_6<VAR>CommMonoid N<VAR>MulAction M N<VAR>IsScalarTower M N N<VAR>r : M<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ Submonoid.closure s<GOAL>∃ n, r ^ n • x ∈ Submonoid.closure (r • s)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Submonoid G<GOAL>↑S⁻¹ = (↑S)⁻¹
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : AddSubmonoid G<GOAL>↑(-S) = -↑S
<VAR>G : Type u_2<VAR>AddGroup G<VAR>g : G<VAR>S : AddSubmonoid G<GOAL>g ∈ -S ↔ -g ∈ S
<VAR>G : Type u_2<VAR>Group G<VAR>g : G<VAR>S : Submonoid G<GOAL>g ∈ S⁻¹ ↔ g⁻¹ ∈ S
<VAR>G : Type u_2<VAR>Group G<VAR>S T : Submonoid G<GOAL>S⁻¹ ≤ T⁻¹ ↔ S ≤ T
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S T : AddSubmonoid G<GOAL>-S ≤ -T ↔ S ≤ T
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S T : AddSubmonoid G<GOAL>-S ≤ T ↔ S ≤ -T
<VAR>G : Type u_2<VAR>Group G<VAR>S T : Submonoid G<GOAL>S⁻¹ ≤ T ↔ S ≤ T⁻¹
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>∀ (a : AddSubmonoid G), ↑((RelIso.symm AddSubmonoid.negOrderIso) a) = -↑a
<VAR>G : Type u_2<VAR>Group G<GOAL>∀ (a : Submonoid G), ↑(Submonoid.invOrderIso a) = (↑a)⁻¹
<VAR>G : Type u_2<VAR>Group G<GOAL>∀ (a : Submonoid G), ↑((RelIso.symm Submonoid.invOrderIso) a) = (↑a)⁻¹
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>∀ (a : AddSubmonoid G), ↑(AddSubmonoid.negOrderIso a) = -↑a
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<GOAL>AddSubmonoid.closure (-s) = -AddSubmonoid.closure s
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<GOAL>Submonoid.closure s⁻¹ = (Submonoid.closure s)⁻¹
<VAR>G : Type u_2<VAR>Group G<VAR>S T : Submonoid G<GOAL>(S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S T : AddSubmonoid G<GOAL>-(S ⊓ T) = -S ⊓ -T
<VAR>G : Type u_2<VAR>Group G<VAR>S T : Submonoid G<GOAL>(S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S T : AddSubmonoid G<GOAL>-(S ⊔ T) = -S ⊔ -T
<VAR>G : Type u_2<VAR>Group G<GOAL>⊥⁻¹ = ⊥
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>-⊥ = ⊥
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>-⊤ = ⊤
<VAR>G : Type u_2<VAR>Group G<GOAL>⊤⁻¹ = ⊤
<VAR>G : Type u_2<VAR>Group G<VAR>ι : Sort u_6<VAR>S : ι → Submonoid G<GOAL>(⨅ i, S i)⁻¹ = ⨅ i, (S i)⁻¹
<VAR>G : Type u_2<VAR>AddGroup G<VAR>ι : Sort u_6<VAR>S : ι → AddSubmonoid G<GOAL>-⨅ i, S i = ⨅ i, -S i
<VAR>G : Type u_2<VAR>AddGroup G<VAR>ι : Sort u_6<VAR>S : ι → AddSubmonoid G<GOAL>-⨆ i, S i = ⨆ i, -S i
<VAR>G : Type u_2<VAR>Group G<VAR>ι : Sort u_6<VAR>S : ι → Submonoid G<GOAL>(⨆ i, S i)⁻¹ = ⨆ i, (S i)⁻¹
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S : Submonoid M<GOAL>↑(a • S) = a • ↑S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>m : M<VAR>a : α<VAR>S : Submonoid M<GOAL>m ∈ S → a • m ∈ a • S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>m : M<VAR>a : α<VAR>S : Submonoid M<GOAL>m ∈ a • S ↔ ∃ s ∈ S, a • s = m
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>a : α<GOAL>a • ⊥ = ⊥
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S T : Submonoid M<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>s : Set M<GOAL>a • Submonoid.closure s = Submonoid.closure (a • s)
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction α M<VAR>MulDistribMulAction αᵐᵒᵖ M<VAR>IsCentralScalar α M<GOAL>IsCentralScalar α (Submonoid M)
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S : Submonoid M<VAR>x : M<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S : Submonoid M<VAR>x : M<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S : Submonoid M<VAR>x : M<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S T : Submonoid M<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S T : Submonoid M<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>S T : Submonoid M<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>GroupWithZero α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : Submonoid M<VAR>x : M<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>GroupWithZero α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : Submonoid M<VAR>x : M<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>GroupWithZero α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : Submonoid M<VAR>x : M<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>GroupWithZero α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : Submonoid M<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>GroupWithZero α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : Submonoid M<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>GroupWithZero α<VAR>MulDistribMulAction α M<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : Submonoid M<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>G : Type u_6<VAR>Group G<VAR>S : Set G<VAR>x : G<GOAL>x ∈ Submonoid.closure S⁻¹ ↔ x⁻¹ ∈ Submonoid.closure S
<VAR>G : Type u_6<VAR>AddGroup G<VAR>S : Set G<VAR>x : G<GOAL>x ∈ AddSubmonoid.closure (-S) ↔ -x ∈ AddSubmonoid.closure S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubmonoid A<GOAL>↑(a • S) = a • ↑S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>m : A<VAR>a : α<VAR>S : AddSubmonoid A<GOAL>m ∈ S → a • m ∈ a • S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>m : A<VAR>a : α<VAR>S : AddSubmonoid A<GOAL>m ∈ a • S ↔ ∃ s ∈ S, a • s = m
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<GOAL>a • ⊥ = ⊥
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubmonoid A<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>a : α<VAR>s : Set A<GOAL>a • AddSubmonoid.closure s = AddSubmonoid.closure (a • s)
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Monoid α<VAR>DistribMulAction α A<VAR>DistribMulAction αᵐᵒᵖ A<VAR>IsCentralScalar α A<GOAL>IsCentralScalar α (AddSubmonoid A)
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubmonoid A<VAR>x : A<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubmonoid A<VAR>x : A<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S : AddSubmonoid A<VAR>x : A<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubmonoid A<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubmonoid A<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>Group α<VAR>DistribMulAction α A<VAR>a : α<VAR>S T : AddSubmonoid A<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : AddSubmonoid A<VAR>x : A<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : AddSubmonoid A<VAR>x : A<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S : AddSubmonoid A<VAR>x : A<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : AddSubmonoid A<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : AddSubmonoid A<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>A : Type u_5<VAR>AddMonoid A<VAR>GroupWithZero α<VAR>DistribMulAction α A<VAR>a : α<VAR>ha : a ≠ 0<VAR>S T : AddSubmonoid A<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>R : Type u_4<VAR>AddMonoidWithOne R<GOAL>1 = AddMonoidHom.mrange (Nat.castAddMonoidHom R)
<VAR>R : Type u_4<VAR>AddMonoidWithOne R<VAR>n : ℕ<GOAL>↑n ∈ 1
<VAR>R : Type u_4<VAR>AddMonoidWithOne R<VAR>x : R<GOAL>x ∈ 1 ↔ ∃ n, ↑n = x
<VAR>R : Type u_4<VAR>AddMonoidWithOne R<GOAL>1 = AddSubmonoid.closure {1}
<VAR>R : Type u_4<VAR>AddMonoidWithOne R<GOAL>1 = AddSubmonoid.closure 1
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N : AddSubmonoid R<VAR>m n : R<VAR>hm : m ∈ M<VAR>hn : n ∈ N<GOAL>m * n ∈ M * N
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N P : AddSubmonoid R<GOAL>M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N : AddSubmonoid R<VAR>C : R → Prop<VAR>r : R<VAR>hr : r ∈ M * N<VAR>hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)<VAR>ha : ∀ (x y : R), C x → C y → C (x + y)<GOAL>C r
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>S T : Set R<GOAL>AddSubmonoid.closure S * AddSubmonoid.closure T = AddSubmonoid.closure (S * T)
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N : AddSubmonoid R<GOAL>M * N = AddSubmonoid.closure (↑M * ↑N)
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>S : AddSubmonoid R<GOAL>S * ⊥ = ⊥
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>S : AddSubmonoid R<GOAL>⊥ * S = ⊥
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N P Q : AddSubmonoid R<VAR>hmp : M ≤ P<VAR>hnq : N ≤ Q<GOAL>M * N ≤ P * Q
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N P : AddSubmonoid R<VAR>h : M ≤ N<GOAL>M * P ≤ N * P
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N P : AddSubmonoid R<VAR>h : N ≤ P<GOAL>M * N ≤ M * P
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<VAR>M N : AddSubmonoid R<GOAL>↑M * ↑N ⊆ ↑(M * N)
<VAR>R : Type u_4<VAR>Semiring R<VAR>s : Set R<VAR>n : ℕ<GOAL>AddSubmonoid.closure s ^ n = AddSubmonoid.closure (s ^ n)
<VAR>R : Type u_4<VAR>Semiring R<VAR>s : AddSubmonoid R<VAR>n : ℕ<GOAL>s ^ n = AddSubmonoid.closure (↑s ^ n)
<VAR>R : Type u_4<VAR>Semiring R<VAR>s : AddSubmonoid R<VAR>n : ℕ<GOAL>↑s ^ n ⊆ ↑(s ^ n)
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s : Set α<VAR>hpos : ∀ x ∈ s, 1 ≤ x<VAR>h : s.IsPWO<GOAL>(↑(Submonoid.closure s)).IsPWO
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s : Set α<VAR>hpos : ∀ x ∈ s, 0 ≤ x<VAR>h : s.IsPWO<GOAL>(↑(AddSubmonoid.closure s)).IsPWO
<VAR>α : Type u_1<VAR>Monoid α<VAR>x : α<VAR>n : ℕ<GOAL>MulOpposite.op (x ^ n) = MulOpposite.op x ^ n
<VAR>α : Type u_1<VAR>Monoid α<VAR>x : αᵐᵒᵖ<VAR>n : ℕ<GOAL>MulOpposite.unop (x ^ n) = MulOpposite.unop x ^ n
<VAR>α : Type u_1<VAR>DivInvMonoid α<VAR>x : α<VAR>z : ℤ<GOAL>MulOpposite.op (x ^ z) = MulOpposite.op x ^ z
<VAR>α : Type u_1<VAR>DivInvMonoid α<VAR>x : αᵐᵒᵖ<VAR>z : ℤ<GOAL>MulOpposite.unop (x ^ z) = MulOpposite.unop x ^ z
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>AddOpposite.op ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>MulOpposite.op ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>AddOpposite.op (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>MulOpposite.op (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>IntCast α<VAR>n : ℤ<GOAL>AddOpposite.op ↑n = ↑n
<VAR>α : Type u_1<VAR>IntCast α<VAR>n : ℤ<GOAL>MulOpposite.op ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>MulOpposite.unop ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>AddOpposite.unop ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>MulOpposite.unop (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>AddOpposite.unop (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>IntCast α<VAR>n : ℤ<GOAL>MulOpposite.unop ↑n = ↑n
<VAR>α : Type u_1<VAR>IntCast α<VAR>n : ℤ<GOAL>AddOpposite.unop ↑n = ↑n
<VAR>α : Type u_1<VAR>SubNegMonoid α<VAR>x y : αᵃᵒᵖ<GOAL>AddOpposite.unop (x - y) = -AddOpposite.unop y + AddOpposite.unop x
<VAR>α : Type u_1<VAR>DivInvMonoid α<VAR>x y : αᵐᵒᵖ<GOAL>MulOpposite.unop (x / y) = (MulOpposite.unop y)⁻¹ * MulOpposite.unop x
<VAR>α : Type u_1<VAR>SubNegMonoid α<VAR>x y : α<GOAL>AddOpposite.op (x - y) = -AddOpposite.op y + AddOpposite.op x
<VAR>α : Type u_1<VAR>DivInvMonoid α<VAR>x y : α<GOAL>MulOpposite.op (x / y) = (MulOpposite.op y)⁻¹ * MulOpposite.op x
<VAR>α : Type u_1<VAR>Add α<VAR>a x y : α<GOAL>AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x) ↔ AddSemiconjBy a x y