no goals
α : Type ?u.54177
β : Type ?u.54180
G : Type u_1
inst✝ : Group G
a b c d : G
h : a = b * c⁻¹
⊢ a * c = b
rw [h, inv_mul_cancel_right]
no goals
α : Type ?u.54177
β : Type ?u.54180
G : Type u_1
inst✝ : Group G
a b c d : G
h : a * c = b
⊢ a = b * c⁻¹
rw [← h, mul_inv_cancel_right]