no goals
F : Type ?u.65500
G : Type ?u.65503
α : Type u_1
M : Type ?u.65509
N : Type ?u.65512
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
  hd.div_mul_cancel]