conv at hg =>
  left
  rw [← H.mul_one (φ G.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
hg : φ has_one.one = φ has_one.one * φ has_one.one
⊢ φ has_one.one = 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
hg : φ has_one.one * has_one.one = φ has_one.one * φ has_one.one
⊢ φ has_one.one = has_one.one