no goals
F : Type ?u.87422
α : Type u_1
β : Type ?u.87428
𝕜 : Type ?u.87431
E : Type ?u.87434
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer ((fun x => x * a) '' s)
b c d : α
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
h : b * c = d * d
⊢ b * a * (c * a) = d * a * (d * a)
rw [mul_mul_mul_comm, h, mul_mul_mul_comm]