let φ := hom.fn
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
⊢ 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
⊢ group_homomorphism.fn G H has_one.one = has_one.one