no goals
F : Type ?u.63416
G : Type ?u.63419
α : Type u_1
M : Type ?u.63425
N : Type ?u.63428
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a * (b / a) = b
rw [mul_comm, h.div_mul_cancel]