no goals
α : Type ?u.54779
β : Type ?u.54782
G : Type u_1
inst✝ : Group G
a b c d : G
h : a⁻¹ * b = c
⊢ b = a * c
rw [← h, mul_inv_cancel_left]
no goals
α : Type ?u.54779
β : Type ?u.54782
G : Type u_1
inst✝ : Group G
a b c d : G
h : b = a * c
⊢ a⁻¹ * b = c
rw [h, inv_mul_cancel_left]