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