have h' := mult_left G (G.inv a) (a * b) (a * c) h
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
⊢ b = c
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : group.inv a * (a * b) = group.inv a * (a * c)
⊢ b = c