no goals
F : Type ?u.60370
G : Type ?u.60373
α : Type u_1
M : Type ?u.60379
N : Type ?u.60382
inst✝ : DivisionMonoid α
a✝ b✝ c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b
simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]