case mpr =>
  intro h
  rw [set_eq]
  intro x
  apply Iff.intro
  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
  case mpr =>
    intro hone
    rw [trivial_subgroup, Membership.mem, instMembershipSet] at hone
    simp at hone
    rw [hone]
    rw [kernel, Membership.mem, instMembershipSet]
    simp
    apply hom_preserve_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
⊢ injective (group_homomorphism.fn G H) → set_eq (kernel G H hom) (trivial_subgroup G)
no goals