have h := (g.mul_left_inv (g.inv a))
α : Type u_1
g : group α
a : α
⊢ group.inv (group.inv a) = a
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) = a