ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a - b = a - c ↔ b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>b - a = c - a ↔ b = c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>b / a = c / a ↔ b = c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a - b + (b - c) = a - c
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a / b * (b / c) = a / c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a - c - (b - c) = a - b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a / c / (b / c) = a / b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a - b = 0 ↔ a = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a / b = 1 ↔ a = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a / b ≠ 1 ↔ a ≠ b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a - b ≠ 0 ↔ a ≠ b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b : G<GOAL>a - b = a ↔ b = 0
<VAR>G : Type u_3<VAR>Group G<VAR>a b : G<GOAL>a / b = a ↔ b = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a = b - c ↔ a + c = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a = b / c ↔ a * c = b
<VAR>G : Type u_3<VAR>Group G<VAR>a b c : G<GOAL>a / b = c ↔ a = c * b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c : G<GOAL>a - b = c ↔ a = c + b
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a b c d : G<VAR>H : a - b = c - d<GOAL>a = b ↔ c = d
<VAR>G : Type u_3<VAR>Group G<VAR>a b c d : G<VAR>H : a / b = c / d<GOAL>a = b ↔ c = d
<VAR>G : Type u_3<VAR>AddGroup G<VAR>c : G<GOAL>Function.LeftInverse (fun x => x - c) fun x => x + c
<VAR>G : Type u_3<VAR>Group G<VAR>c : G<GOAL>Function.LeftInverse (fun x => x / c) fun x => x * c
<VAR>G : Type u_3<VAR>Group G<VAR>c : G<GOAL>Function.LeftInverse (fun x => x * c) fun x => x / c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>c : G<GOAL>Function.LeftInverse (fun x => x + c) fun x => x - c
<VAR>G : Type u_3<VAR>AddGroup G<VAR>c : G<GOAL>Function.LeftInverse (fun x => c + x) fun x => -c + x
<VAR>G : Type u_3<VAR>Group G<VAR>c : G<GOAL>Function.LeftInverse (fun x => c * x) fun x => c⁻¹ * x
<VAR>G : Type u_3<VAR>Group G<VAR>c : G<GOAL>Function.LeftInverse (fun x => c⁻¹ * x) fun x => c * x
<VAR>G : Type u_3<VAR>AddGroup G<VAR>c : G<GOAL>Function.LeftInverse (fun x => -c + x) fun x => c + x
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ n.natAbs = 1 ↔ a ^ n = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>n.natAbs • a = 0 ↔ n • a = 0
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>h : n • a = 0<GOAL>∃ n, 0 < n ∧ n • a = 0
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>h : a ^ n = 1<GOAL>∃ n, 0 < n ∧ a ^ n = 1
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>(m - n) • a = m • a + -(n • a)
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>(m - n) • -a = -(m • a) + n • a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>(n + 1) • a = n • a + a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n + 1) = a ^ n * a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>(n - 1) • a = n • a + -a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n - 1) = a ^ n * a⁻¹
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>m n : ℤ<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>m n : ℤ<GOAL>(m + n) • a = m • a + n • a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (1 + n) = a * a ^ n
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>(1 + n) • a = a + n • a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a * a ^ n = a ^ (n + 1)
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>a + n • a = (n + 1) • a
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>n • a + a = (n + 1) • a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ n * a = a ^ (n + 1)
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>m n : ℤ<GOAL>(m - n) • a = m • a + -(n • a)
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>m n : ℤ<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>G : Type u_3<VAR>AddGroup G<VAR>a : G<VAR>m n : ℤ<GOAL>m • a + n • a = n • a + m • a
<VAR>G : Type u_3<VAR>Group G<VAR>a : G<VAR>m n : ℤ<GOAL>a ^ m * a ^ n = a ^ n * a ^ m
<VAR>G : Type u_3<VAR>Group G<VAR>x : G<VAR>m : ℤ<VAR>n : ℤ<VAR>h : x ^ n = 1<GOAL>x ^ m = x ^ (m % n)
<VAR>G : Type u_3<VAR>Group G<VAR>x : G<VAR>m : ℤ<VAR>n : ℕ<VAR>h : x ^ n = 1<GOAL>x ^ m = x ^ (m % ↑n)
<VAR>G : Type u_3<VAR>AddGroup G<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 0<VAR>h_mul : ∀ (a : G), P a → P (g + a)<VAR>h_inv : ∀ (a : G), P a → P (-g + a)<VAR>n : ℤ<GOAL>P (n • g)
<VAR>G : Type u_3<VAR>Group G<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (g * a)<VAR>h_inv : ∀ (a : G), P a → P (g⁻¹ * a)<VAR>n : ℤ<GOAL>P (g ^ n)
<VAR>G : Type u_3<VAR>AddGroup G<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 0<VAR>h_mul : ∀ (a : G), P a → P (a + g)<VAR>h_inv : ∀ (a : G), P a → P (a + -g)<VAR>n : ℤ<GOAL>P (n • g)
<VAR>G : Type u_3<VAR>Group G<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (a * g)<VAR>h_inv : ∀ (a : G), P a → P (a * g⁻¹)<VAR>n : ℤ<GOAL>P (g ^ n)
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<VAR>h : a = b * c<GOAL>a / b = c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<VAR>h : a = b + c<GOAL>a - b = c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>c + a - (c + b) = a - b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>c * a / (c * b) = a / b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<VAR>h : c * a = b<GOAL>a = b / c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<VAR>h : c + a = b<GOAL>a = b - c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<VAR>h : a - b = c<GOAL>a = b + c
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<VAR>h : a / b = c<GOAL>a = b * c
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<VAR>h : b = c / a<GOAL>a * b = c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<VAR>h : b = c - a<GOAL>a + b = c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b : G<GOAL>a - (a - b) = b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b : G<GOAL>a / (a / b) = b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a - b = c - b + (a - c)
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a / b = c / b * (a / c)
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b : G<GOAL>a / b / a = b⁻¹
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b : G<GOAL>a - b - a = -b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a = b / c ↔ c * a = b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a = b - c ↔ c + a = b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a - b = c ↔ a = b + c
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a / b = c ↔ a = b * c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b : G<GOAL>a + b - a = b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b : G<GOAL>a * b / a = b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b : G<GOAL>a * (b / a) = b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b : G<GOAL>a + (b - a) = b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b : G<GOAL>a / (a * b) = b⁻¹
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b : G<GOAL>a - (a + b) = -b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b : G<GOAL>a + (b + -a) = b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b : G<GOAL>a * (b * a⁻¹) = b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a + c + (b - c) = a + b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a * c * (b / c) = a * b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a / c * (b * c) = a * b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a - c + (b + c) = a + b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a - b + (c - a) = c - b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a / b * (c / a) = c / b
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>a * b / (a / c) = b * c
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>a + b - (a - c) = b + c
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c : G<GOAL>c / a / (c / b) = b / a
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c : G<GOAL>c - a - (c - b) = b - a
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c d : G<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c d : G<GOAL>a - b = c - d ↔ a + d = c + b
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>a b c d : G<GOAL>a - b = c - d ↔ a - c = b - d
<VAR>G : Type u_3<VAR>CommGroup G<VAR>a b c d : G<GOAL>a / b = c / d ↔ a / c = b / d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid β<VAR>p r : α → α → Prop<VAR>IsTotal α r<VAR>f : α → α → β<VAR>hsymm : Symmetric p<VAR>hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c<VAR>a b c : α<VAR>pab : p a b<VAR>pbc : p b c<VAR>pac : p a c<GOAL>f a c = f a b * f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoid β<VAR>p r : α → α → Prop<VAR>IsTotal α r<VAR>f : α → α → β<VAR>hsymm : Symmetric p<VAR>hf_swap : ∀ {a b : α}, p a b → f a b + f b a = 0<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b + f b c<VAR>a b c : α<VAR>pab : p a b<VAR>pbc : p b c<VAR>pac : p a c<GOAL>f a c = f a b + f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoid β<VAR>r : α → α → Prop<VAR>IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b + f b a = 0<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b + f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>f a c = f a b + f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid β<VAR>r : α → α → Prop<VAR>IsTotal α r<VAR>f : α → α → β<VAR>p : α → Prop<VAR>hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c<VAR>a b c : α<VAR>pa : p a<VAR>pb : p b<VAR>pc : p c<GOAL>f a c = f a b * f b c
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>S : Subgroup G<VAR>g : ↥S<VAR>m : α<GOAL>g • m = ↑g • m
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>S : AddSubgroup G<VAR>g : ↥S<VAR>m : α<GOAL>g +ᵥ m = ↑g +ᵥ m
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>S : AddSubgroup G<VAR>g : G<VAR>hg : g ∈ S<VAR>a : α<GOAL>⟨g, hg⟩ +ᵥ a = g +ᵥ a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>S : Subgroup G<VAR>g : G<VAR>hg : g ∈ S<VAR>a : α<GOAL>⟨g, hg⟩ • a = g • a
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>g ∈ Subgroup.zpowers g
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>↑(Subgroup.zpowers g) = Set.range fun x => g ^ x
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>Subgroup.zpowers g = Subgroup.closure {g}
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>((zpowersHom G) g).range = Subgroup.zpowers g
<VAR>G : Type u_1<VAR>Group G<VAR>g h : G<GOAL>h ∈ Subgroup.zpowers g ↔ ∃ k, g ^ k = h
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>k : ℤ<GOAL>g ^ k ∈ Subgroup.zpowers g
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>k : ℕ<GOAL>g ^ k ∈ Subgroup.zpowers g
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>p : ↥(Subgroup.zpowers x) → Prop<GOAL>(∀ (g : ↥(Subgroup.zpowers x)), p g) ↔ ∀ (m : ℤ), p ⟨x ^ m, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>p : ↥(Subgroup.zpowers x) → Prop<GOAL>(∃ g, p g) ↔ ∃ m, p ⟨x ^ m, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>p : G → Prop<GOAL>(∀ g ∈ Subgroup.zpowers x, p g) ↔ ∀ (m : ℤ), p (x ^ m)
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<VAR>p : G → Prop<GOAL>(∃ g ∈ Subgroup.zpowers x, p g) ↔ ∃ m, p (x ^ m)
<VAR>A : Type u_2<VAR>AddGroup A<VAR>a : A<GOAL>((zmultiplesHom A) a).range = AddSubgroup.zmultiples a
<VAR>R : Type u_4<VAR>Ring R<VAR>r : R<VAR>k : ℤ<GOAL>↑k * r ∈ AddSubgroup.zmultiples r
<VAR>R : Type u_4<VAR>Ring R<VAR>k : ℤ<GOAL>↑k ∈ AddSubgroup.zmultiples 1
<VAR>A : Type u_4<VAR>AddGroupWithOne A<GOAL>(Int.castAddHom A).range = AddSubgroup.zmultiples 1
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_3<VAR>Group N<VAR>f : G →* N<VAR>x : G<GOAL>Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_3<VAR>AddGroup N<VAR>f : G →+ N<VAR>x : G<GOAL>AddSubgroup.map f (AddSubgroup.zmultiples x) = AddSubgroup.zmultiples (f x)
<VAR>a b : ℤ<GOAL>b ∈ AddSubgroup.zmultiples a ↔ a ∣ b
<VAR>G : Type u_1<VAR>Group G<VAR>x : G<GOAL>⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))
<VAR>A : Type u_2<VAR>AddGroup A<VAR>x : A<GOAL>⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<VAR>H : AddSubgroup G<GOAL>AddSubgroup.zmultiples g ≤ H ↔ g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>H : Subgroup G<GOAL>Subgroup.zpowers g ≤ H ↔ g ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<GOAL>AddSubgroup.zmultiples g = ⊥ ↔ g = 0
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>Subgroup.zpowers g = ⊥ ↔ g = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<GOAL>AddSubgroup.zmultiples g ≠ ⊥ ↔ g ≠ 0
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>Subgroup.zpowers g ≠ ⊥ ↔ g ≠ 1
<VAR>G : Type u_1<VAR>Group G<GOAL>Subgroup.zpowers 1 = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>AddSubgroup.zmultiples 0 = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<GOAL>Subgroup.centralizer ↑(Subgroup.closure S) = ⨅ g ∈ S, Subgroup.centralizer ↑(Subgroup.zpowers g)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<GOAL>AddSubgroup.centralizer ↑(AddSubgroup.closure S) = ⨅ g ∈ S, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples g)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<VAR>hS : AddSubgroup.closure S = ⊤<GOAL>AddSubgroup.center G = ⨅ g ∈ S, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples g)
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>hS : Subgroup.closure S = ⊤<GOAL>Subgroup.center G = ⨅ g ∈ S, Subgroup.centralizer ↑(Subgroup.zpowers g)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>S : Set G<VAR>hS : AddSubgroup.closure S = ⊤<GOAL>AddSubgroup.center G = ⨅ g, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples ↑g)
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>hS : Subgroup.closure S = ⊤<GOAL>Subgroup.center G = ⨅ g, Subgroup.centralizer ↑(Subgroup.zpowers ↑g)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>↑H.op = AddOpposite.unop ⁻¹' ↑H
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<GOAL>↑H.op = MulOpposite.unop ⁻¹' ↑H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>x : Gᵃᵒᵖ<VAR>S : AddSubgroup G<GOAL>x ∈ S.op ↔ AddOpposite.unop x ∈ S
<VAR>G : Type u_2<VAR>Group G<VAR>x : Gᵐᵒᵖ<VAR>S : Subgroup G<GOAL>x ∈ S.op ↔ MulOpposite.unop x ∈ S
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<GOAL>H.op.toSubmonoid = H.op
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.op.toAddSubmonoid = H.op
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup Gᵐᵒᵖ<GOAL>↑H.unop = MulOpposite.op ⁻¹' ↑H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup Gᵃᵒᵖ<GOAL>↑H.unop = AddOpposite.op ⁻¹' ↑H
<VAR>G : Type u_2<VAR>AddGroup G<VAR>x : G<VAR>S : AddSubgroup Gᵃᵒᵖ<GOAL>x ∈ S.unop ↔ AddOpposite.op x ∈ S
<VAR>G : Type u_2<VAR>Group G<VAR>x : G<VAR>S : Subgroup Gᵐᵒᵖ<GOAL>x ∈ S.unop ↔ MulOpposite.op x ∈ S
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup Gᵐᵒᵖ<GOAL>H.unop.toSubmonoid = H.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup Gᵃᵒᵖ<GOAL>H.unop.toAddSubmonoid = H.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : AddSubgroup G<GOAL>S.op.unop = S
<VAR>G : Type u_2<VAR>Group G<VAR>S : Subgroup G<GOAL>S.op.unop = S
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : AddSubgroup Gᵃᵒᵖ<GOAL>S.unop.op = S
<VAR>G : Type u_2<VAR>Group G<VAR>S : Subgroup Gᵐᵒᵖ<GOAL>S.unop.op = S
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ : Subgroup G<VAR>S₂ : Subgroup Gᵐᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ : AddSubgroup G<VAR>S₂ : AddSubgroup Gᵃᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ : AddSubgroup Gᵃᵒᵖ<VAR>S₂ : AddSubgroup G<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ : Subgroup Gᵐᵒᵖ<VAR>S₂ : Subgroup G<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ S₂ : AddSubgroup G<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ S₂ : Subgroup G<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ S₂ : AddSubgroup Gᵃᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ S₂ : Subgroup Gᵐᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup Gᵃᵒᵖ<GOAL>(RelIso.symm AddSubgroup.opEquiv) H = H.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>AddSubgroup.opEquiv H = H.op
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup Gᵐᵒᵖ<GOAL>(RelIso.symm Subgroup.opEquiv) H = H.unop
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<GOAL>Subgroup.opEquiv H = H.op
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>⊥.op = ⊥
<VAR>G : Type u_2<VAR>Group G<GOAL>⊥.op = ⊥
<VAR>G : Type u_2<VAR>Group G<GOAL>⊥.unop = ⊥
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>⊥.unop = ⊥
<VAR>G : Type u_2<VAR>Group G<GOAL>⊤.op = ⊤
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>⊤.op = ⊤
<VAR>G : Type u_2<VAR>AddGroup G<GOAL>⊤.unop = ⊤
<VAR>G : Type u_2<VAR>Group G<GOAL>⊤.unop = ⊤
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ S₂ : Subgroup G<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ S₂ : AddSubgroup G<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ S₂ : Subgroup Gᵐᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ S₂ : AddSubgroup Gᵃᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ S₂ : Subgroup G<GOAL>(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ S₂ : AddSubgroup G<GOAL>(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S₁ S₂ : AddSubgroup Gᵃᵒᵖ<GOAL>(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
<VAR>G : Type u_2<VAR>Group G<VAR>S₁ S₂ : Subgroup Gᵐᵒᵖ<GOAL>(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : Set (AddSubgroup G)<GOAL>(sSup S).op = sSup (AddSubgroup.unop ⁻¹' S)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Set (Subgroup G)<GOAL>(sSup S).op = sSup (Subgroup.unop ⁻¹' S)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : Set (AddSubgroup Gᵃᵒᵖ)<GOAL>(sSup S).unop = sSup (AddSubgroup.op ⁻¹' S)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Set (Subgroup Gᵐᵒᵖ)<GOAL>(sSup S).unop = sSup (Subgroup.op ⁻¹' S)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Set (Subgroup G)<GOAL>(sInf S).op = sInf (Subgroup.unop ⁻¹' S)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : Set (AddSubgroup G)<GOAL>(sInf S).op = sInf (AddSubgroup.unop ⁻¹' S)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : Set (AddSubgroup Gᵃᵒᵖ)<GOAL>(sInf S).unop = sInf (AddSubgroup.op ⁻¹' S)
<VAR>G : Type u_2<VAR>Group G<VAR>S : Set (Subgroup Gᵐᵒᵖ)<GOAL>(sInf S).unop = sInf (Subgroup.op ⁻¹' S)
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>Group G<VAR>S : ι → Subgroup G<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : ι → AddSubgroup G<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>Group G<VAR>S : ι → Subgroup Gᵐᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : ι → AddSubgroup Gᵃᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>Group G<VAR>S : ι → Subgroup G<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : ι → AddSubgroup G<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>S : ι → AddSubgroup Gᵃᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>Group G<VAR>S : ι → Subgroup Gᵐᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set G<GOAL>(AddSubgroup.closure s).op = AddSubgroup.closure (AddOpposite.unop ⁻¹' s)
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set G<GOAL>(Subgroup.closure s).op = Subgroup.closure (MulOpposite.unop ⁻¹' s)
<VAR>G : Type u_2<VAR>Group G<VAR>s : Set Gᵐᵒᵖ<GOAL>(Subgroup.closure s).unop = Subgroup.closure (MulOpposite.op ⁻¹' s)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>s : Set Gᵃᵒᵖ<GOAL>(AddSubgroup.closure s).unop = AddSubgroup.closure (AddOpposite.op ⁻¹' s)
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>b : { b // (fun x => x ∈ H.op) b }<GOAL>↑(H.equivOp.symm b) = AddOpposite.unop ↑b
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>a : { a // (fun x => x ∈ H) a }<GOAL>↑(H.equivOp a) = AddOpposite.op ↑a
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>b : { b // (fun x => x ∈ H.op) b }<GOAL>↑(H.equivOp.symm b) = MulOpposite.unop ↑b
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>a : { a // (fun x => x ∈ H) a }<GOAL>↑(H.equivOp a) = MulOpposite.op ↑a
<VAR>G : Type u_2<VAR>Group G<VAR>H : Subgroup G<VAR>x g : G<VAR>h : ↥H.op<GOAL>h • (g * x) = g * h • x
<VAR>G : Type u_2<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>x g : G<VAR>h : ↥H.op<GOAL>h +ᵥ (g + x) = g + (h +ᵥ x)
<VAR>S : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>LinearOrder G<GOAL>∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, |x_1| ∈ H ↔ x_1 ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hnc : NormalizerCondition G<VAR>hmax : IsCoatom H<GOAL>H.Normal
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : G ≃* H<VAR>K : Subgroup H<GOAL>IsCoatom (Subgroup.comap (↑f) K) ↔ IsCoatom K
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>f : G ≃* ↥H<VAR>K : Subgroup G<GOAL>IsCoatom (Subgroup.map (↑f) K) ↔ IsCoatom K
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>M : Subgroup H<VAR>hM : IsCoatom M<GOAL>IsCoatom (Subgroup.comap φ M)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>a x y : M<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>h : SemiconjBy a x y<VAR>f : F<GOAL>SemiconjBy (f a) (f x) (f y)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>a x y : M<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>h : AddSemiconjBy a x y<VAR>f : F<GOAL>AddSemiconjBy (f a) (f x) (f y)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>x y : M<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>h : Commute x y<VAR>f : F<GOAL>Commute (f x) (f y)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>x y : M<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>h : AddCommute x y<VAR>f : F<GOAL>AddCommute (f x) (f y)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>a x y : M<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : SemiconjBy (f a) (f x) (f y)<GOAL>SemiconjBy a x y
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>a x y : M<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : AddSemiconjBy (f a) (f x) (f y)<GOAL>AddSemiconjBy a x y
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Add M<VAR>Add N<VAR>x y : M<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : AddCommute (f x) (f y)<GOAL>AddCommute x y
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Mul M<VAR>Mul N<VAR>x y : M<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : Commute (f x) (f y)<GOAL>Commute x y
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<GOAL>Commute a b → Commute a⁻¹ b⁻¹
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<GOAL>AddCommute a b → AddCommute (-a) (-b)
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b : G<GOAL>AddCommute (-a) (-b) ↔ AddCommute a b
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b : G<GOAL>Commute a⁻¹ b⁻¹ ↔ Commute a b
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b c d : G<VAR>hbd : Commute b d<VAR>hbc : Commute b⁻¹ c<GOAL>a / b * (c / d) = a * c / (b * d)
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b c d : G<VAR>hbd : AddCommute b d<VAR>hbc : AddCommute (-b) c<GOAL>a - b + (c - d) = a + c - (b + d)
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b c d : G<VAR>hcd : AddCommute c d<VAR>hbc : AddCommute b (-c)<GOAL>a + b - (c + d) = a - c + (b - d)
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b c d : G<VAR>hcd : Commute c d<VAR>hbc : Commute b c⁻¹<GOAL>a * b / (c * d) = a / c * (b / d)
<VAR>G : Type u_1<VAR>DivisionMonoid G<VAR>a b c d : G<VAR>hbc : Commute b c<VAR>hbd : Commute b⁻¹ d<VAR>hcd : Commute c⁻¹ d<GOAL>a / b / (c / d) = a / c / (b / d)