ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : N ≃+ G<VAR>K : AddSubgroup G<GOAL>AddSubgroup.comap (↑f) K = AddSubgroup.map (↑f.symm) K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : N ≃+ G<VAR>K : AddSubgroup G<GOAL>AddSubgroup.comap f.toAddMonoidHom K = AddSubgroup.map f.symm.toAddMonoidHom K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : N ≃* G<VAR>K : Subgroup G<GOAL>Subgroup.comap f.toMonoidHom K = Subgroup.map f.symm.toMonoidHom K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup N<VAR>e : G ≃+ N<GOAL>AddSubgroup.map (↑e.symm) H = K ↔ AddSubgroup.map (↑e) K = H
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup N<VAR>e : G ≃* N<GOAL>Subgroup.map (↑e.symm) H = K ↔ Subgroup.map (↑e) K = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>K : AddSubgroup G<VAR>H : AddSubgroup N<GOAL>AddSubgroup.map f K ≤ H ↔ K ≤ 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>K : Subgroup G<VAR>H : Subgroup N<GOAL>Subgroup.map f K ≤ H ↔ K ≤ Subgroup.comap f H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>GaloisConnection (Subgroup.map f) (Subgroup.comap f)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H K : AddSubgroup G<VAR>f : G →+ N<GOAL>AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H K : Subgroup G<VAR>f : G →* N<GOAL>Subgroup.map f (H ⊔ K) = Subgroup.map f H ⊔ Subgroup.map f K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>ι : Sort u_7<VAR>f : G →+ N<VAR>s : ι → AddSubgroup G<GOAL>AddSubgroup.map f (iSup s) = ⨆ i, AddSubgroup.map f (s i)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>ι : Sort u_7<VAR>f : G →* N<VAR>s : ι → Subgroup G<GOAL>Subgroup.map f (iSup s) = ⨆ i, Subgroup.map f (s i)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H K : AddSubgroup N<VAR>f : G →+ N<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>H K : Subgroup N<VAR>f : G →* N<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>ι : Sort u_7<VAR>f : G →+ N<VAR>s : ι → AddSubgroup N<GOAL>⨆ i, AddSubgroup.comap f (s i) ≤ AddSubgroup.comap f (iSup s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>ι : Sort u_7<VAR>f : G →* N<VAR>s : ι → Subgroup N<GOAL>⨆ i, Subgroup.comap f (s i) ≤ Subgroup.comap f (iSup s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H K : Subgroup N<VAR>f : G →* N<GOAL>Subgroup.comap f (H ⊓ K) = Subgroup.comap f H ⊓ Subgroup.comap f K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H K : AddSubgroup N<VAR>f : G →+ N<GOAL>AddSubgroup.comap f (H ⊓ K) = AddSubgroup.comap f H ⊓ AddSubgroup.comap f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>ι : Sort u_7<VAR>f : G →* N<VAR>s : ι → Subgroup N<GOAL>Subgroup.comap f (iInf s) = ⨅ i, Subgroup.comap f (s i)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>ι : Sort u_7<VAR>f : G →+ N<VAR>s : ι → AddSubgroup N<GOAL>AddSubgroup.comap f (iInf s) = ⨅ i, AddSubgroup.comap f (s i)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H K : Subgroup G<VAR>f : G →* N<GOAL>Subgroup.map f (H ⊓ K) ≤ Subgroup.map f H ⊓ Subgroup.map f K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H K : AddSubgroup G<VAR>f : G →+ N<GOAL>AddSubgroup.map f (H ⊓ K) ≤ AddSubgroup.map f H ⊓ AddSubgroup.map f K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H K : AddSubgroup G<VAR>f : G →+ N<VAR>hf : Function.Injective ⇑f<GOAL>AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H K : Subgroup G<VAR>f : G →* N<VAR>hf : Function.Injective ⇑f<GOAL>Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Subgroup.map f ⊥ = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>AddSubgroup.map 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>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.Surjective ⇑f<GOAL>AddSubgroup.map f ⊤ = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>AddSubgroup.comap f ⊤ = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Subgroup.comap f ⊤ = ⊤
<VAR>G : Type u_7<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<VAR>g : ↥H<GOAL>↑↑((Subgroup.subgroupOfEquivOfLe h).symm g) = ↑g
<VAR>G : Type u_7<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<VAR>g : ↥(H.subgroupOf K)<GOAL>↑((Subgroup.subgroupOfEquivOfLe h) g) = ↑↑g
<VAR>G : Type u_7<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<VAR>g : ↥H<GOAL>↑↑((AddSubgroup.addSubgroupOfEquivOfLe h).symm g) = ↑g
<VAR>G : Type u_7<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<VAR>g : ↥(H.addSubgroupOf K)<GOAL>↑((AddSubgroup.addSubgroupOfEquivOfLe h) g) = ↑↑g
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>Subgroup.comap K.subtype H = H.subgroupOf K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>AddSubgroup.comap K.subtype H = H.addSubgroupOf K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K₁ K₂ : AddSubgroup G<VAR>h : K₁ ≤ K₂<VAR>H : AddSubgroup G<GOAL>AddSubgroup.comap (AddSubgroup.inclusion h) (H.addSubgroupOf K₂) = H.addSubgroupOf K₁
<VAR>G : Type u_1<VAR>Group G<VAR>K₁ K₂ : Subgroup G<VAR>h : K₁ ≤ K₂<VAR>H : Subgroup G<GOAL>Subgroup.comap (Subgroup.inclusion h) (H.subgroupOf K₂) = H.subgroupOf K₁
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>↑(H.subgroupOf K) = ⇑K.subtype ⁻¹' ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>↑(H.addSubgroupOf K) = ⇑K.subtype ⁻¹' ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : ↥K<GOAL>h ∈ H.subgroupOf K ↔ ↑h ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : ↥K<GOAL>h ∈ H.addSubgroupOf K ↔ ↑h ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>AddSubgroup.map K.subtype (H.addSubgroupOf K) = H ⊓ K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>Subgroup.map K.subtype (H.subgroupOf K) = H ⊓ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⊥.addSubgroupOf H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⊥.subgroupOf H = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⊤.subgroupOf H = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⊤.addSubgroupOf H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.subgroupOf ⊥ = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.addSubgroupOf ⊥ = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.addSubgroupOf ⊥ = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.subgroupOf ⊥ = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.addSubgroupOf H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.subgroupOf H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ K : Subgroup G<GOAL>H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H₁ H₂ K : AddSubgroup G<GOAL>H₁.addSubgroupOf K = H₂.addSubgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>(H ⊓ K).addSubgroupOf K = H.addSubgroupOf K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>(H ⊓ K).subgroupOf K = H.subgroupOf K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>(K ⊓ H).addSubgroupOf K = H.addSubgroupOf K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>(K ⊓ H).subgroupOf K = H.subgroupOf K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>H.subgroupOf K = ⊥ ↔ Disjoint H K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H.addSubgroupOf K = ⊥ ↔ Disjoint H K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>H.addSubgroupOf K = ⊤ ↔ K ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>H.subgroupOf K = ⊤ ↔ K ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>K : Subgroup N<GOAL>↑(H.prod K) = ↑H ×ˢ ↑K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>K : AddSubgroup N<GOAL>↑(H.prod K) = ↑H ×ˢ ↑K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>K : AddSubgroup N<VAR>p : G × N<GOAL>p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>K : Subgroup N<VAR>p : G × N<GOAL>p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<GOAL>((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) AddSubgroup.prod AddSubgroup.prod
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<GOAL>((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) Subgroup.prod Subgroup.prod
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>K : Subgroup G<GOAL>Monotone fun t => K.prod t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>K : AddSubgroup G<GOAL>Monotone fun t => K.prod t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup N<GOAL>Monotone fun K => K.prod H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup N<GOAL>Monotone fun K => K.prod H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>K : AddSubgroup G<GOAL>K.prod ⊤ = AddSubgroup.comap (AddMonoidHom.fst G N) K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>K : Subgroup G<GOAL>K.prod ⊤ = Subgroup.comap (MonoidHom.fst G N) K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup N<GOAL>⊤.prod H = AddSubgroup.comap (AddMonoidHom.snd G N) H
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup N<GOAL>⊤.prod H = Subgroup.comap (MonoidHom.snd G N) H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<GOAL>⊤.prod ⊤ = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<GOAL>⊤.prod ⊤ = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<GOAL>⊥.prod ⊥ = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<GOAL>⊥.prod ⊥ = ⊥
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>K : AddSubgroup N<VAR>J : AddSubgroup (G × N)<GOAL>J ≤ H.prod K ↔ AddSubgroup.map (AddMonoidHom.fst G N) J ≤ H ∧ AddSubgroup.map (AddMonoidHom.snd G N) J ≤ K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>K : Subgroup N<VAR>J : Subgroup (G × N)<GOAL>J ≤ H.prod K ↔ Subgroup.map (MonoidHom.fst G N) J ≤ H ∧ Subgroup.map (MonoidHom.snd G N) J ≤ K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>K : Subgroup N<VAR>J : Subgroup (G × N)<GOAL>H.prod K ≤ J ↔ Subgroup.map (MonoidHom.inl G N) H ≤ J ∧ Subgroup.map (MonoidHom.inr G N) K ≤ J
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>K : AddSubgroup N<VAR>J : AddSubgroup (G × N)<GOAL>H.prod K ≤ J ↔ AddSubgroup.map (AddMonoidHom.inl G N) H ≤ J ∧ AddSubgroup.map (AddMonoidHom.inr G N) K ≤ J
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>K : AddSubgroup N<GOAL>H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup G<VAR>K : Subgroup N<GOAL>H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>I : Set η<VAR>H : (i : η) → Subgroup (f i)<GOAL>↑(Subgroup.pi I H) = I.pi fun i => ↑(H i)
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>I : Set η<VAR>H : (i : η) → AddSubgroup (f i)<GOAL>↑(AddSubgroup.pi I H) = I.pi fun i => ↑(H i)
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>I : Set η<VAR>H : (i : η) → Subgroup (f i)<VAR>p : (i : η) → f i<GOAL>p ∈ Subgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>I : Set η<VAR>H : (i : η) → AddSubgroup (f i)<VAR>p : (i : η) → f i<GOAL>p ∈ AddSubgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>I : Set η<GOAL>(AddSubgroup.pi I fun i => ⊤) = ⊤
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>I : Set η<GOAL>(Subgroup.pi I fun i => ⊤) = ⊤
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>H : (i : η) → Subgroup (f i)<GOAL>Subgroup.pi ∅ H = ⊤
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>H : (i : η) → AddSubgroup (f i)<GOAL>AddSubgroup.pi ∅ H = ⊤
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<GOAL>(Subgroup.pi Set.univ fun i => ⊥) = ⊥
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<GOAL>(AddSubgroup.pi Set.univ fun i => ⊥) = ⊥
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>I : Set η<VAR>H : (i : η) → AddSubgroup (f i)<VAR>J : AddSubgroup ((i : η) → f i)<GOAL>J ≤ AddSubgroup.pi I H ↔ ∀ i ∈ I, AddSubgroup.map (Pi.evalAddMonoidHom f i) J ≤ H i
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>I : Set η<VAR>H : (i : η) → Subgroup (f i)<VAR>J : Subgroup ((i : η) → f i)<GOAL>J ≤ Subgroup.pi I H ↔ ∀ i ∈ I, Subgroup.map (Pi.evalMonoidHom f i) J ≤ H i
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>DecidableEq η<VAR>I : Set η<VAR>H : (i : η) → Subgroup (f i)<VAR>i : η<VAR>x : f i<GOAL>Pi.mulSingle i x ∈ Subgroup.pi I H ↔ i ∈ I → x ∈ H i
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>DecidableEq η<VAR>I : Set η<VAR>H : (i : η) → AddSubgroup (f i)<VAR>i : η<VAR>x : f i<GOAL>Pi.single i x ∈ AddSubgroup.pi I H ↔ i ∈ I → x ∈ H i
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → AddGroup (f i)<VAR>H : (i : η) → AddSubgroup (f i)<GOAL>AddSubgroup.pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>(i : η) → Group (f i)<VAR>H : (i : η) → Subgroup (f i)<GOAL>Subgroup.pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>self : H.Normal<VAR>n : G<GOAL>n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H
<VAR>A : Type u_4<VAR>AddGroup A<VAR>H : AddSubgroup A<VAR>self : H.Normal<VAR>n : A<GOAL>n ∈ H → ∀ (g : A), g + n + -g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>nH : H.Normal<VAR>n : G<VAR>hn : n ∈ H<VAR>g : G<GOAL>g⁻¹ * n * g ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>nH : H.Normal<VAR>n : G<VAR>hn : n ∈ H<VAR>g : G<GOAL>-g + n + g ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>nH : H.Normal<VAR>a b : G<VAR>h : a + b ∈ H<GOAL>b + a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>nH : H.Normal<VAR>a b : G<VAR>h : a * b ∈ H<GOAL>b * a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>nH : H.Normal<VAR>a b : G<GOAL>a * b ∈ H ↔ b * a ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>nH : H.Normal<VAR>a b : G<GOAL>a + b ∈ H ↔ b + a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>self : H.Characteristic<VAR>ϕ : G ≃* G<GOAL>Subgroup.comap ϕ.toMonoidHom H = H
<VAR>A : Type u_4<VAR>AddGroup A<VAR>H : AddSubgroup A<VAR>self : H.Characteristic<VAR>ϕ : A ≃+ A<GOAL>AddSubgroup.comap ϕ.toAddMonoidHom H = H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H = H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H ≤ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H ≤ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.comap ϕ.toAddMonoidHom H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.comap ϕ.toMonoidHom H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H = H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H ≤ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.map ϕ.toAddMonoidHom H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.map ϕ.toMonoidHom H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g * h * g⁻¹ ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g + h + -g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ -g + h + g ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (n : G), n + g ∈ H ↔ g + n ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<GOAL>g ∈ H.normalizer ↔ ∀ (n : G), n * g ∈ H ↔ g * n ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H ≤ H.normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H ≤ H.normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.normalizer = ⊤ ↔ H.Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.normalizer = ⊤ ↔ H.Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>hK : (H.addSubgroupOf K).Normal<VAR>HK : H ≤ K<GOAL>K ≤ H.normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hK : (H.subgroupOf K).Normal<VAR>HK : H ≤ K<GOAL>K ≤ H.normalizer
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : N →+ G<GOAL>AddSubgroup.comap f H.normalizer ≤ (AddSubgroup.comap f H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>N : Type u_5<VAR>Group N<VAR>f : N →* G<GOAL>Subgroup.comap f H.normalizer ≤ (Subgroup.comap f H).normalizer
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>Subgroup.map f H.normalizer ≤ (Subgroup.map f H).normalizer
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>AddSubgroup.map f H.normalizer ≤ (AddSubgroup.map f H).normalizer
<VAR>G : Type u_1<VAR>Group G<GOAL>NormalizerCondition G ↔ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>self : H.IsCommutative<GOAL>Std.Commutative fun x x_1 => x * x_1
<VAR>A : Type u_4<VAR>AddGroup A<VAR>H : AddSubgroup A<VAR>self : H.IsCommutative<GOAL>Std.Commutative fun x x_1 => x + x_1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G' →+ G<VAR>hf : Function.Injective ⇑f<VAR>H.IsCommutative<GOAL>(AddSubgroup.comap f H).IsCommutative
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G' →* G<VAR>hf : Function.Injective ⇑f<VAR>H.IsCommutative<GOAL>(Subgroup.comap f H).IsCommutative
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_5<VAR>Group H<VAR>f : G ≃* H<GOAL>∀ (H_1 : Subgroup G), (RelIso.symm f.comapSubgroup) H_1 = Subgroup.comap (↑f.symm) H_1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_5<VAR>Group H<VAR>f : G ≃* H<GOAL>∀ (H_1 : Subgroup H), f.comapSubgroup H_1 = Subgroup.comap (↑f) H_1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_6<VAR>Group H<VAR>f : G ≃* H<GOAL>∀ (H_1 : Subgroup G), f.mapSubgroup H_1 = Subgroup.map (↑f) H_1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_6<VAR>Group H<VAR>f : G ≃* H<GOAL>∀ (H_1 : Subgroup H), (RelIso.symm f.mapSubgroup) H_1 = Subgroup.map (↑f.symm) H_1
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>x : G<GOAL>x ∈ Group.conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>s ⊆ Group.conjugatesOfSet s
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>h : s ⊆ t<GOAL>Group.conjugatesOfSet s ⊆ Group.conjugatesOfSet t
<VAR>G : Type u_1<VAR>Group G<VAR>N : Subgroup G<VAR>tn : N.Normal<VAR>a : G<VAR>h : a ∈ N<GOAL>conjugatesOf a ⊆ ↑N
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h : s ⊆ ↑N<GOAL>Group.conjugatesOfSet s ⊆ ↑N
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>x c : G<GOAL>x ∈ Group.conjugatesOfSet s → c * x * c⁻¹ ∈ Group.conjugatesOfSet s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Group.conjugatesOfSet s ⊆ ↑(Subgroup.normalClosure s)
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>s ⊆ ↑(Subgroup.normalClosure s)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H ≤ Subgroup.normalClosure ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h : s ⊆ ↑N<GOAL>Subgroup.normalClosure s ≤ N
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>N : Subgroup G<VAR>N.Normal<GOAL>s ⊆ ↑N ↔ Subgroup.normalClosure s ≤ N
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>h : s ⊆ t<GOAL>Subgroup.normalClosure s ≤ Subgroup.normalClosure t
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.normalClosure s = ⨅ N, ⨅ (_ : N.Normal), ⨅ (_ : s ⊆ ↑N), N
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<GOAL>Subgroup.normalClosure ↑H = H
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.normalClosure ↑(Subgroup.normalClosure s) = Subgroup.normalClosure s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.closure s ≤ Subgroup.normalClosure s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Subgroup.normalClosure ↑(Subgroup.closure s) = Subgroup.normalClosure s
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.normalCore ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>H N : Subgroup G<VAR>hN : N.Normal<GOAL>N ≤ H.normalCore ↔ N ≤ H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<GOAL>H.normalCore ≤ K.normalCore
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.normalCore = ⨆ N, ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<GOAL>H.normalCore = H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.normalCore.normalCore = H.normalCore
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>↑f.range = Set.range ⇑f
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>↑f.range = Set.range ⇑f
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>y : N<GOAL>y ∈ f.range ↔ ∃ x, f x = y
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>y : N<GOAL>y ∈ f.range ↔ ∃ x, f x = y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>f.range = AddSubgroup.map f ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<GOAL>f.range = Subgroup.map f ⊤
<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).range = AddSubgroup.map f 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).range = Subgroup.map f K
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>f : G →* N<VAR>g : G<GOAL>↑(f.rangeRestrict g) = f g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<VAR>g : G<GOAL>↑(f.rangeRestrict g) = f g
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>f : G →+ N<GOAL>Subtype.val ∘ ⇑f.rangeRestrict = ⇑f