ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Monoid α<VAR>Unique αˣ<GOAL>Function.Injective Associates.mk
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : α<GOAL>Associates.mk x * Associates.mk y = Associates.mk (x * y)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<GOAL>Associates.mkMonoidHom a = Associates.mk a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>f : Associates α →* α<VAR>hinv : Function.RightInverse (⇑f) Associates.mk<VAR>a : α<GOAL>a ~ᵤ f (Associates.mk a)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<VAR>n : ℕ<GOAL>Associates.mk (a ^ n) = Associates.mk a ^ n
<VAR>α : Type u_1<VAR>CommMonoid α<GOAL>(fun x x_1 => x ∣ x_1) = fun x x_1 => x ≤ x_1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x y : Associates α<GOAL>x * y = 1 ↔ x = 1 ∧ y = 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>u : (Associates α)ˣ<GOAL>u = 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>u : (Associates α)ˣ<GOAL>↑u = 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : Associates α<GOAL>IsUnit a ↔ a = 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : Associates α<GOAL>IsUnit a ↔ a = ⊥
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<GOAL>IsUnit (Associates.mk a) ↔ IsUnit a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b c d : Associates α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a * c ≤ b * d
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : Associates α<GOAL>1 ≤ a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : Associates α<GOAL>a ≤ a * b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : Associates α<GOAL>a ≤ b * a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>Associates.mk a ∣ Associates.mk b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>Associates.mk a ≤ Associates.mk b → a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>a ∣ b → Associates.mk a ≤ Associates.mk b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>Associates.mk a ≤ Associates.mk b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<GOAL>IsPrimal (Associates.mk a) ↔ IsPrimal a
<VAR>α : Type u_1<VAR>CommMonoid α<GOAL>DecompositionMonoid (Associates α) ↔ DecompositionMonoid α
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
<VAR>α : Type u_1<VAR>Zero α<VAR>Monoid α<GOAL>Associates.mk 0 = 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a : α<GOAL>Associates.mk a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<GOAL>Quot.out 0 = 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a : α<GOAL>Associates.mk a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a : Associates α<GOAL>a ≠ 0 → ∃ a0, a0 ≠ 0 ∧ Associates.mk a0 = a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>a : Associates α<GOAL>a ≤ 0
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : Associates α<VAR>hp : Prime p<VAR>a b : Associates α<VAR>h : p ≤ a * b<GOAL>p ≤ a ∨ p ≤ b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<GOAL>Prime (Associates.mk p) ↔ Prime p
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>a : α<GOAL>Irreducible (Associates.mk a) ↔ Irreducible a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>a b : α<GOAL>DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>a b : Associates α<VAR>hlt : a < b<GOAL>DvdNotUnit a b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<GOAL>(∀ (a : α), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates α), Irreducible a ↔ Prime a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecompositionMonoid α<VAR>p : Associates α<GOAL>Irreducible p ↔ Prime p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b c : Associates α<VAR>ha : a ≠ 0<GOAL>a * b ≤ a * c → b ≤ c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p m : Associates α<VAR>hp : Prime p<VAR>hle : m ≤ p<GOAL>m = 1 ∨ m = p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : Associates α<GOAL>DvdNotUnit a b ↔ a < b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : Associates α<GOAL>p ≤ 1 ↔ p = 1
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p q : α<VAR>h : DvdNotUnit p q<VAR>hq : Irreducible q<GOAL>IsUnit p
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p q : α<VAR>hp : ¬IsUnit p<VAR>h : DvdNotUnit p q<GOAL>¬Irreducible q
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p q : α<VAR>hp : DvdNotUnit p q<GOAL>¬IsUnit q
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>Nontrivial α<VAR>p q r : α<VAR>h : DvdNotUnit p q<VAR>h' : q ~ᵤ r<GOAL>DvdNotUnit p r
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p b : α<VAR>h : p * b ~ᵤ p<VAR>hp : p ≠ 0<GOAL>IsUnit b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p q : α<VAR>h : DvdNotUnit p q<GOAL>¬p ~ᵤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p q : α<VAR>h : DvdNotUnit p q<GOAL>p ≠ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>q : α<VAR>hq : ¬IsUnit q<VAR>hq' : q ≠ 0<GOAL>Function.Injective fun n => q ^ n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p q : α<VAR>hp : Prime p<VAR>n : ℕ<GOAL>q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.IsOpenImmersion f ↔ OpenEmbedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
<GOAL>@AlgebraicGeometry.IsOpenImmersion = (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding) ⊓ AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
<GOAL>CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.IsOpenImmersion
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Set S<VAR>hs : IsSubring s<GOAL>IsSubring (⇑f ⁻¹' s)
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Set R<VAR>hs : IsSubring s<GOAL>IsSubring (⇑f '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>IsSubring (Set.range ⇑f)
<VAR>R : Type u<VAR>Ring R<VAR>S₁ S₂ : Set R<VAR>hS₁ : IsSubring S₁<VAR>hS₂ : IsSubring S₂<GOAL>IsSubring (S₁ ∩ S₂)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Sort u_1<VAR>S : ι → Set R<VAR>h : ∀ (y : ι), IsSubring (S y)<GOAL>IsSubring (Set.iInter S)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>s : ι → Set R<VAR>h : ∀ (i : ι), IsSubring (s i)<VAR>directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k<GOAL>IsSubring (⋃ i, s i)
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>a : R<VAR>h : a ∈ Ring.closure s<GOAL>∃ L, (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1) ∧ (List.map List.prod L).sum = a
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>C : R → Prop<VAR>x : R<VAR>hx : x ∈ Ring.closure s<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<GOAL>C x
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>IsSubring (Ring.closure s)
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>a : R<GOAL>a ∈ s → a ∈ Ring.closure s
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<GOAL>s ⊆ Ring.closure s
<VAR>R : Type u<VAR>Ring R<VAR>s t : Set R<VAR>ht : IsSubring t<GOAL>s ⊆ t → Ring.closure s ⊆ t
<VAR>R : Type u<VAR>Ring R<VAR>s t : Set R<VAR>ht : IsSubring t<GOAL>Ring.closure s ⊆ t ↔ s ⊆ t
<VAR>R : Type u<VAR>Ring R<VAR>s t : Set R<VAR>H : s ⊆ t<GOAL>Ring.closure s ⊆ Ring.closure t
<VAR>R : Type u<VAR>Ring R<VAR>S : Type u_1<VAR>Ring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>⇑f '' Ring.closure s = Ring.closure (⇑f '' s)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.UniversallyClosed f<GOAL>(AlgebraicGeometry.topologically @IsClosedMap).universally f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.UniversallyClosed f ↔ (AlgebraicGeometry.topologically @IsClosedMap).universally f
<GOAL>@AlgebraicGeometry.UniversallyClosed = (AlgebraicGeometry.topologically @IsClosedMap).universally
<GOAL>CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyClosed
<GOAL>CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.UniversallyClosed
<VAR>X : AlgebraicGeometry.Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>U V : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>hV : AlgebraicGeometry.IsAffineOpen V<VAR>hxU : x ∈ U<VAR>hxV : x ∈ V<GOAL>hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>x : ↑↑X.toPresheafedSpace<VAR>hxU : x ∈ U<GOAL>hU.fromSpecStalk hxU = X.fromSpecStalk x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.val.base).obj ↑U), RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.LocallyOfFiniteType f<VAR>U : ↑Y.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ (TopologicalSpace.Opens.map f.val.base).obj ↑U<GOAL>RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.LocallyOfFiniteType (f ≫ g)<GOAL>AlgebraicGeometry.LocallyOfFiniteType f
<GOAL>CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.LocallyOfFiniteType
<GOAL>CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme = @AlgebraicGeometry.IsOpenImmersion ⊓ @AlgebraicGeometry.Surjective
<GOAL>CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme = (CategoryTheory.MorphismProperty.isomorphisms TopCat).inverseImage AlgebraicGeometry.Scheme.forgetToTop ⊓ AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.IsClosedImmersion f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.IsClosedImmersion f<GOAL>ClosedEmbedding ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.IsClosedImmersion f ↔ ClosedEmbedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsClosedImmersion f<GOAL>ClosedEmbedding ⇑f.val.base
<GOAL>@AlgebraicGeometry.IsClosedImmersion = (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => ClosedEmbedding) ⊓ AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.IsClosedImmersion f ↔ AlgebraicGeometry.IsPreimmersion f ∧ IsClosed (Set.range ⇑f.val.base)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsPreimmersion f<VAR>hf : IsClosed (Set.range ⇑f.val.base)<GOAL>AlgebraicGeometry.IsClosedImmersion f
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>h : Function.Surjective ⇑f<GOAL>AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map f)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>AlgebraicGeometry.IsAffine Y<VAR>f : X ⟶ Y<VAR>h : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Γ.map f.op)<GOAL>AlgebraicGeometry.IsClosedImmersion f
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.IsClosedImmersion g<VAR>AlgebraicGeometry.IsClosedImmersion (f ≫ g)<GOAL>AlgebraicGeometry.IsClosedImmersion f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.Surjective f<GOAL>Function.Surjective ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.Surjective f ↔ Function.Surjective ⇑f.val.base
<GOAL>@AlgebraicGeometry.Surjective = AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>AlgebraicGeometry.Surjective f<GOAL>Function.Surjective ⇑f.val.base
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.Surjective (f ≫ g)<GOAL>AlgebraicGeometry.Surjective g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.Surjective f<GOAL>AlgebraicGeometry.Surjective (f ≫ g) ↔ AlgebraicGeometry.Surjective g
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.IsSeparated f ↔ autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)) _auto✝
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.IsSeparated f<GOAL>AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
<GOAL>@AlgebraicGeometry.IsSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.IsClosedImmersion
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<VAR>self : IsAddSubgroup s<VAR>a : A<GOAL>a ∈ s → -a ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>self : IsSubgroup s<VAR>a : G<GOAL>a ∈ s → a⁻¹ ∈ s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<VAR>x y : G<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x - y ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>x y : G<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x / y ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>IsAddSubgroup s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>IsAddSubgroup s ↔ IsSubgroup s
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<VAR>hs : IsAddSubgroup s<GOAL>IsSubgroup s
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<GOAL>IsSubgroup s ↔ IsAddSubgroup s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>one_mem : 1 ∈ s<VAR>div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s<GOAL>IsSubgroup s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>one_mem : 0 ∈ s<VAR>div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a + -b ∈ s<GOAL>IsAddSubgroup s
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<VAR>zero_mem : 0 ∈ s<VAR>sub_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a - b ∈ s<GOAL>IsAddSubgroup s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s₁ s₂ : Set G<VAR>hs₁ : IsAddSubgroup s₁<VAR>hs₂ : IsAddSubgroup s₂<GOAL>IsAddSubgroup (s₁ ∩ s₂)
<VAR>G : Type u_1<VAR>Group G<VAR>s₁ s₂ : Set G<VAR>hs₁ : IsSubgroup s₁<VAR>hs₂ : IsSubgroup s₂<GOAL>IsSubgroup (s₁ ∩ s₂)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Sort u_4<VAR>s : ι → Set G<VAR>hs : ∀ (y : ι), IsSubgroup (s y)<GOAL>IsSubgroup (Set.iInter s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Sort u_4<VAR>s : ι → Set G<VAR>hs : ∀ (y : ι), IsAddSubgroup (s y)<GOAL>IsAddSubgroup (Set.iInter s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>s : ι → Set G<VAR>hs : ∀ (i : ι), IsAddSubgroup (s i)<VAR>directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k<GOAL>IsAddSubgroup (⋃ i, s i)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>s : ι → Set G<VAR>hs : ∀ (i : ι), IsSubgroup (s i)<VAR>directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k<GOAL>IsSubgroup (⋃ i, s i)
<VAR>G : Type u_1<VAR>a : G<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<GOAL>-a ∈ s ↔ a ∈ s
<VAR>G : Type u_1<VAR>a : G<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>a⁻¹ ∈ s ↔ a ∈ s
<VAR>G : Type u_1<VAR>a b : G<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>h : a ∈ s<GOAL>b * a ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>a b : G<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<VAR>h : a ∈ s<GOAL>b + a ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>a b : G<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>h : a ∈ s<GOAL>a * b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>a b : G<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<VAR>h : a ∈ s<GOAL>a + b ∈ s ↔ b ∈ s
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<VAR>self : IsNormalAddSubgroup s<VAR>n : A<GOAL>n ∈ s → ∀ (g : A), g + n + -g ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>self : IsNormalSubgroup s<VAR>n : G<GOAL>n ∈ s → ∀ (g : G), g * n * g⁻¹ ∈ s
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<GOAL>IsNormalAddSubgroup s
<VAR>G : Type u_1<VAR>CommGroup G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>IsNormalSubgroup s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsNormalSubgroup s<GOAL>IsNormalAddSubgroup s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>IsNormalAddSubgroup s ↔ IsNormalSubgroup s
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<VAR>hs : IsNormalAddSubgroup s<GOAL>IsNormalSubgroup s
<VAR>A : Type u_3<VAR>AddGroup A<VAR>s : Set A<GOAL>IsNormalSubgroup s ↔ IsNormalAddSubgroup s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsNormalAddSubgroup s<VAR>a b : G<VAR>hab : a + b ∈ s<GOAL>b + a ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsNormalSubgroup s<VAR>a b : G<VAR>hab : a * b ∈ s<GOAL>b * a ∈ s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsNormalSubgroup s<VAR>a b : G<GOAL>a * b ∈ s ↔ b * a ∈ s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsNormalAddSubgroup s<VAR>a b : G<GOAL>a + b ∈ s ↔ b + a ∈ s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>g : G<GOAL>g ∈ IsAddSubgroup.trivial G ↔ g = 0
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>g ∈ IsSubgroup.trivial G ↔ g = 1
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>IsNormalAddSubgroup (IsAddSubgroup.trivial G)
<VAR>G : Type u_1<VAR>Group G<GOAL>IsNormalSubgroup (IsSubgroup.trivial G)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<GOAL>s = IsAddSubgroup.trivial G ↔ ∀ x ∈ s, x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>s = IsSubgroup.trivial G ↔ ∀ x ∈ s, x = 1
<VAR>G : Type u_1<VAR>Group G<GOAL>IsNormalSubgroup Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>IsNormalAddSubgroup Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<GOAL>a ∈ IsSubgroup.center G ↔ ∀ (g : G), g * a = a * g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<GOAL>a ∈ IsAddSubgroup.addCenter G ↔ ∀ (g : G), g + a = a + g
<VAR>G : Type u_1<VAR>Group G<GOAL>IsNormalSubgroup (IsSubgroup.center G)
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>IsNormalAddSubgroup (IsAddSubgroup.addCenter G)
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>IsSubgroup (IsSubgroup.normalizer s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>IsAddSubgroup (IsAddSubgroup.addNormalizer s)
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>s ⊆ IsSubgroup.normalizer s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<GOAL>s ⊆ IsAddSubgroup.addNormalizer s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group H<VAR>f : G → H<VAR>x : G<GOAL>x ∈ IsGroupHom.ker f ↔ f x = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : G → H<VAR>x : G<GOAL>x ∈ IsAddGroupHom.ker f ↔ f x = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f (a * b⁻¹) = 1<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<VAR>h : f (a + -b) = 0<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f (a⁻¹ * b) = 1<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<VAR>h : f (-a + b) = 0<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<VAR>h : f a = f b<GOAL>f (a + -b) = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a = f b<GOAL>f (a * b⁻¹) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<VAR>h : f a = f b<GOAL>f (-a + b) = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a = f b<GOAL>f (a⁻¹ * b) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ f (a * b⁻¹) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ f (a + -b) = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ f (-a + b) = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ f (a⁻¹ * b) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ a * b⁻¹ ∈ IsGroupHom.ker f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ a + -b ∈ IsAddGroupHom.ker f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ a⁻¹ * b ∈ IsGroupHom.ker f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ -a + b ∈ IsAddGroupHom.ker f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>s : Set G<VAR>hs : IsAddSubgroup s<GOAL>IsAddSubgroup (f '' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>IsSubgroup (f '' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<GOAL>IsSubgroup (Set.range f)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<GOAL>IsAddSubgroup (Set.range f)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>s : Set H<VAR>hs : IsAddSubgroup s<GOAL>IsAddSubgroup (f ⁻¹' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsSubgroup s<GOAL>IsSubgroup (f ⁻¹' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsNormalSubgroup s<GOAL>IsNormalSubgroup (f ⁻¹' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>s : Set H<VAR>hs : IsNormalAddSubgroup s<GOAL>IsNormalAddSubgroup (f ⁻¹' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<GOAL>IsNormalAddSubgroup (IsAddGroupHom.ker f)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<GOAL>IsNormalSubgroup (IsGroupHom.ker f)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>h : IsAddGroupHom.ker f = IsAddSubgroup.trivial G<GOAL>Function.Injective f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>h : IsGroupHom.ker f = IsSubgroup.trivial G<GOAL>Function.Injective f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>h : Function.Injective f<GOAL>IsGroupHom.ker f = IsSubgroup.trivial G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>h : Function.Injective f<GOAL>IsAddGroupHom.ker f = IsAddSubgroup.trivial G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<GOAL>Function.Injective f ↔ IsAddGroupHom.ker f = IsAddSubgroup.trivial G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<GOAL>Function.Injective f ↔ IsGroupHom.ker f = IsSubgroup.trivial G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<GOAL>IsAddGroupHom.ker f = IsAddSubgroup.trivial G ↔ ∀ (x : G), f x = 0 → x = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<GOAL>IsGroupHom.ker f = IsSubgroup.trivial G ↔ ∀ (x : G), f x = 1 → x = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>a : G<GOAL>a ∈ s → a ∈ AddGroup.closure s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>a : G<GOAL>a ∈ s → a ∈ Group.closure s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>IsAddSubgroup (AddGroup.closure s)
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>IsSubgroup (Group.closure s)
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>s ⊆ Group.closure s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>s ⊆ AddGroup.closure s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s t : Set G<VAR>ht : IsAddSubgroup t<VAR>h : s ⊆ t<GOAL>AddGroup.closure s ⊆ t