rw [inv_invo] at h
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one
α : Type u_1
g : group α
a : α
h : a * group.inv a = has_one.one
⊢ a * group.inv a = has_one.one