no goals
F : Type ?u.62857
G : Type ?u.62860
α : Type u_1
M : Type ?u.62866
N : Type ?u.62869
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a * b / a = b
rw [mul_comm, h.mul_div_cancel]