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