rw [←G.mul_assoc, ←G.mul_assoc, G.mul_left_inv, G.one_mul, G.one_mul] at h'
α : 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
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : b = c
⊢ b = c