ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>StrictMono AddSubgroup.toAddSubmonoid
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>Monotone AddSubgroup.toAddSubmonoid
<VAR>G : Type u_1<VAR>Group G<GOAL>Monotone Subgroup.toSubmonoid
<VAR>G : Type u_1<VAR>AddGroup G<VAR>p q : AddSubgroup G<GOAL>p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q
<VAR>G : Type u_1<VAR>Group G<VAR>p q : Subgroup G<GOAL>p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : AddSubgroup G<GOAL>(↑s).Nonempty
<VAR>G : Type u_1<VAR>Group G<VAR>s : Subgroup G<GOAL>(↑s).Nonempty
<VAR>G : Type u_1<VAR>Group G<VAR>S : Subgroup G<GOAL>↑(Subgroup.toAddSubgroup S) = ⇑Additive.toMul ⁻¹' ↑S
<VAR>G : Type u_1<VAR>Group G<VAR>S : AddSubgroup (Additive G)<GOAL>↑((RelIso.symm Subgroup.toAddSubgroup) S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
<VAR>A : Type u_4<VAR>AddGroup A<VAR>S : Subgroup (Multiplicative A)<GOAL>↑((RelIso.symm AddSubgroup.toSubgroup) S) = ⇑Additive.toMul ⁻¹' ↑S
<VAR>A : Type u_4<VAR>AddGroup A<VAR>S : AddSubgroup A<GOAL>↑(AddSubgroup.toSubgroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>s : Set G<VAR>hs : s = ↑K<GOAL>↑(K.copy s hs) = s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>s : Set G<VAR>hs : s = ↑K<GOAL>↑(K.copy s hs) = s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>s : Set G<VAR>hs : s = ↑K<GOAL>K.copy s hs = K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>s : Set G<VAR>hs : s = ↑K<GOAL>K.copy s hs = K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : ∀ (x : G), x ∈ H ↔ x ∈ K<GOAL>H = K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : ∀ (x : G), x ∈ H ↔ x ∈ K<GOAL>H = K
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>1 ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>0 ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x y : G<GOAL>x ∈ H → y ∈ H → x + y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x y : G<GOAL>x ∈ H → y ∈ H → x * y ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : G<GOAL>x ∈ H → -x ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x : G<GOAL>x ∈ H → x⁻¹ ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x y : G<VAR>hx : x ∈ H<VAR>hy : y ∈ H<GOAL>x - y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x y : G<VAR>hx : x ∈ H<VAR>hy : y ∈ H<GOAL>x / y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x : G<GOAL>x⁻¹ ∈ H ↔ x ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : G<GOAL>-x ∈ H ↔ x ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>a b : G<GOAL>a / b ∈ H ↔ b / a ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>a b : G<GOAL>a - b ∈ H ↔ b - a ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>P : G → Prop<GOAL>(∃ x ∈ K, P (-x)) ↔ ∃ x ∈ K, P x
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>P : G → Prop<GOAL>(∃ x ∈ K, P x⁻¹) ↔ ∃ x ∈ K, P x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x y : G<VAR>h : x ∈ H<GOAL>y + x ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x y : G<VAR>h : x ∈ H<GOAL>y * x ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x y : G<VAR>h : x ∈ H<GOAL>x + y ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x y : G<VAR>h : x ∈ H<GOAL>x * y ∈ H ↔ y ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>x : G<VAR>hx : x ∈ K<VAR>n : ℕ<GOAL>x ^ n ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>x : G<VAR>hx : x ∈ K<VAR>n : ℕ<GOAL>n • x ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>x : G<VAR>hx : x ∈ K<VAR>n : ℤ<GOAL>x ^ n ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>x : G<VAR>hx : x ∈ K<VAR>n : ℤ<GOAL>n • x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x y : ↥H<GOAL>↑(x + y) = ↑x + ↑y
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x y : ↥H<GOAL>↑(x * y) = ↑x * ↑y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>↑0 = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>↑1 = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : ↥H<GOAL>↑(-x) = -↑x
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x : ↥H<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x y : ↥H<GOAL>↑(x / y) = ↑x / ↑y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x y : ↥H<GOAL>↑(x - y) = ↑x - ↑y
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x : G<VAR>hx : x ∈ H<GOAL>↑⟨x, hx⟩ = x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : G<VAR>hx : x ∈ H<GOAL>↑⟨x, hx⟩ = x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : ↥H<VAR>n : ℕ<GOAL>↑(n • x) = n • ↑x
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x : ↥H<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x : ↥H<VAR>n : ℤ<GOAL>↑(n • x) = n • ↑x
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>x : ↥H<VAR>n : ℤ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>h : g ∈ H<GOAL>⟨g, h⟩ = 1 ↔ g = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<VAR>h : g ∈ H<GOAL>⟨g, h⟩ = 0 ↔ g = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⇑H.subtype = Subtype.val
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⇑H.subtype = Subtype.val
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Function.Injective ⇑H.subtype
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>Function.Injective ⇑H.subtype
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<VAR>a : ↥H<GOAL>↑((AddSubgroup.inclusion h) a) = ↑a
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<VAR>a : ↥H<GOAL>↑((Subgroup.inclusion h) a) = ↑a
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<GOAL>Function.Injective ⇑(AddSubgroup.inclusion h)
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<GOAL>Function.Injective ⇑(Subgroup.inclusion h)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>hH : H ≤ K<GOAL>K.subtype.comp (AddSubgroup.inclusion hH) = H.subtype
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : H ≤ K<GOAL>K.subtype.comp (Subgroup.inclusion hH) = H.subtype
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>↑(Subgroup.topEquiv.symm x) = x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : ↥⊤<GOAL>AddSubgroup.topEquiv x = ↑x
<VAR>G : Type u_1<VAR>Group G<VAR>x : ↥⊤<GOAL>Subgroup.topEquiv x = ↑x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<GOAL>↑(AddSubgroup.topEquiv.symm x) = x
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>x ∈ ⊥ ↔ x = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>x ∈ ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x : G<GOAL>x ∈ ⊤
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>↑⊤ = Set.univ
<VAR>G : Type u_1<VAR>Group G<GOAL>↑⊤ = Set.univ
<VAR>G : Type u_1<VAR>Group G<GOAL>↑⊥ = {1}
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>↑⊥ = {0}
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⊤.toAddSubmonoid = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>⊤.toSubmonoid = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>⊥.toSubmonoid = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⊥.toAddSubmonoid = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H = ⊥ ↔ ∀ x ∈ H, x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H = ⊥ ↔ ∀ x ∈ H, x = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Subsingleton ↥H<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Subsingleton ↥H<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>↑H = Set.univ ↔ H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>↑H = Set.univ ↔ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>(∃ g, ↑H = {g}) ↔ H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>(∃ g, ↑H = {g}) ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>Nontrivial ↥H<GOAL>∃ x ∈ H, x ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>Nontrivial ↥H<GOAL>∃ x ∈ H, x ≠ 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>Nontrivial ↥H ↔ H ≠ ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Nontrivial ↥H ↔ H ≠ ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H = ⊥ ∨ Nontrivial ↥H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H = ⊥ ∨ Nontrivial ↥H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H = ⊥ ∨ ∃ x ∈ H, x ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H = ⊥ ∨ ∃ x ∈ H, x ≠ 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H ≠ ⊥ ↔ ∃ a, a ≠ 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H ≠ ⊥ ↔ ∃ a, a ≠ 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>p p' : AddSubgroup G<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>G : Type u_1<VAR>Group G<VAR>p p' : Subgroup G<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>G : Type u_1<VAR>AddGroup G<VAR>p p' : AddSubgroup G<VAR>x : G<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>G : Type u_1<VAR>Group G<VAR>p p' : Subgroup G<VAR>x : G<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>G : Type u_1<VAR>Group G<VAR>H : Set (Subgroup G)<GOAL>↑(sInf H) = ⋂ s ∈ H, ↑s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : Set (AddSubgroup G)<GOAL>↑(sInf H) = ⋂ s ∈ H, ↑s
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set (Subgroup G)<VAR>x : G<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set (AddSubgroup G)<VAR>x : G<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>x : G<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>S : ι → AddSubgroup G<VAR>x : G<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>S : ι → AddSubgroup G<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Subgroup G<VAR>x : G<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : AddSubgroup G<VAR>x : G<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : AddSubgroup G<VAR>x : G<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Subgroup G<VAR>x : G<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S T : AddSubgroup G<VAR>x y : G<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x + y ∈ S ⊔ T
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Subgroup G<VAR>x y : G<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>S : ι → AddSubgroup G<VAR>i : ι<VAR>x : G<GOAL>x ∈ S i → x ∈ iSup S
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>i : ι<VAR>x : G<GOAL>x ∈ S i → x ∈ iSup S
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set (AddSubgroup G)<VAR>s : AddSubgroup G<VAR>hs : s ∈ S<VAR>x : G<GOAL>x ∈ s → x ∈ sSup S
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set (Subgroup G)<VAR>s : Subgroup G<VAR>hs : s ∈ S<VAR>x : G<GOAL>x ∈ s → x ∈ sSup S
<VAR>G : Type u_1<VAR>Group G<GOAL>Subsingleton (Subgroup G) ↔ Subsingleton G
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>Subsingleton (AddSubgroup G) ↔ Subsingleton G
<VAR>G : Type u_1<VAR>Group G<GOAL>Nontrivial (Subgroup G) ↔ Nontrivial G
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>Nontrivial (AddSubgroup G) ↔ Nontrivial G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H = ⊤ ↔ ∀ (x : G), x ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H = ⊤ ↔ ∀ (x : G), x ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<VAR>x : G<GOAL>x ∈ Subgroup.closure k ↔ ∀ (K : Subgroup G), k ⊆ ↑K → x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<VAR>x : G<GOAL>x ∈ AddSubgroup.closure k ↔ ∀ (K : AddSubgroup G), k ⊆ ↑K → x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<GOAL>k ⊆ ↑(AddSubgroup.closure k)
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<GOAL>k ⊆ ↑(Subgroup.closure k)
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<VAR>P : G<VAR>hP : P ∉ Subgroup.closure k<GOAL>P ∉ k
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<VAR>P : G<VAR>hP : P ∉ AddSubgroup.closure k<GOAL>P ∉ k
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>k : Set G<GOAL>Subgroup.closure k ≤ K ↔ k ⊆ ↑K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>k : Set G<GOAL>AddSubgroup.closure k ≤ K ↔ k ⊆ ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>k : Set G<VAR>h₁ : k ⊆ ↑K<VAR>h₂ : K ≤ Subgroup.closure k<GOAL>Subgroup.closure k = K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>k : Set G<VAR>h₁ : k ⊆ ↑K<VAR>h₂ : K ≤ AddSubgroup.closure k<GOAL>AddSubgroup.closure k = K
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<VAR>p : G → Prop<VAR>x : G<VAR>h : x ∈ Subgroup.closure k<VAR>mem : ∀ x ∈ k, p x<VAR>one : p 1<VAR>mul : ∀ (x y : G), p x → p y → p (x * y)<VAR>inv : ∀ (x : G), p x → p x⁻¹<GOAL>p x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<VAR>p : G → Prop<VAR>x : G<VAR>h : x ∈ AddSubgroup.closure k<VAR>mem : ∀ x ∈ k, p x<VAR>one : p 0<VAR>mul : ∀ (x y : G), p x → p y → p (x + y)<VAR>inv : ∀ (x : G), p x → p (-x)<GOAL>p x
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<VAR>p : (x : G) → x ∈ Subgroup.closure k → Prop<VAR>mem : ∀ (x : G) (h : x ∈ k), p x ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x : G) (hx : x ∈ Subgroup.closure k) (y : G) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯<VAR>inv : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯<VAR>x : G<VAR>hx : x ∈ Subgroup.closure k<GOAL>p x hx
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<VAR>p : (x : G) → x ∈ AddSubgroup.closure k → Prop<VAR>mem : ∀ (x : G) (h : x ∈ k), p x ⋯<VAR>one : p 0 ⋯<VAR>mul : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k) (y : G) (hy : y ∈ AddSubgroup.closure k), p x hx → p y hy → p (x + y) ⋯<VAR>inv : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x hx → p (-x) ⋯<VAR>x : G<VAR>hx : x ∈ AddSubgroup.closure k<GOAL>p x hx
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<VAR>p : G → G → Prop<VAR>x y : G<VAR>hx : x ∈ Subgroup.closure k<VAR>hy : y ∈ Subgroup.closure k<VAR>Hk : ∀ x ∈ k, ∀ y ∈ k, p x y<VAR>H1_left : ∀ (x : G), p 1 x<VAR>H1_right : ∀ (x : G), p x 1<VAR>Hmul_left : ∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>Hinv_left : ∀ (x y : G), p x y → p x⁻¹ y<VAR>Hinv_right : ∀ (x y : G), p x y → p x y⁻¹<GOAL>p x y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<VAR>p : G → G → Prop<VAR>x y : G<VAR>hx : x ∈ AddSubgroup.closure k<VAR>hy : y ∈ AddSubgroup.closure k<VAR>Hk : ∀ x ∈ k, ∀ y ∈ k, p x y<VAR>H1_left : ∀ (x : G), p 0 x<VAR>H1_right : ∀ (x : G), p x 0<VAR>Hmul_left : ∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hinv_left : ∀ (x y : G), p x y → p (-x) y<VAR>Hinv_right : ∀ (x y : G), p x y → p x (-y)<GOAL>p x y
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<GOAL>Subgroup.closure (Subtype.val ⁻¹' k) = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<GOAL>AddSubgroup.closure (Subtype.val ⁻¹' k) = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>h k : Set G<VAR>h' : h ⊆ k<GOAL>Subgroup.closure h ≤ Subgroup.closure k
<VAR>G : Type u_1<VAR>AddGroup G<VAR>h k : Set G<VAR>h' : h ⊆ k<GOAL>AddSubgroup.closure h ≤ AddSubgroup.closure k
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<GOAL>Subgroup.closure ↑K = K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<GOAL>AddSubgroup.closure ↑K = K
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>AddSubgroup.closure ∅ = ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>Subgroup.closure ∅ = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>AddSubgroup.closure Set.univ = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>Subgroup.closure Set.univ = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<GOAL>Subgroup.closure (s ∪ t) = Subgroup.closure s ⊔ Subgroup.closure t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s t : Set G<GOAL>AddSubgroup.closure (s ∪ t) = AddSubgroup.closure s ⊔ AddSubgroup.closure t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H H' : AddSubgroup G<GOAL>H ⊔ H' = AddSubgroup.closure (↑H ∪ ↑H')
<VAR>G : Type u_1<VAR>Group G<VAR>H H' : Subgroup G<GOAL>H ⊔ H' = Subgroup.closure (↑H ∪ ↑H')
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>s : ι → Set G<GOAL>Subgroup.closure (⋃ i, s i) = ⨆ i, Subgroup.closure (s i)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>s : ι → Set G<GOAL>AddSubgroup.closure (⋃ i, s i) = ⨆ i, AddSubgroup.closure (s i)
<VAR>G : Type u_1<VAR>Group G<VAR>k : Set G<GOAL>Subgroup.closure k = ⊥ ↔ k ⊆ {1}
<VAR>G : Type u_1<VAR>AddGroup G<VAR>k : Set G<GOAL>AddSubgroup.closure k = ⊥ ↔ k ⊆ {0}
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>p : ι → AddSubgroup G<GOAL>⨆ i, p i = AddSubgroup.closure (⋃ i, ↑(p i))
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>p : ι → Subgroup G<GOAL>⨆ i, p i = Subgroup.closure (⋃ i, ↑(p i))
<VAR>G : Type u_1<VAR>Group G<VAR>x y : G<GOAL>y ∈ Subgroup.closure {x} ↔ ∃ n, x ^ n = y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>x y : G<GOAL>y ∈ AddSubgroup.closure {x} ↔ ∃ n, n • x = y
<VAR>G : Type u_1<VAR>Group G<GOAL>Subgroup.closure {1} = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>AddSubgroup.closure {0} = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<GOAL>AddSubmonoid.closure S ≤ (AddSubgroup.closure S).toAddSubmonoid
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<GOAL>Submonoid.closure S ≤ (Subgroup.closure S).toSubmonoid
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>h : Submonoid.closure S = ⊤<GOAL>Subgroup.closure S = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<VAR>h : AddSubmonoid.closure S = ⊤<GOAL>AddSubgroup.closure S = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → AddSubgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ iSup K ↔ ∃ i, x ∈ K i
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ iSup K ↔ ∃ i, x ∈ K i
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_5<VAR>Nonempty ι<VAR>S : ι → AddSubgroup G<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_5<VAR>Nonempty ι<VAR>S : ι → Subgroup G<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : Set (AddSubgroup G)<VAR>Kne : K.Nonempty<VAR>hK : DirectedOn (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>K : Set (Subgroup G)<VAR>Kne : K.Nonempty<VAR>hK : DirectedOn (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>K : Subgroup N<VAR>f : G →* N<GOAL>↑(Subgroup.comap f K) = ⇑f ⁻¹' ↑K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>K : AddSubgroup N<VAR>f : G →+ N<GOAL>↑(AddSubgroup.comap f K) = ⇑f ⁻¹' ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>G₂ : Type u_7<VAR>Group G₂<VAR>f : G →* G₂<VAR>s : Subgroup G₂<GOAL>AddSubgroup.comap (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.comap f s)
<VAR>A : Type u_7<VAR>A₂ : Type u_8<VAR>AddGroup A<VAR>AddGroup A₂<VAR>f : A →+ A₂<VAR>s : AddSubgroup A₂<GOAL>Subgroup.comap (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.comap f s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>K : Subgroup N<VAR>f : G →* N<VAR>x : G<GOAL>x ∈ Subgroup.comap f K ↔ f x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>K : AddSubgroup N<VAR>f : G →+ N<VAR>x : G<GOAL>x ∈ AddSubgroup.comap f K ↔ f x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K K' : AddSubgroup N<GOAL>K ≤ K' → AddSubgroup.comap f K ≤ AddSubgroup.comap f K'
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K K' : Subgroup N<GOAL>K ≤ K' → Subgroup.comap f K ≤ Subgroup.comap f K'
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>P : Type u_6<VAR>Group P<VAR>K : Subgroup P<VAR>g : N →* P<VAR>f : G →* N<GOAL>Subgroup.comap f (Subgroup.comap g K) = Subgroup.comap (g.comp f) K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>P : Type u_6<VAR>AddGroup P<VAR>K : AddSubgroup P<VAR>g : N →+ P<VAR>f : G →+ N<GOAL>AddSubgroup.comap f (AddSubgroup.comap g K) = AddSubgroup.comap (g.comp f) K
<VAR>N : Type u_5<VAR>Group N<VAR>K : Subgroup N<GOAL>Subgroup.comap (MonoidHom.id N) K = K
<VAR>N : Type u_5<VAR>AddGroup N<VAR>K : AddSubgroup N<GOAL>AddSubgroup.comap (AddMonoidHom.id N) K = K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K : Subgroup G<GOAL>↑(Subgroup.map f K) = ⇑f '' ↑K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K : AddSubgroup G<GOAL>↑(AddSubgroup.map f K) = ⇑f '' ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K : Subgroup G<VAR>y : N<GOAL>y ∈ Subgroup.map f K ↔ ∃ x ∈ K, f x = y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K : AddSubgroup G<VAR>y : N<GOAL>y ∈ AddSubgroup.map f K ↔ ∃ x ∈ K, f x = y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K : AddSubgroup G<VAR>x : G<VAR>hx : x ∈ K<GOAL>f x ∈ AddSubgroup.map f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K : Subgroup G<VAR>x : G<VAR>hx : x ∈ K<GOAL>f x ∈ Subgroup.map f K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K : AddSubgroup G<VAR>x : ↥K<GOAL>f ↑x ∈ AddSubgroup.map f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K : Subgroup G<VAR>x : ↥K<GOAL>f ↑x ∈ Subgroup.map f K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K K' : AddSubgroup G<GOAL>K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K'
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K K' : Subgroup G<GOAL>K ≤ K' → Subgroup.map f K ≤ Subgroup.map f K'
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<GOAL>AddSubgroup.map (AddMonoidHom.id G) K = K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<GOAL>Subgroup.map (MonoidHom.id G) K = K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>N : Type u_5<VAR>Group N<VAR>P : Type u_6<VAR>Group P<VAR>g : N →* P<VAR>f : G →* N<GOAL>Subgroup.map g (Subgroup.map f K) = Subgroup.map (g.comp f) K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>P : Type u_6<VAR>AddGroup P<VAR>g : N →+ P<VAR>f : G →+ N<GOAL>AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (g.comp f) K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>N : Type u_5<VAR>Group N<GOAL>Subgroup.map 1 K = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>N : Type u_5<VAR>AddGroup N<GOAL>AddSubgroup.map 0 K = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G ≃* N<VAR>K : Subgroup G<VAR>x : N<GOAL>x ∈ Subgroup.map f.toMonoidHom K ↔ f.symm x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G ≃+ N<VAR>K : AddSubgroup G<VAR>x : N<GOAL>x ∈ AddSubgroup.map f.toAddMonoidHom K ↔ f.symm x ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>hf : Function.Injective ⇑f<VAR>K : AddSubgroup G<VAR>x : G<GOAL>f x ∈ AddSubgroup.map f K ↔ x ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>hf : Function.Injective ⇑f<VAR>K : Subgroup G<VAR>x : G<GOAL>f x ∈ Subgroup.map f K ↔ x ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G ≃* N<VAR>K : Subgroup G<GOAL>Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G ≃+ N<VAR>K : AddSubgroup G<GOAL>AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G ≃+ N<VAR>K : AddSubgroup G<GOAL>AddSubgroup.map (↑f) K = AddSubgroup.comap (↑f.symm) K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G ≃* N<VAR>K : Subgroup G<GOAL>Subgroup.map (↑f) K = Subgroup.comap (↑f.symm) K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : N ≃* G<VAR>K : Subgroup G<GOAL>Subgroup.comap (↑f) K = Subgroup.map (↑f.symm) K