no goals
G : Type u_1
H : Type u_2
A : Type ?u.100510
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ 1 ∈ f ⁻¹' s
simp [hf.map_one, hs.toIsSubgroup.one_mem]
no goals
G : Type u_1
H : Type u_2
A : Type ?u.100510
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ ∀ {a b : G}, a ∈ f ⁻¹' s → b ∈ f ⁻¹' s → a * b ∈ f ⁻¹' s
simp (config := { contextual := true }) [hf.map_mul, hs.toIsSubgroup.mul_mem]
no goals
G : Type u_1
H : Type u_2
A : Type ?u.100510
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ ∀ {a : G}, a ∈ f ⁻¹' s → a⁻¹ ∈ f ⁻¹' s
simp (config := { contextual := true }) [hf.map_inv, hs.toIsSubgroup.inv_mem]
no goals
G : Type u_1
H : Type u_2
A : Type ?u.100510
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ ∀ (n : G), n ∈ f ⁻¹' s → ∀ (g : G), g * n * g⁻¹ ∈ f ⁻¹' s
simp (config := { contextual := true }) [hs.normal, hf.map_mul, hf.map_inv]