no goals
α : Type u_1
β : Type ?u.297556
γ : Type ?u.297559
δ : Type ?u.297562
inst✝ : CommMonoid α
a b c d : Associates α
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates α
hx : b = a * x
y : Associates α
hy : d = c * y
⊢ b * d = a * c * (x * y)
simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]