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