rw [←hphi] at hker
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : group_homomorphism.fn G H x = has_one.one
⊢ x ∈ trivial_subgroup G
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : φ x = has_one.one
⊢ x ∈ trivial_subgroup G