case mp =>
  intro h
  rw [injective]
  intros x y hinj
  rw [← hphi] at hinj
  have hh := mult_left H (H.inv (φ x)) _ _ hinj
  rw [H.mul_left_inv] at hh
  rw [←hom_preserve_inv] at hh
  rw [←hphi] at hh
  rw [←hom.preserve_comp] at hh
  have hker : (G.inv x * y) ∈ kernel G H hom := by
    rw [kernel, Membership.mem, instMembershipSet]
    simp
    rw [hh]
  have hsp := (h (G.inv x * y)).mp hker
  rw [trivial_subgroup, Membership.mem, instMembershipSet] at hsp
  simp at hsp
  have hmul := mult_left G x (group.inv x * y) G.one hsp
  rw [←G.mul_assoc] at hmul
  rw [mul_right_inv, G.one_mul, G.mul_one] at hmul
  rw [hmul]
α : 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
⊢ set_eq (kernel G H hom) (trivial_subgroup G) → injective (group_homomorphism.fn G H)
no goals