have hg : φ (G.one) = (φ G.one) * (φ G.one) := by
  rw [← hom.preserve_comp]
  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 = 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