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