rw [g.mul_left_inv a] at h2
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * (group.inv a * a) = 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
h2 : group.inv (group.inv a) * has_one.one = a
⊢ group.inv (group.inv a) = a