ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>xs : List Nat<VAR>y : Nat<VAR>h : y ≠ 0<GOAL>xs.nonzeroMinimum = y ↔ y ∈ xs ∧ ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
<VAR>xs : List Nat<VAR>h : xs.nonzeroMinimum ≠ 0<GOAL>∃ x, x ∈ xs ∧ xs.nonzeroMinimum = x
<VAR>xs : List Nat<VAR>y : Nat<GOAL>xs.nonzeroMinimum ≤ y ↔ xs.nonzeroMinimum = 0 ∨ ∃ x, x ∈ xs ∧ x ≤ y ∧ x ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : α → Nat<VAR>q : β → Nat<VAR>xs : List α<VAR>h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)<VAR>w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a<GOAL>(List.map q (List.map f xs)).nonzeroMinimum ≤ (List.map p xs).nonzeroMinimum
<VAR>xs : List Int<GOAL>xs.minNatAbs = 0 ↔ ∀ (y : Int), y ∈ xs → y = 0
<VAR>z : Nat<VAR>xs : List Int<VAR>w : z ≠ 0<GOAL>xs.minNatAbs = z ↔ (∃ y, y ∈ xs ∧ y.natAbs = z) ∧ ∀ (y : Int), y ∈ xs → z ≤ y.natAbs ∨ y = 0
<VAR>self : Lean.Elab.Tactic.Omega.Problem<GOAL>(self.possible || self.proveFalse?.isSome) = true
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>z : M<GOAL>z ∈ AddSubsemigroup.center M ↔ ∀ (g : M), g + z = z + g
<VAR>M : Type u_1<VAR>Semigroup M<VAR>z : M<GOAL>z ∈ Subsemigroup.center M ↔ ∀ (g : M), g * z = z * g
<VAR>M : Type u_1<VAR>CommSemigroup M<GOAL>Subsemigroup.center M = ⊤
<VAR>M : Type u_1<VAR>AddCommSemigroup M<GOAL>AddSubsemigroup.center M = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Mul M<VAR>Mul N<VAR>Semigroup P<VAR>f : M →ₙ* P<VAR>g : N →ₙ* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<VAR>mn : M × N<GOAL>(f.noncommCoprod g comm) mn = f mn.1 * g mn.2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Add M<VAR>Add N<VAR>AddSemigroup P<VAR>f : AddHom M P<VAR>g : AddHom N P<VAR>comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)<VAR>mn : M × N<GOAL>(f.noncommCoprod g comm) mn = f mn.1 + g mn.2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Mul M<VAR>Mul N<VAR>Semigroup P<VAR>f : M →ₙ* P<VAR>g : N →ₙ* P<VAR>Q : Type u_4<VAR>Semigroup Q<VAR>h : P →ₙ* Q<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<GOAL>h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Add M<VAR>Add N<VAR>AddSemigroup P<VAR>f : AddHom M P<VAR>g : AddHom N P<VAR>Q : Type u_4<VAR>AddSemigroup Q<VAR>h : AddHom P Q<VAR>comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)<GOAL>h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<VAR>mn : M × N<GOAL>(f.noncommCoprod g comm) mn = f mn.1 * g mn.2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)<VAR>mn : M × N<GOAL>(f.noncommCoprod g comm) mn = f mn.1 + g mn.2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<GOAL>(f.noncommCoprod g comm).comp (MonoidHom.inl M N) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)<GOAL>(f.noncommCoprod g comm).comp (AddMonoidHom.inl M N) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)<GOAL>(f.noncommCoprod g comm).comp (AddMonoidHom.inr M N) = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<GOAL>(f.noncommCoprod g comm).comp (MonoidHom.inr M N) = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M × N →* P<GOAL>(f.comp (MonoidHom.inl M N)).noncommCoprod (f.comp (MonoidHom.inr M N)) ⋯ = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M × N →+ P<GOAL>(f.comp (AddMonoidHom.inl M N)).noncommCoprod (f.comp (AddMonoidHom.inr M N)) ⋯ = f
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<GOAL>(MonoidHom.inl M N).noncommCoprod (MonoidHom.inr M N) ⋯ = MonoidHom.id (M × N)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<GOAL>(AddMonoidHom.inl M N).noncommCoprod (AddMonoidHom.inr M N) ⋯ = AddMonoidHom.id (M × N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>Monoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<VAR>Q : Type u_4<VAR>Monoid Q<VAR>h : P →* Q<GOAL>h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddMonoid P<VAR>f : M →+ P<VAR>g : N →+ P<VAR>comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)<VAR>Q : Type u_4<VAR>AddMonoid Q<VAR>h : P →+ Q<GOAL>h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
<VAR>M : Type u_1<VAR>S : Set M<VAR>Semigroup M<GOAL>↑(Subsemigroup.centralizer S) = S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddSemigroup M<GOAL>↑(AddSubsemigroup.centralizer S) = S.addCentralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Semigroup M<VAR>z : M<GOAL>z ∈ Subsemigroup.centralizer S ↔ ∀ g ∈ S, g * z = z * g
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddSemigroup M<VAR>z : M<GOAL>z ∈ AddSubsemigroup.centralizer S ↔ ∀ g ∈ S, g + z = z + g
<VAR>M : Type u_1<VAR>Semigroup M<VAR>S : Set M<GOAL>Subsemigroup.center M ≤ Subsemigroup.centralizer S
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>S : Set M<GOAL>AddSubsemigroup.center M ≤ AddSubsemigroup.centralizer S
<VAR>M : Type u_1<VAR>S T : Set M<VAR>Semigroup M<VAR>h : S ⊆ T<GOAL>Subsemigroup.centralizer T ≤ Subsemigroup.centralizer S
<VAR>M : Type u_1<VAR>S T : Set M<VAR>AddSemigroup M<VAR>h : S ⊆ T<GOAL>AddSubsemigroup.centralizer T ≤ AddSubsemigroup.centralizer S
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>s : Set M<GOAL>AddSubsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubsemigroup.center M)
<VAR>M : Type u_1<VAR>Semigroup M<VAR>s : Set M<GOAL>Subsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subsemigroup.center M)
<VAR>M : Type u_1<VAR>Semigroup M<GOAL>Subsemigroup.centralizer Set.univ = Subsemigroup.center M
<VAR>M : Type u_1<VAR>AddSemigroup M<GOAL>AddSubsemigroup.centralizer Set.univ = AddSubsemigroup.center M
<VAR>M : Type u_1<VAR>S : Set M<VAR>Monoid M<GOAL>↑(Submonoid.centralizer S) = S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddMonoid M<GOAL>↑(AddSubmonoid.centralizer S) = S.addCentralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Monoid M<GOAL>(Submonoid.centralizer S).toSubsemigroup = Subsemigroup.centralizer S
<VAR>M : Type u_2<VAR>AddMonoid M<VAR>S : Set M<GOAL>(AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
<VAR>M : Type u_1<VAR>S : Set M<VAR>Monoid M<VAR>z : M<GOAL>z ∈ Submonoid.centralizer S ↔ ∀ g ∈ S, g * z = z * g
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddMonoid M<VAR>z : M<GOAL>z ∈ AddSubmonoid.centralizer S ↔ ∀ g ∈ S, g + z = z + g
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>Submonoid.center M ≤ Submonoid.centralizer s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>AddSubmonoid.center M ≤ AddSubmonoid.centralizer s
<VAR>M : Type u_1<VAR>S T : Set M<VAR>AddMonoid M<VAR>h : S ⊆ T<GOAL>AddSubmonoid.centralizer T ≤ AddSubmonoid.centralizer S
<VAR>M : Type u_1<VAR>S T : Set M<VAR>Monoid M<VAR>h : S ⊆ T<GOAL>Submonoid.centralizer T ≤ Submonoid.centralizer S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>AddSubmonoid.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubmonoid.center M)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>Submonoid.centralizer s = ⊤ ↔ s ⊆ ↑(Submonoid.center M)
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Submonoid.centralizer Set.univ = Submonoid.center M
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>AddSubmonoid.centralizer Set.univ = AddSubmonoid.center M
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : AddSubmonoid M<GOAL>s ≤ AddSubmonoid.centralizer ↑(AddSubmonoid.centralizer ↑s)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Submonoid M<GOAL>s ≤ Submonoid.centralizer ↑(Submonoid.centralizer ↑s)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>AddSubmonoid.centralizer s.addCentralizer.addCentralizer = AddSubmonoid.centralizer s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>Submonoid.centralizer s.centralizer.centralizer = Submonoid.centralizer s
<VAR>X : Type u<VAR>_G : MulOneClass X<GOAL>EckmannHilton.IsUnital (fun x x_1 => x * x_1) 1
<VAR>X : Type u<VAR>_G : AddZeroClass X<GOAL>EckmannHilton.IsUnital (fun x x_1 => x + x_1) 0
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : EckmannHilton.IsUnital m₁ e₁<VAR>h₂ : EckmannHilton.IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<GOAL>e₁ = e₂
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : EckmannHilton.IsUnital m₁ e₁<VAR>h₂ : EckmannHilton.IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<GOAL>m₁ = m₂
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : EckmannHilton.IsUnital m₁ e₁<VAR>h₂ : EckmannHilton.IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<GOAL>Std.Commutative m₂
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : EckmannHilton.IsUnital m₁ e₁<VAR>h₂ : EckmannHilton.IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<GOAL>Std.Associative m₂
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>↑(AddSubmonoid.center M) = Set.addCenter M
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>↑(Submonoid.center M) = Set.center M
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>(Submonoid.center M).toSubsemigroup = Subsemigroup.center M
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>(AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>z : M<GOAL>z ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + z = z + g
<VAR>M : Type u_1<VAR>Monoid M<VAR>z : M<GOAL>z ∈ Submonoid.center M ↔ ∀ (g : M), g * z = z * g
<VAR>M : Type u_1<VAR>CommMonoid M<GOAL>Submonoid.center M = ⊤
<VAR>M : Type u_1<VAR>Monoid M<VAR>n : (↥(Submonoid.center M))ˣ<GOAL>↑↑((unitsCenterToCenterUnits M) n) = ↑↑n
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>n : AddUnits ↥(AddSubmonoid.center M)<GOAL>↑↑((addUnitsCenterToCenterAddUnits M) n) = ↑↑n
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Function.Injective ⇑(unitsCenterToCenterUnits M)
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>Function.Injective ⇑(addUnitsCenterToCenterAddUnits M)
<VAR>G : Type u_1<VAR>Group G<VAR>self : IsSimpleGroup G<VAR>H : Subgroup G<GOAL>H.Normal → H = ⊥ ∨ H = ⊤
<VAR>A : Type u_2<VAR>AddGroup A<VAR>self : IsSimpleAddGroup A<VAR>H : AddSubgroup A<GOAL>H.Normal → H = ⊥ ∨ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>IsSimpleAddGroup G<VAR>H : AddSubgroup G<VAR>Hn : H.Normal<GOAL>H = ⊥ ∨ H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>IsSimpleGroup G<VAR>H : Subgroup G<VAR>Hn : H.Normal<GOAL>H = ⊥ ∨ H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : Type u_3<VAR>AddGroup H<VAR>IsSimpleAddGroup G<VAR>Nontrivial H<VAR>f : G →+ H<VAR>hf : Function.Surjective ⇑f<GOAL>IsSimpleAddGroup H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_3<VAR>Group H<VAR>IsSimpleGroup G<VAR>Nontrivial H<VAR>f : G →* H<VAR>hf : Function.Surjective ⇑f<GOAL>IsSimpleGroup H
<VAR>G : Type u_1<VAR>φ : G → G<VAR>Div G<VAR>g : G<GOAL>MonoidHom.commutatorMap φ g = g / φ g
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<GOAL>Function.Injective (MonoidHom.commutatorMap ⇑φ)
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<GOAL>Function.Surjective (MonoidHom.commutatorMap ⇑φ)
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>n : ℕ<VAR>hn : (⇑φ)^[n] = id<VAR>g : G<GOAL>(List.map (fun k => (⇑φ)^[k] g) (List.range n)).prod = 1
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>h2 : (⇑φ)^[2] = id<GOAL>⇑φ = fun x => x⁻¹
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<GOAL>⇑φ = fun x => x⁻¹
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g h : G<GOAL>Commute g h
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g : G<GOAL>orderOf g ≠ 2
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<GOAL>Odd (Nat.card G)
<VAR>G : Type u_1<VAR>Group G<VAR>φ : G →* G<VAR>Finite G<VAR>hφ : MonoidHom.FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g : G<GOAL>Odd (orderOf g)
<VAR>α : Type u_1<VAR>AddMonoid α<GOAL>AddMonoid.minOrder α = ⊤ ↔ AddMonoid.IsTorsionFree α
<VAR>α : Type u_1<VAR>Monoid α<GOAL>Monoid.minOrder α = ⊤ ↔ Monoid.IsTorsionFree α
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>n : ℕ∞<GOAL>n ≤ AddMonoid.minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 0 → IsOfFinAddOrder a → n ≤ ↑(addOrderOf a)
<VAR>α : Type u_1<VAR>Monoid α<VAR>n : ℕ∞<GOAL>n ≤ Monoid.minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>a : α<VAR>ha : a ≠ 0<VAR>ha' : IsOfFinAddOrder a<GOAL>AddMonoid.minOrder α ≤ ↑(addOrderOf a)
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<VAR>ha : a ≠ 1<VAR>ha' : IsOfFinOrder a<GOAL>Monoid.minOrder α ≤ ↑(orderOf a)
<VAR>α : Type u_1<VAR>Group α<VAR>n : ℕ∞<GOAL>n ≤ Monoid.minOrder α ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>n : ℕ∞<GOAL>n ≤ AddMonoid.minOrder α ↔ ∀ ⦃s : AddSubgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>hs : s ≠ ⊥<VAR>hs' : (↑s).Finite<GOAL>Monoid.minOrder α ≤ ↑(Nat.card ↥s)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>hs : s ≠ ⊥<VAR>hs' : (↑s).Finite<GOAL>AddMonoid.minOrder α ≤ ↑(Nat.card ↥s)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn₁ : n ≠ 1<GOAL>AddMonoid.minOrder (ZMod n) = ↑n.minFac
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>AddMonoid.minOrder (ZMod p) = ↑p
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Saturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Saturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Saturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Saturated ↔ ∀ (n : ℤ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
<VAR>A₁ : Type u_1<VAR>A₂ : Type u_2<VAR>AddCommGroup A₁<VAR>AddCommGroup A₂<VAR>NoZeroSMulDivisors ℕ A₂<VAR>f : A₁ →+ A₂<GOAL>f.ker.Saturated
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>s : Set G<GOAL>g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, h * g = g * h
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<VAR>s : Set G<GOAL>g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, h + g = g + h
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<VAR>s : Set G<GOAL>g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, h + g + -h + -g = 0
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>s : Set G<GOAL>g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>AddSubgroup.centralizer Set.univ = AddSubgroup.center G
<VAR>G : Type u_1<VAR>Group G<GOAL>Subgroup.centralizer Set.univ = Subgroup.center G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H ≤ AddSubgroup.centralizer ↑K ↔ K ≤ AddSubgroup.centralizer ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>H ≤ Subgroup.centralizer ↑K ↔ K ≤ Subgroup.centralizer ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>AddSubgroup.center G ≤ AddSubgroup.centralizer s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.center G ≤ Subgroup.centralizer s
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>h : s ⊆ t<GOAL>Subgroup.centralizer t ≤ Subgroup.centralizer s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s t : Set G<VAR>h : s ⊆ t<GOAL>AddSubgroup.centralizer t ≤ AddSubgroup.centralizer s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subgroup.center G)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>AddSubgroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubgroup.center G)
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<GOAL>K ≤ Subgroup.centralizer ↑K ↔ K.IsCommutative
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<GOAL>K ≤ AddSubgroup.centralizer ↑K ↔ K.IsCommutative
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>h : H.IsCommutative<GOAL>H ≤ Subgroup.centralizer ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>h : H.IsCommutative<GOAL>H ≤ AddSubgroup.centralizer ↑H
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : ↥(IsAddUnit.addSubmonoid M)<GOAL>↑(-x) = ↑(-IsAddUnit.addUnit ⋯)
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : ↥(IsUnit.submonoid M)<GOAL>↑x⁻¹ = ↑(IsUnit.unit ⋯)⁻¹
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<GOAL>S.leftInv.leftInv ≤ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<GOAL>S.leftNeg.leftNeg ≤ S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : AddUnits M<VAR>hx : ↑x ∈ S<GOAL>↑(-x) ∈ S.leftNeg
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : Mˣ<VAR>hx : ↑x ∈ S<GOAL>↑x⁻¹ ∈ S.leftInv
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<GOAL>S.leftInv.leftInv = S
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<GOAL>S.leftNeg.leftNeg = S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : ↥S.leftInv<GOAL>↑x * ↑(S.fromLeftInv x) = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : ↥S.leftNeg<GOAL>↑x + ↑(S.fromLeftNeg x) = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<GOAL>S.fromLeftInv 1 = 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<GOAL>S.fromLeftNeg 0 = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>x : ↥S.leftInv<GOAL>↑(S.fromLeftInv x) * ↑x = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>x : ↥S.leftNeg<GOAL>↑(S.fromLeftNeg x) + ↑x = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<GOAL>S.leftInv ≤ IsUnit.submonoid M
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>S.leftNeg ≤ IsAddUnit.addSubmonoid M
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>a : ↥S.leftInv<VAR>b : M<GOAL>↑(S.fromLeftInv a) = b ↔ ↑a * b = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>a : ↥S.leftNeg<VAR>b : M<GOAL>↑(S.fromLeftNeg a) = b ↔ ↑a + b = 0
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>∀ (a : ↥S.leftNeg), S.fromCommLeftNeg a = S.fromLeftNeg a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<GOAL>∀ (a : ↥S.leftInv), S.fromCommLeftInv a = S.fromLeftInv a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<GOAL>∀ (a : ↥S.leftInv), (S.leftInvEquiv hS) a = (↑S.fromCommLeftInv).toFun a
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<GOAL>∀ (a : ↥S.leftNeg), (S.leftNegEquiv hS) a = (↑S.fromCommLeftNeg).toFun a
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S<GOAL>S.fromLeftNeg ((S.leftNegEquiv hS).symm x) = x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>S.fromLeftInv ((S.leftInvEquiv hS).symm x) = x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<GOAL>(S.leftInvEquiv hS).symm (S.fromLeftInv x) = x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S.leftNeg<GOAL>(S.leftNegEquiv hS).symm (S.fromLeftNeg x) = x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<GOAL>↑((S.leftInvEquiv hS) x) * ↑x = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S.leftNeg<GOAL>↑((S.leftNegEquiv hS) x) + ↑x = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<GOAL>↑x * ↑((S.leftInvEquiv hS) x) = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S.leftNeg<GOAL>↑x + ↑((S.leftNegEquiv hS) x) = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑((S.leftInvEquiv hS).symm x) * ↑x = 1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S<GOAL>↑((S.leftNegEquiv hS).symm x) + ↑x = 0
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S<GOAL>↑x + ↑((S.leftNegEquiv hS).symm x) = 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑x * ↑((S.leftInvEquiv hS).symm x) = 1
<VAR>M : Type u_1<VAR>Group M<VAR>S : Submonoid M<GOAL>S.leftInv = S⁻¹
<VAR>M : Type u_1<VAR>AddGroup M<VAR>S : AddSubmonoid M<GOAL>S.leftNeg = -S
<VAR>M : Type u_1<VAR>AddGroup M<VAR>S : AddSubmonoid M<VAR>x : ↥S.leftNeg<GOAL>↑(S.fromLeftNeg x) = -↑x
<VAR>M : Type u_1<VAR>Group M<VAR>S : Submonoid M<VAR>x : ↥S.leftInv<GOAL>↑(S.fromLeftInv x) = (↑x)⁻¹
<VAR>M : Type u_1<VAR>CommGroup M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑((S.leftInvEquiv hS).symm x) = (↑x)⁻¹
<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>S : AddSubmonoid M<VAR>hS : S ≤ IsAddUnit.addSubmonoid M<VAR>x : ↥S<GOAL>↑((S.leftNegEquiv hS).symm x) = -↑x
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>↑(AddSubgroup.center G) = Set.addCenter G
<VAR>G : Type u_1<VAR>Group G<GOAL>↑(Subgroup.center G) = Set.center G
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>(AddSubgroup.center G).toAddSubmonoid = AddSubmonoid.center G
<VAR>G : Type u_1<VAR>Group G<GOAL>(Subgroup.center G).toSubmonoid = Submonoid.center G
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<VAR>a : ↥(Subgroup.center G₀ˣ)<GOAL>↑↑((Subgroup.centerUnitsEquivUnitsCenter G₀) a) = ↑↑a
<VAR>G₀ : Type u_2<VAR>GroupWithZero G₀<VAR>u : (↥(Submonoid.center G₀))ˣ<GOAL>↑↑((Subgroup.centerUnitsEquivUnitsCenter G₀).symm u) = ↑↑u
<VAR>G : Type u_1<VAR>AddGroup G<VAR>z : G<GOAL>z ∈ AddSubgroup.center G ↔ ∀ (g : G), g + z = z + g
<VAR>G : Type u_1<VAR>Group G<VAR>z : G<GOAL>z ∈ Subgroup.center G ↔ ∀ (g : G), g * z = z * g
<VAR>G : Type u_2<VAR>CommGroup G<GOAL>Subgroup.center G = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Subgroup.center G ≤ H.normalizer
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>AddSubgroup.center G ≤ H.normalizer
<VAR>M : Type u_2<VAR>Monoid M<VAR>g h : M<VAR>H : IsConj g h<VAR>Hg : g ∈ Set.center M<GOAL>g = h
<VAR>M : Type u_2<VAR>Monoid M<VAR>g h : M<VAR>H : IsConj g h<VAR>Hh : h ∈ Set.center M<GOAL>g = h
<VAR>G : Type u_2<VAR>Group G<GOAL>Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (ConjClasses.noncenter G)ᶜ
<VAR>G : Type u_1<VAR>AddMonoid G<GOAL>¬AddMonoid.IsTorsion G ↔ ∃ g, ¬IsOfFinAddOrder g
<VAR>G : Type u_1<VAR>Monoid G<GOAL>¬Monoid.IsTorsion G ↔ ∃ g, ¬IsOfFinOrder g
<VAR>G : Type u_1<VAR>Group G<VAR>tG : Monoid.IsTorsion G<VAR>H : Subgroup G<GOAL>Monoid.IsTorsion ↥H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>tG : AddMonoid.IsTorsion G<VAR>H : AddSubgroup G<GOAL>AddMonoid.IsTorsion ↥H
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G →* H<VAR>hf : Function.Surjective ⇑f<VAR>tG : Monoid.IsTorsion G<GOAL>Monoid.IsTorsion H
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G →+ H<VAR>hf : Function.Surjective ⇑f<VAR>tG : AddMonoid.IsTorsion G<GOAL>AddMonoid.IsTorsion H
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>AddGroup H<VAR>f : G →+ H<VAR>hN : N = f.ker<VAR>tH : AddMonoid.IsTorsion H<VAR>tN : AddMonoid.IsTorsion ↥N<GOAL>AddMonoid.IsTorsion G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>N : Subgroup G<VAR>Group H<VAR>f : G →* H<VAR>hN : N = f.ker<VAR>tH : Monoid.IsTorsion H<VAR>tN : Monoid.IsTorsion ↥N<GOAL>Monoid.IsTorsion G