Theorem: Misc.Nat.mul_div_cancel_left' (LeanSAT/Util/Misc.lean)

State before:
a b : Nat
Hd : a ∣ b
⊢ a * (b / a) = b
Tactic:
rw [Nat.mul_comm, Nat.div_mul_cancel Hd]
State after:
no goals