case mp =>
  intro hker
  rw [kernel, Membership.mem, instMembershipSet] at hker
  simp at hker
  rw [←hphi] at hker
  rw [injective] at h
  have hinj := h G.one x
  rw [←hphi] at hinj
  rw [hphi, hom_preserve_one G H hom, ←hphi] at hinj
  have hl := hinj hker.symm
  rw [←hl]
  rw [Membership.mem, instMembershipSet]
  simp
  have hts : subgroup G (trivial_subgroup G) := triv_is_subgroup
  apply hts.one_mem
α : 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 : α
⊢ x ∈ kernel G H hom → x ∈ trivial_subgroup G
no goals