no goals
F : Type ?u.59663
G : Type ?u.59666
α : Type u_1
M : Type ?u.59672
N : Type ?u.59675
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ b / (a * b) = 1 / a
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div]