ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>h₁ : IsAddUnit x<VAR>h₂ : x ∈ S.ofAddUnits<GOAL>h₁.addUnit ∈ S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>h₁ : IsUnit x<VAR>h₂ : x ∈ S.ofUnits<GOAL>h₁.unit ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<VAR>h₁ : IsAddUnit x<VAR>h₂ : h₁.addUnit ∈ S<GOAL>x ∈ S.ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<VAR>h₁ : IsUnit x<VAR>h₂ : h₁.unit ∈ S<GOAL>x ∈ S.ofUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Subgroup Mˣ<VAR>x : M<GOAL>x ∈ S.ofUnits ↔ ∃ (h : IsUnit x), h.unit ∈ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubgroup (AddUnits M)<VAR>x : M<GOAL>x ∈ S.ofAddUnits ↔ ∃ (h : IsAddUnit x), h.addUnit ∈ S
<VAR>M : Type u_1<VAR>Monoid M<GOAL>⊥.ofUnits = ⊥
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>⊥.ofAddUnits = ⊥
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S T : AddSubgroup (AddUnits M)<GOAL>(S ⊔ T).ofAddUnits = S.ofAddUnits ⊔ T.ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S T : Subgroup Mˣ<GOAL>(S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set (Subgroup Mˣ)<GOAL>(sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set (AddSubgroup (AddUnits M))<GOAL>(sSup s).ofAddUnits = ⨆ S ∈ s, S.ofAddUnits
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Sort u_2<VAR>f : ι → AddSubgroup (AddUnits M)<GOAL>(iSup f).ofAddUnits = ⨆ i, (f i).ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Sort u_2<VAR>f : ι → Subgroup Mˣ<GOAL>(iSup f).ofUnits = ⨆ i, (f i).ofUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>f : (i : ι) → κ i → Subgroup Mˣ<GOAL>(⨆ i, ⨆ j, f i j).ofUnits = ⨆ i, ⨆ j, (f i j).ofUnits
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>f : (i : ι) → κ i → AddSubgroup (AddUnits M)<GOAL>(⨆ i, ⨆ j, f i j).ofAddUnits = ⨆ i, ⨆ j, (f i j).ofAddUnits
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Function.Injective AddSubgroup.ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Function.Injective Subgroup.ofUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S T : Subgroup Mˣ<GOAL>(S.ofUnits ⊔ T.ofUnits).units = S ⊔ T
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S T : AddSubgroup (AddUnits M)<GOAL>(S.ofAddUnits ⊔ T.ofAddUnits).addUnits = S ⊔ T
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S T : AddSubgroup (AddUnits M)<GOAL>(S.ofAddUnits ⊓ T.ofAddUnits).addUnits = S ⊓ T
<VAR>M : Type u_1<VAR>Monoid M<VAR>S T : Subgroup Mˣ<GOAL>(S.ofUnits ⊓ T.ofUnits).units = S ⊓ T
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Function.RightInverse Subgroup.ofUnits Submonoid.units
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Function.RightInverse AddSubgroup.ofAddUnits AddSubmonoid.addUnits
<VAR>M : Type u_1<VAR>Monoid M<GOAL>StrictMono Subgroup.ofUnits
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>StrictMono AddSubgroup.ofAddUnits
<VAR>M : Type u_1<VAR>Monoid M<VAR>S T : Subgroup Mˣ<GOAL>S.ofUnits ≤ T.ofUnits ↔ S ≤ T
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>x : Gˣ<GOAL>x ∈ H.units ↔ ↑x ∈ H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : AddUnits G<GOAL>x ∈ H.addUnits ↔ ↑x ∈ H
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup Gˣ<VAR>x : G<GOAL>x ∈ H.ofUnits ↔ toUnits x ∈ H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup (AddUnits G)<VAR>x : G<GOAL>x ∈ H.ofAddUnits ↔ toAddUnits x ∈ H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : G<GOAL>toAddUnits x ∈ H.addUnits ↔ x ∈ H
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>x : G<GOAL>toUnits x ∈ H.units ↔ x ∈ H
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup Gˣ<VAR>x : Gˣ<GOAL>↑x ∈ H.ofUnits ↔ x ∈ H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup (AddUnits G)<VAR>x : AddUnits G<GOAL>↑x ∈ H.ofAddUnits ↔ x ∈ H
<VAR>a : Multiplicative ℤ<VAR>b : ℕ<GOAL>Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * ↑b
<VAR>a : Multiplicative ℤ<VAR>b : ℤ<GOAL>Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
<VAR>a b : ℤ<GOAL>Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b
<VAR>u : ℤˣ<GOAL>(↑u).natAbs = 1
<VAR>u : ℤ<VAR>hu : IsUnit u<GOAL>u.natAbs = 1
<VAR>u : ℤ<VAR>hu : IsUnit u<GOAL>u = 1 ∨ u = -1
<VAR>u v : ℤ<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>u ≠ v ↔ u = -v
<VAR>u v : ℤ<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>u = v ∨ u = -v
<VAR>u : ℤ<GOAL>IsUnit u ↔ u = 1 ∨ u = -1
<VAR>u v : ℤ<VAR>h : u * v = 1<GOAL>u = 1 ∨ u = -1
<VAR>u v : ℤ<VAR>h : u * v = 1<GOAL>u = v
<VAR>u : ℤ<GOAL>IsUnit u ↔ u.natAbs = 1
<VAR>n : ℕ<GOAL>IsUnit ↑n ↔ IsUnit n
<VAR>u : ℤ<VAR>hu : IsUnit u<GOAL>u * u = 1
<VAR>a b c d : ℤ<VAR>ha : IsUnit a<VAR>hb : IsUnit b<VAR>hc : IsUnit c<VAR>hd : IsUnit d<GOAL>a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
<VAR>u v : ℤ<VAR>h : u * v = -1<GOAL>u = 1 ∨ u = -1
<VAR>n : ℤ<GOAL>¬n % 2 = 1 ↔ n % 2 = 0
<VAR>n : ℤ<GOAL>¬n % 2 = 0 ↔ n % 2 = 1
<VAR>n : ℤ<GOAL>Even n ↔ n % 2 = 0
<VAR>n : ℤ<GOAL>¬Even n ↔ n % 2 = 1
<VAR>n : ℤ<GOAL>¬2 ∣ n ↔ n % 2 = 1
<VAR>m n : ℤ<GOAL>Even (m + n) ↔ (Even m ↔ Even n)
<VAR>n : ℤ<GOAL>¬2 ∣ 2 * n + 1
<VAR>m n : ℤ<GOAL>Even (m - n) ↔ (Even m ↔ Even n)
<VAR>n : ℤ<GOAL>Even (n + 1) ↔ ¬Even n
<VAR>n : ℤ<GOAL>Even (n - 1) ↔ ¬Even n
<VAR>m n : ℤ<GOAL>Even (m * n) ↔ Even m ∨ Even n
<VAR>m : ℤ<VAR>n : ℕ<GOAL>Even (m ^ n) ↔ Even m ∧ n ≠ 0
<VAR>m : ℤ<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Even (m ^ n) ↔ Even m
<VAR>n : ℕ<GOAL>Even ↑n ↔ Even n
<VAR>n : ℤ<GOAL>Even n → 2 * (n / 2) = n
<VAR>n : ℤ<GOAL>Even n → n / 2 * 2 = n
<VAR>a b : ℤ<GOAL>a • b = a * b
<VAR>n : ℤ<GOAL>n • 1 = n
<VAR>K : Type u_1<VAR>n : ℕ<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>DivisionRing K<VAR>terminatedAt_succ_n : s.TerminatedAt (n + 1)<GOAL>GenContFract.squashSeq s n = s
<VAR>K : Type u_1<VAR>n : ℕ<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>DivisionRing K<VAR>gp_n gp_succ_n : GenContFract.Pair K<VAR>s_nth_eq : s.get? n = some gp_n<VAR>s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n<GOAL>(GenContFract.squashSeq s n).get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }
<VAR>K : Type u_1<VAR>n : ℕ<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>DivisionRing K<VAR>m : ℕ<VAR>m_lt_n : m < n<GOAL>(GenContFract.squashSeq s n).get? m = s.get? m
<VAR>K : Type u_1<VAR>n : ℕ<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>DivisionRing K<GOAL>(GenContFract.squashSeq s (n + 1)).tail = GenContFract.squashSeq s.tail n
<VAR>K : Type u_1<VAR>n : ℕ<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>DivisionRing K<GOAL>GenContFract.convs'Aux s (n + 2) = GenContFract.convs'Aux (GenContFract.squashSeq s n) (n + 1)
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.squashGCF n = g
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>m : ℕ<VAR>m_lt_n : m < n<GOAL>(g.squashGCF (n + 1)).s.get? m = g.s.get? m
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.convs' (n + 1) = (g.squashGCF n).convs' n
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>m : ℕ<GOAL>m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>Field K<VAR>nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0<GOAL>g.convs (n + 1) = (g.squashGCF n).convs n
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>LinearOrderedField K<VAR>s_pos : ∀ {gp : GenContFract.Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b<GOAL>g.convs n = g.convs' n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>c : ContFract K<GOAL>(↑↑c).convs = (↑↑c).convs'
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>IsConj a a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>IsConj a b → IsConj b a
<VAR>α : Type u<VAR>Monoid α<VAR>g h : α<GOAL>IsConj g h ↔ IsConj h g
<VAR>α : Type u<VAR>Monoid α<VAR>a b c : α<GOAL>IsConj a b → IsConj b c → IsConj a c
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>IsConj a b ↔ a = b
<VAR>α : Type u<VAR>β : Type v<VAR>Monoid α<VAR>Monoid β<VAR>f : α →* β<VAR>a b : α<GOAL>IsConj a b → IsConj (f a) (f b)
<VAR>α : Type u<VAR>CancelMonoid α<VAR>a : α<GOAL>IsConj 1 a ↔ a = 1
<VAR>α : Type u<VAR>CancelMonoid α<VAR>a : α<GOAL>IsConj a 1 ↔ a = 1
<VAR>α : Type u<VAR>Group α<VAR>a b : α<GOAL>IsConj a b ↔ ∃ c, c * a * c⁻¹ = b
<VAR>α : Type u<VAR>Group α<VAR>a b : α<GOAL>(b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
<VAR>α : Type u<VAR>Group α<VAR>a b c : α<GOAL>b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹
<VAR>α : Type u<VAR>Group α<VAR>i : ℕ<VAR>a b : α<GOAL>(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>i : ℤ<VAR>a b : α<GOAL>(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>x : α<GOAL>Function.Injective fun g => x * g * x⁻¹
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>⟦a⟧ = ConjClasses.mk a
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>Quot.mk Setoid.r a = ConjClasses.mk a
<VAR>α : Type u<VAR>Monoid α<VAR>p : ConjClasses α → Prop<GOAL>(∀ (a : ConjClasses α), p a) ↔ ∀ (a : α), p (ConjClasses.mk a)
<VAR>α : Type u<VAR>Monoid α<GOAL>Function.Surjective ConjClasses.mk
<VAR>α : Type u<VAR>Monoid α<GOAL>1 = ConjClasses.mk 1
<VAR>α : Type u<VAR>Monoid α<VAR>a : ConjClasses α<GOAL>∃ a0, ConjClasses.mk a0 = a
<VAR>α : Type u<VAR>β : Type v<VAR>Monoid α<VAR>Monoid β<VAR>f : α →* β<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (ConjClasses.map f)
<VAR>α : Type u<VAR>CommMonoid α<GOAL>Function.Injective ConjClasses.mk
<VAR>α : Type u<VAR>CommMonoid α<GOAL>Function.Bijective ConjClasses.mk
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>a ∈ conjugatesOf a
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<VAR>ab : IsConj a b<GOAL>conjugatesOf a = conjugatesOf b
<VAR>α : Type u<VAR>Monoid α<VAR>a b : α<GOAL>IsConj a b ↔ conjugatesOf a = conjugatesOf b
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<GOAL>a ∈ (ConjClasses.mk a).carrier
<VAR>α : Type u<VAR>Monoid α<VAR>a : α<VAR>b : ConjClasses α<GOAL>a ∈ b.carrier ↔ ConjClasses.mk a = b
<VAR>α : Type u<VAR>Monoid α<VAR>a : ConjClasses α<GOAL>a.carrier = ConjClasses.mk ⁻¹' {a}
<VAR>S : Type u_4<VAR>M : Type u_5<VAR>One M<VAR>SetLike S M<VAR>self : OneMemClass S M<VAR>s : S<GOAL>1 ∈ s
<VAR>S : Type u_4<VAR>M : Type u_5<VAR>Zero M<VAR>SetLike S M<VAR>self : ZeroMemClass S M<VAR>s : S<GOAL>0 ∈ s
<VAR>M : Type u_4<VAR>MulOneClass M<VAR>self : Submonoid M<GOAL>1 ∈ self.carrier
<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>self : AddSubmonoid M<GOAL>0 ∈ self.carrier
<VAR>M : Type u_4<VAR>A : Type u_5<VAR>AddMonoid M<VAR>SetLike A M<VAR>AddSubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>n • x ∈ S
<VAR>M : Type u_4<VAR>A : Type u_5<VAR>Monoid M<VAR>SetLike A M<VAR>SubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>x ^ n ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Submonoid M<VAR>x : M<GOAL>x ∈ s.toSubsemigroup ↔ x ∈ s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : AddSubmonoid M<VAR>x : M<GOAL>x ∈ s.toAddSubsemigroup ↔ x ∈ s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Submonoid M<VAR>x : M<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : AddSubmonoid M<VAR>x : M<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : AddSubsemigroup M<VAR>x : M<VAR>h_one : 0 ∈ s.carrier<GOAL>x ∈ { toAddSubsemigroup := s, zero_mem' := h_one } ↔ x ∈ s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Subsemigroup M<VAR>x : M<VAR>h_one : 1 ∈ s.carrier<GOAL>x ∈ { toSubsemigroup := s, one_mem' := h_one } ↔ x ∈ s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Subsemigroup M<VAR>h_one : 1 ∈ s.carrier<GOAL>↑{ toSubsemigroup := s, one_mem' := h_one } = ↑s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : AddSubsemigroup M<VAR>h_one : 0 ∈ s.carrier<GOAL>↑{ toAddSubsemigroup := s, zero_mem' := h_one } = ↑s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s t : Subsemigroup M<VAR>h_one : 1 ∈ s.carrier<VAR>h_one' : 1 ∈ t.carrier<GOAL>{ toSubsemigroup := s, one_mem' := h_one } ≤ { toSubsemigroup := t, one_mem' := h_one' } ↔ s ≤ t
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s t : AddSubsemigroup M<VAR>h_one : 0 ∈ s.carrier<VAR>h_one' : 0 ∈ t.carrier<GOAL>{ toAddSubsemigroup := s, zero_mem' := h_one } ≤ { toAddSubsemigroup := t, zero_mem' := h_one' } ↔ s ≤ t
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S T : Submonoid M<VAR>h : ∀ (x : M), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S T : AddSubmonoid M<VAR>h : ∀ (x : M), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>0 ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>1 ∈ S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>x y : M<GOAL>x ∈ S → y ∈ S → x + y ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>x y : M<GOAL>x ∈ S → y ∈ S → x * y ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>x : M<GOAL>x ∈ ⊥ ↔ x = 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>x : M<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>↑⊤ = Set.univ
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>↑⊤ = Set.univ
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>↑⊥ = {1}
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>↑⊥ = {0}
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>p p' : Submonoid M<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>p p' : AddSubmonoid M<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>p p' : AddSubmonoid M<VAR>x : M<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>p p' : Submonoid M<VAR>x : M<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : Set (AddSubmonoid M)<VAR>x : M<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set (Submonoid M)<VAR>x : M<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>S : ι → AddSubmonoid M<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>S : ι → Submonoid M<VAR>x : M<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>S : ι → AddSubmonoid M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>Subsingleton (Submonoid M) ↔ Subsingleton M
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>Subsingleton (AddSubmonoid M) ↔ Subsingleton M
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>Nontrivial (Submonoid M) ↔ Nontrivial M
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>Nontrivial (AddSubmonoid M) ↔ Nontrivial M
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ AddSubmonoid.closure s ↔ ∀ (S : AddSubmonoid M), s ⊆ ↑S → x ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ Submonoid.closure s ↔ ∀ (S : Submonoid M), s ⊆ ↑S → x ∈ S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<GOAL>s ⊆ ↑(Submonoid.closure s)
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<GOAL>s ⊆ ↑(AddSubmonoid.closure s)
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>P : M<VAR>hP : P ∉ AddSubmonoid.closure s<GOAL>P ∉ s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>P : M<VAR>hP : P ∉ Submonoid.closure s<GOAL>P ∉ s
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>S : Submonoid M<GOAL>Submonoid.closure s ≤ S ↔ s ⊆ ↑S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>S : AddSubmonoid M<GOAL>AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>AddSubmonoid.closure s ≤ AddSubmonoid.closure t
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>Submonoid.closure s ≤ Submonoid.closure t
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>S : Submonoid M<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ Submonoid.closure s<GOAL>Submonoid.closure s = S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>S : AddSubmonoid M<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ AddSubmonoid.closure s<GOAL>AddSubmonoid.closure s = S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>p : M → Prop<VAR>x : M<VAR>h : x ∈ AddSubmonoid.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 0<VAR>mul : ∀ (x y : M), p x → p y → p (x + y)<GOAL>p x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>p : M → Prop<VAR>x : M<VAR>h : x ∈ Submonoid.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>p : (x : M) → x ∈ AddSubmonoid.closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>one : p 0 ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ AddSubmonoid.closure s) (y : M) (hy : y ∈ AddSubmonoid.closure s), p x hx → p y hy → p (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ AddSubmonoid.closure s<GOAL>p x hx
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>p : (x : M) → x ∈ Submonoid.closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ Submonoid.closure s) (y : M) (hy : y ∈ Submonoid.closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ Submonoid.closure s<GOAL>p x hx
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<VAR>p : M → M → Prop<VAR>x y : M<VAR>hx : x ∈ Submonoid.closure s<VAR>hy : y ∈ Submonoid.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>H1_left : ∀ (x : M), p 1 x<VAR>H1_right : ∀ (x : M), p x 1<VAR>Hmul_left : ∀ (x y z : M), p x z → p y z → p (x * y) z<VAR>Hmul_right : ∀ (x y z : M), p z x → p z y → p z (x * y)<GOAL>p x y
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<VAR>p : M → M → Prop<VAR>x y : M<VAR>hx : x ∈ AddSubmonoid.closure s<VAR>hy : y ∈ AddSubmonoid.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>H1_left : ∀ (x : M), p 0 x<VAR>H1_right : ∀ (x : M), p x 0<VAR>Hmul_left : ∀ (x y z : M), p x z → p y z → p (x + y) z<VAR>Hmul_right : ∀ (x y z : M), p z x → p z y → p z (x + y)<GOAL>p x y
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : AddSubmonoid.closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 0<VAR>mul : ∀ (x y : M), p x → p y → p (x + y)<GOAL>p x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : Submonoid.closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<GOAL>↑(Submonoid.closure s) = {1} ∪ ↑(Subsemigroup.closure s)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>Submonoid.closure ↑S = S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>AddSubmonoid.closure ↑S = S
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>Submonoid.closure ∅ = ⊥
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>AddSubmonoid.closure ∅ = ⊥
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>Submonoid.closure Set.univ = ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>AddSubmonoid.closure Set.univ = ⊤
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s t : Set M<GOAL>Submonoid.closure (s ∪ t) = Submonoid.closure s ⊔ Submonoid.closure t
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s t : Set M<GOAL>AddSubmonoid.closure (s ∪ t) = AddSubmonoid.closure s ⊔ AddSubmonoid.closure t
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>N N' : Submonoid M<GOAL>N ⊔ N' = Submonoid.closure (↑N ∪ ↑N')
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>N N' : AddSubmonoid M<GOAL>N ⊔ N' = AddSubmonoid.closure (↑N ∪ ↑N')
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>s : ι → Set M<GOAL>AddSubmonoid.closure (⋃ i, s i) = ⨆ i, AddSubmonoid.closure (s i)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>s : ι → Set M<GOAL>Submonoid.closure (⋃ i, s i) = ⨆ i, Submonoid.closure (s i)
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>m : M<VAR>p : AddSubmonoid M<GOAL>AddSubmonoid.closure {m} ≤ p ↔ m ∈ p
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>m : M<VAR>p : Submonoid M<GOAL>Submonoid.closure {m} ≤ p ↔ m ∈ p
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>p : ι → AddSubmonoid M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : AddSubmonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>p : ι → Submonoid M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>ι : Sort u_4<VAR>p : ι → Submonoid M<GOAL>⨆ i, p i = Submonoid.closure (⋃ i, ↑(p i))
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>ι : Sort u_4<VAR>p : ι → AddSubmonoid M<GOAL>⨆ i, p i = AddSubmonoid.closure (⋃ i, ↑(p i))
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>p₁ p₂ : AddSubmonoid M<GOAL>Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 0
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>p₁ p₂ : Submonoid M<GOAL>Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>p₁ p₂ : Submonoid M<GOAL>Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>p₁ p₂ : AddSubmonoid M<GOAL>Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>f.eqLocusM f = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>f.eqLocusM f = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f g : M →+ N<VAR>s : Set M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(AddSubmonoid.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f g : M →* N<VAR>s : Set M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Submonoid.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f g : M →+ N<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f g : M →* N<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : Set M<VAR>hs : AddSubmonoid.closure s = ⊤<VAR>f g : M →+ N<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Set M<VAR>hs : Submonoid.closure s = ⊤<VAR>f g : M →* N<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>a : M<GOAL>a ∈ IsAddUnit.addSubmonoid M ↔ IsAddUnit a
<VAR>M : Type u_4<VAR>Monoid M<VAR>a : M<GOAL>a ∈ IsUnit.submonoid M ↔ IsUnit a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>s : Set M<VAR>f : M → N<VAR>hs : Submonoid.closure s = ⊤<VAR>h1 : f 1 = 1<VAR>hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y<GOAL>⇑(MonoidHom.ofClosureMEqTopLeft f hs h1 hmul) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>s : Set M<VAR>f : M → N<VAR>hs : AddSubmonoid.closure s = ⊤<VAR>h1 : f 0 = 0<VAR>hmul : ∀ x ∈ s, ∀ (y : M), f (x + y) = f x + f y<GOAL>⇑(AddMonoidHom.ofClosureMEqTopLeft f hs h1 hmul) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>s : Set M<VAR>f : M → N<VAR>hs : Submonoid.closure s = ⊤<VAR>h1 : f 1 = 1<VAR>hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y<GOAL>⇑(MonoidHom.ofClosureMEqTopRight f hs h1 hmul) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddMonoid M<VAR>AddMonoid N<VAR>s : Set M<VAR>f : M → N<VAR>hs : AddSubmonoid.closure s = ⊤<VAR>h1 : f 0 = 0<VAR>hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y<GOAL>⇑(AddMonoidHom.ofClosureMEqTopRight f hs h1 hmul) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>p : Prop<VAR>Decidable p<VAR>a : α<VAR>b : p → β<VAR>c : ¬p → β<GOAL>(a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul β α<VAR>p : Prop<VAR>Decidable p<VAR>a : α<VAR>b : p → β<VAR>c : ¬p → β<GOAL>(if h : p then b h else c h) • a = if h : p then b h • a else c h • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>p : Prop<VAR>Decidable p<VAR>a : p → α<VAR>b : ¬p → α<VAR>c : β<GOAL>(if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c