no goals
F : Type ?u.63975
G : Type ?u.63978
α : Type u_1
M : Type ?u.63984
N : Type ?u.63987
inst✝ : DivisionCommMonoid α
a✝ b✝ c d : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b
rw [mul_comm c, mul_comm c, h.mul_div_mul_right]