no goals
F : Type ?u.62190
G : Type ?u.62193
α : Type u_1
M : Type ?u.62199
N : Type ?u.62202
inst✝ : DivisionCommMonoid α
a b✝ c d : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b
rw [mul_comm, h.div_mul_left]