apply (cancel_right H (φ 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) = group.inv (φ 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 = group.inv (φ g) * φ g