conv =>
  left
  right
  rw [← G.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
⊢ φ has_one.one = group_homomorphism.fn G H (has_one.one * has_one.one)
no goals