rw [← hom.preserve_comp (G.inv g) g]
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) * φ g = has_one.one
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g * g) = has_one.one