no goals
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : a = ↑b⁻¹ * c
⊢ ↑b * a = c
rw [h, mul_inv_cancel_left]
no goals
α : Type u
inst✝ : Monoid α
a✝ b c✝ u : αˣ
a c : α
h : ↑b * a = c
⊢ a = ↑b⁻¹ * c
rw [← h, inv_mul_cancel_left]