no goals
F : Type ?u.64657
G : Type ?u.64660
α : Type u_1
M : Type ?u.64666
N : Type ?u.64669
inst✝ : DivisionCommMonoid α
a✝ b c✝ d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b
rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]