G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ f x = f 1
G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ x ∈ IsSubgroup.trivial G
suffices f x = f 1 by simpa using h this
G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ f x = 1
G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ f x = f 1
simp [hf.map_one]
no goals
G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ f x = 1
rwa [mem_ker] at hx
no goals
G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
this : f x = f 1
⊢ x ∈ IsSubgroup.trivial G
simpa using h this
no goals
G : Type u_1
H : Type u_2
A : Type ?u.113567
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
⊢ x ∈ IsSubgroup.trivial G → x ∈ ker f
simp (config := { contextual := true }) [mem_ker, hf.map_one]