rw [G.mul_assoc, G.mul_assoc, mul_right_inv, G.mul_one, G.mul_one] at h'
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b * a * group.inv a = c * a * group.inv a
⊢ b = c
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b = c
⊢ b = c