no goals
α : Type ?u.54481
β : Type ?u.54484
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.54481
β : Type ?u.54484
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]