have hts : subgroup G (trivial_subgroup G) := triv_is_subgroup
α : 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 : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ Set.isMember has_one.one
α : 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 : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
hts : subgroup G (trivial_subgroup G)
⊢ Set.isMember has_one.one