have h : (g.inv g.one) * g.one = g.one := g.mul_left_inv g.one
α : Type u_1
g : group α
⊢ 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
⊢ group.inv has_one.one = has_one.one