no goals
F : Type ?u.66666
G : Type ?u.66669
α : Type u_1
M : Type ?u.66675
N : Type ?u.66678
inst✝ : DivisionCommMonoid α
a b c d : α
h : IsUnit a
⊢ a / (a / b) = b
rw [div_div_eq_mul_div, h.mul_div_cancel_left]