have h2 : g.inv (g.inv a) * (g.inv a) * a = a := by {
  rw[h]
  apply g.one_mul
}
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ 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) * group.inv a * a = a
⊢ group.inv (group.inv a) = a