no goals
α : Type u_1
β : Type ?u.333972
γ : Type ?u.333975
δ : Type ?u.333978
inst✝ : CancelCommMonoidWithZero α
a b c : Associates α
ha : a ≠ 0
d : Associates α
hd : a * c = a * b * d
⊢ a * c = a * (b * d)
rwa [← mul_assoc]