rw [kernel, Membership.mem, instMembershipSet]
α : 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 : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ group.inv x * y ∈ kernel G H hom
α : 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 : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ { mem := fun x s => Set.isMember x }.1 (group.inv x * y)
    { isMember := fun g => group_homomorphism.fn G H g = has_one.one }