ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Subtype.val ∘ ⇑f.rangeRestrict = ⇑f
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>f.range.subtype.comp f.rangeRestrict = f
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>f.range.subtype.comp f.rangeRestrict = f
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Function.Surjective ⇑f.rangeRestrict
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>Function.Surjective ⇑f.rangeRestrict
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Group N<VAR>Group P<VAR>g : N →* P<VAR>f : G →* N<GOAL>Subgroup.map g f.range = (g.comp f).range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddGroup N<VAR>AddGroup P<VAR>g : N →+ P<VAR>f : G →+ N<GOAL>AddSubgroup.map g f.range = (g.comp f).range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_7<VAR>AddGroup N<VAR>f : G →+ N<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_7<VAR>Group N<VAR>f : G →* N<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_7<VAR>Group N<VAR>f : G →* N<VAR>hf : Function.Surjective ⇑f<GOAL>f.range = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_7<VAR>AddGroup N<VAR>f : G →+ N<VAR>hf : Function.Surjective ⇑f<GOAL>f.range = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<GOAL>MonoidHom.range 1 = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<GOAL>AddMonoidHom.range 0 = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.subtype.range = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.subtype.range = H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h_le : H ≤ K<GOAL>(Subgroup.inclusion h_le).range = H.subgroupOf K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h_le : H ≤ K<GOAL>(AddSubgroup.inclusion h_le).range = H.addSubgroupOf K
<VAR>G₁ : Type u_7<VAR>G₂ : Type u_8<VAR>AddGroup G₁<VAR>AddGroup G₂<VAR>K : AddSubgroup G₂<VAR>f : G₁ →+ G₂<VAR>h : f.range ≤ K<GOAL>f.range.addSubgroupOf K = (f.codRestrict K ⋯).range
<VAR>G₁ : Type u_7<VAR>G₂ : Type u_8<VAR>Group G₁<VAR>Group G₂<VAR>K : Subgroup G₂<VAR>f : G₁ →* G₂<VAR>h : f.range ≤ K<GOAL>f.range.subgroupOf K = (f.codRestrict K ⋯).range
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<GOAL>(MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range
<VAR>A : Type u_7<VAR>A' : Type u_8<VAR>AddGroup A<VAR>AddGroup A'<VAR>f : A →+ A'<GOAL>(AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>g : N →+ G<VAR>h : Function.LeftInverse ⇑g ⇑f<VAR>x : G<GOAL>↑((AddMonoidHom.ofLeftInverse h) x) = f x
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>g : N →* G<VAR>h : Function.LeftInverse ⇑g ⇑f<VAR>x : G<GOAL>↑((MonoidHom.ofLeftInverse h) x) = f x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>g : N →+ G<VAR>h : Function.LeftInverse ⇑g ⇑f<VAR>x : ↥f.range<GOAL>(AddMonoidHom.ofLeftInverse h).symm x = g ↑x
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>g : N →* G<VAR>h : Function.LeftInverse ⇑g ⇑f<VAR>x : ↥f.range<GOAL>(MonoidHom.ofLeftInverse h).symm x = g ↑x
<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>x : G<GOAL>↑((MonoidHom.ofInjective hf) x) = f x
<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>x : G<GOAL>↑((AddMonoidHom.ofInjective hf) x) = f x
<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>x : ↥f.range<GOAL>f ((MonoidHom.ofInjective hf).symm x) = ↑x
<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>x : ↥f.range<GOAL>f ((AddMonoidHom.ofInjective hf).symm x) = ↑x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddZeroClass M<VAR>f : G →+ M<VAR>x : G<GOAL>x ∈ f.ker ↔ f x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>MulOneClass M<VAR>f : G →* M<VAR>x : G<GOAL>x ∈ f.ker ↔ f x = 1
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>MulOneClass M<VAR>f : G →* M<GOAL>↑f.ker = ⇑f ⁻¹' {1}
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddZeroClass M<VAR>f : G →+ M<GOAL>↑f.ker = ⇑f ⁻¹' {0}
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_8<VAR>Monoid M<VAR>f : G →* M<GOAL>f.toHomUnits.ker = f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_8<VAR>AddMonoid M<VAR>f : G →+ M<GOAL>f.toHomAddUnits.ker = f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddZeroClass M<VAR>f : G →+ M<VAR>x y : G<GOAL>f x = f y ↔ -y + x ∈ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>MulOneClass M<VAR>f : G →* M<VAR>x y : G<GOAL>f x = f y ↔ y⁻¹ * x ∈ f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddGroup N<VAR>AddGroup P<VAR>g : N →+ P<VAR>f : G →+ N<GOAL>AddSubgroup.comap f g.ker = (g.comp f).ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Group N<VAR>Group P<VAR>g : N →* P<VAR>f : G →* N<GOAL>Subgroup.comap f g.ker = (g.comp f).ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>AddSubgroup.comap f ⊥ = f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Subgroup.comap f ⊥ = f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>K : AddSubgroup G<VAR>f : G →+ N<GOAL>(f.restrict K).ker = f.ker.addSubgroupOf K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>K : Subgroup G<VAR>f : G →* N<GOAL>(f.restrict K).ker = f.ker.subgroupOf K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>S : Type u_8<VAR>SetLike S N<VAR>SubmonoidClass S N<VAR>f : G →* N<VAR>s : S<VAR>h : ∀ (x : G), f x ∈ s<GOAL>(f.codRestrict s h).ker = f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>S : Type u_8<VAR>SetLike S N<VAR>AddSubmonoidClass S N<VAR>f : G →+ N<VAR>s : S<VAR>h : ∀ (x : G), f x ∈ s<GOAL>(f.codRestrict s h).ker = f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>f.rangeRestrict.ker = f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>f.rangeRestrict.ker = f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>MulOneClass M<GOAL>MonoidHom.ker 1 = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddZeroClass M<GOAL>AddMonoidHom.ker 0 = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>(AddMonoidHom.id G).ker = ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>(MonoidHom.id G).ker = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>MulOneClass M<VAR>f : G →* M<GOAL>f.ker = ⊥ ↔ Function.Injective ⇑f
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddZeroClass M<VAR>f : G →+ M<GOAL>f.ker = ⊥ ↔ Function.Injective ⇑f
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.subtype.ker = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.subtype.ker = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<GOAL>(AddSubgroup.inclusion h).ker = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<GOAL>(Subgroup.inclusion h).ker = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_8<VAR>N : Type u_9<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : G →+ M<VAR>g : G →+ N<GOAL>(f.prod g).ker = f.ker ⊓ g.ker
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_8<VAR>N : Type u_9<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : G →* M<VAR>g : G →* N<GOAL>(f.prod g).ker = f.ker ⊓ g.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>G' : Type u_8<VAR>N' : Type u_9<VAR>Group G'<VAR>Group N'<VAR>f : G →* N<VAR>g : G' →* N'<VAR>S : Subgroup N<VAR>S' : Subgroup N'<GOAL>Subgroup.comap (f.prodMap g) (S.prod S') = (Subgroup.comap f S).prod (Subgroup.comap g S')
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>G' : Type u_8<VAR>N' : Type u_9<VAR>AddGroup G'<VAR>AddGroup N'<VAR>f : G →+ N<VAR>g : G' →+ N'<VAR>S : AddSubgroup N<VAR>S' : AddSubgroup N'<GOAL>AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>G' : Type u_8<VAR>N' : Type u_9<VAR>Group G'<VAR>Group N'<VAR>f : G →* N<VAR>g : G' →* N'<GOAL>(f.prodMap g).ker = f.ker.prod g.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>G' : Type u_8<VAR>N' : Type u_9<VAR>AddGroup G'<VAR>AddGroup N'<VAR>f : G →+ N<VAR>g : G' →+ N'<GOAL>(f.prodMap g).ker = f.ker.prod g.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>AddGroup G<VAR>AddGroup G'<VAR>AddGroup G''<VAR>f : G →+ G'<VAR>g : G' →+ G''<GOAL>f.range ≤ g.ker ↔ g.comp f = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>Group G<VAR>Group G'<VAR>Group G''<VAR>f : G →* G'<VAR>g : G' →* G''<GOAL>f.range ≤ g.ker ↔ g.comp f = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<GOAL>(AddMonoidHom.fst G G').ker = ⊥.prod ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<GOAL>(MonoidHom.fst G G').ker = ⊥.prod ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<GOAL>(AddMonoidHom.snd G G').ker = ⊤.prod ⊥
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<GOAL>(MonoidHom.snd G G').ker = ⊤.prod ⊥
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<GOAL>(MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker
<VAR>A : Type u_8<VAR>A' : Type u_9<VAR>AddGroup A<VAR>AddGroup A'<VAR>f : A →+ A'<GOAL>(AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>f.eqLocus f = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>f.eqLocus f = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddMonoid M<VAR>f g : G →+ M<VAR>s : Set G<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(AddSubgroup.closure s)
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>Monoid M<VAR>f g : G →* M<VAR>s : Set G<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddMonoid M<VAR>f g : G →+ M<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>Monoid M<VAR>f g : G →* M<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>G : Type u_1<VAR>Group G<VAR>M : Type u_7<VAR>Monoid M<VAR>s : Set G<VAR>hs : Subgroup.closure s = ⊤<VAR>f g : G →* M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>M : Type u_7<VAR>AddMonoid M<VAR>s : Set G<VAR>hs : AddSubgroup.closure s = ⊤<VAR>f g : G →+ M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>s : Set N<GOAL>AddSubgroup.closure (⇑f ⁻¹' s) ≤ AddSubgroup.comap f (AddSubgroup.closure s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>s : Set N<GOAL>Subgroup.closure (⇑f ⁻¹' s) ≤ Subgroup.comap f (Subgroup.closure s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>s : Set G<GOAL>AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>s : Set G<GOAL>Subgroup.map f (Subgroup.closure s) = Subgroup.closure (⇑f '' s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>h : H.Normal<VAR>f : G →* N<VAR>hf : Function.Surjective ⇑f<GOAL>(Subgroup.map f H).Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>h : H.Normal<VAR>f : G →+ N<VAR>hf : Function.Surjective ⇑f<GOAL>(AddSubgroup.map f H).Normal
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>f : G →* N<GOAL>Subgroup.map f H = ⊥ ↔ H ≤ f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : G →+ N<GOAL>AddSubgroup.map f H = ⊥ ↔ H ≤ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>f : G →* N<VAR>hf : Function.Injective ⇑f<GOAL>Subgroup.map f H = ⊥ ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : G →+ N<VAR>hf : Function.Injective ⇑f<GOAL>AddSubgroup.map f H = ⊥ ↔ H = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup G<GOAL>AddSubgroup.map f H ≤ f.range
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup G<GOAL>Subgroup.map f H ≤ f.range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>K : AddSubgroup ↥H<GOAL>AddSubgroup.map H.subtype K ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>K : Subgroup ↥H<GOAL>Subgroup.map H.subtype K ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup N<GOAL>f.ker ≤ Subgroup.comap f H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup N<GOAL>f.ker ≤ AddSubgroup.comap f H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup N<GOAL>Subgroup.map f (Subgroup.comap f H) ≤ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup N<GOAL>AddSubgroup.map f (AddSubgroup.comap f H) ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup G<GOAL>H ≤ Subgroup.comap f (Subgroup.map f H)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup G<GOAL>H ≤ AddSubgroup.comap f (AddSubgroup.map f H)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup N<GOAL>AddSubgroup.map f (AddSubgroup.comap f H) = f.range ⊓ H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup N<GOAL>Subgroup.map f (Subgroup.comap f H) = f.range ⊓ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup G<GOAL>AddSubgroup.comap f (AddSubgroup.map f H) = H ⊔ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup G<GOAL>Subgroup.comap f (Subgroup.map f H) = H ⊔ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup N<VAR>h : H ≤ f.range<GOAL>Subgroup.map f (Subgroup.comap f H) = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup N<VAR>h : H ≤ f.range<GOAL>AddSubgroup.map f (AddSubgroup.comap f H) = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>h : Function.Surjective ⇑f<VAR>H : AddSubgroup N<GOAL>AddSubgroup.map f (AddSubgroup.comap f H) = H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>h : Function.Surjective ⇑f<VAR>H : Subgroup N<GOAL>Subgroup.map f (Subgroup.comap f H) = H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K L : Subgroup N<VAR>hf : K ≤ f.range<GOAL>Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K L : AddSubgroup N<VAR>hf : K ≤ f.range<GOAL>AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K L : Subgroup N<VAR>hf : Function.Surjective ⇑f<GOAL>Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K L : AddSubgroup N<VAR>hf : Function.Surjective ⇑f<GOAL>AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K L : AddSubgroup N<VAR>hf : Function.Surjective ⇑f<GOAL>AddSubgroup.comap f K < AddSubgroup.comap f L ↔ K < L
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>K L : Subgroup N<VAR>hf : Function.Surjective ⇑f<GOAL>Subgroup.comap f K < Subgroup.comap f L ↔ K < L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>h : Function.Surjective ⇑f<GOAL>Function.Injective (AddSubgroup.comap f)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>h : Function.Surjective ⇑f<GOAL>Function.Injective (Subgroup.comap f)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup G<VAR>h : f.ker ≤ H<GOAL>Subgroup.comap f (Subgroup.map f H) = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup G<VAR>h : f.ker ≤ H<GOAL>AddSubgroup.comap f (AddSubgroup.map f H) = H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>h : Function.Injective ⇑f<VAR>H : Subgroup G<GOAL>Subgroup.comap f (Subgroup.map f H) = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>h : Function.Injective ⇑f<VAR>H : AddSubgroup G<GOAL>AddSubgroup.comap f (AddSubgroup.map f H) = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H K : AddSubgroup G<GOAL>AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K ⊔ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H K : Subgroup G<GOAL>Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K ⊔ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H K : Subgroup G<GOAL>Subgroup.map f H ≤ Subgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H K : AddSubgroup G<GOAL>AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H K : Subgroup G<GOAL>Subgroup.map f H = Subgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H K : AddSubgroup G<GOAL>AddSubgroup.map f H = AddSubgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H : Subgroup G<GOAL>Subgroup.map f H = f.range ↔ Codisjoint H f.ker
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H : AddSubgroup G<GOAL>AddSubgroup.map f H = f.range ↔ Codisjoint H f.ker
<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>H K : AddSubgroup G<GOAL>AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ 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>H K : Subgroup G<GOAL>Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>G' : AddSubgroup G<VAR>H K : AddSubgroup ↥G'<GOAL>AddSubgroup.map G'.subtype H ≤ AddSubgroup.map G'.subtype K ↔ H ≤ K
<VAR>G : Type u_1<VAR>Group G<VAR>G' : Subgroup G<VAR>H K : Subgroup ↥G'<GOAL>Subgroup.map G'.subtype H ≤ Subgroup.map G'.subtype K ↔ H ≤ K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>h : Function.Injective ⇑f<GOAL>Function.Injective (Subgroup.map f)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>h : Function.Injective ⇑f<GOAL>Function.Injective (AddSubgroup.map f)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>g : N →+ G<VAR>hl : Function.LeftInverse ⇑g ⇑f<VAR>hr : Function.RightInverse ⇑g ⇑f<VAR>H : AddSubgroup G<GOAL>AddSubgroup.map f H = AddSubgroup.comap g H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>g : N →* G<VAR>hl : Function.LeftInverse ⇑g ⇑f<VAR>hr : Function.RightInverse ⇑g ⇑f<VAR>H : Subgroup G<GOAL>Subgroup.map f H = Subgroup.comap g H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H K : AddSubgroup G<VAR>hH : f.ker ≤ H<VAR>hK : f.ker ≤ K<VAR>hf : AddSubgroup.map f H = AddSubgroup.map f K<GOAL>H = K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H K : Subgroup G<VAR>hH : f.ker ≤ H<VAR>hK : f.ker ≤ K<VAR>hf : Subgroup.map f H = Subgroup.map f K<GOAL>H = K
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.closure (⇑(Subgroup.closure s).subtype ⁻¹' s) = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>AddSubgroup.closure (⇑(AddSubgroup.closure s).subtype ⁻¹' s) = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H K : Subgroup N<VAR>hH : H ≤ f.range<VAR>hK : K ≤ f.range<GOAL>Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.comap f (H ⊔ K)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H K : AddSubgroup N<VAR>hH : H ≤ f.range<VAR>hK : K ≤ f.range<GOAL>AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>H K : AddSubgroup N<VAR>hf : Function.Surjective ⇑f<GOAL>AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>H K : Subgroup N<VAR>hf : Function.Surjective ⇑f<GOAL>Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.comap f (H ⊔ K)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hH : H ≤ L<VAR>hK : K ≤ L<GOAL>H.addSubgroupOf L ⊔ K.addSubgroupOf L = (H ⊔ K).addSubgroupOf L
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hH : H ≤ L<VAR>hK : K ≤ L<GOAL>H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>Codisjoint (H.addSubgroupOf (H ⊔ K)) (K.addSubgroupOf (H ⊔ K))
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>f : G →* N<VAR>hf : Function.Injective ⇑f<VAR>h : ↥H<GOAL>↑((H.equivMapOfInjective f hf) h) = f ↑h
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : G →+ N<VAR>hf : Function.Injective ⇑f<VAR>h : ↥H<GOAL>↑((H.equivMapOfInjective f hf) h) = f ↑h
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : N →+ G<VAR>hf : Function.Surjective ⇑f<GOAL>AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Function.Surjective ⇑f<GOAL>Subgroup.comap f H.normalizer = (Subgroup.comap f H).normalizer
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_6<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : N →+ G<VAR>hf : Function.Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_6<VAR>Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Function.Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>Subgroup.comap f H.normalizer = (Subgroup.comap f H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>H N : Subgroup G<VAR>h : H.normalizer ≤ N<GOAL>H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H N : AddSubgroup G<VAR>h : H.normalizer ≤ N<GOAL>H.normalizer.addSubgroupOf N = (H.addSubgroupOf N).normalizer
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : G ≃+ N<GOAL>AddSubgroup.map f.toAddMonoidHom H.normalizer = (AddSubgroup.map f.toAddMonoidHom H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>f : G ≃* N<GOAL>Subgroup.map f.toMonoidHom H.normalizer = (Subgroup.map f.toMonoidHom H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>f : G →* N<VAR>hf : Function.Bijective ⇑f<GOAL>Subgroup.map f H.normalizer = (Subgroup.map f H).normalizer