no goals
F : Type ?u.106147
α : Type u_1
β : Type ?u.106153
𝕜 : Type ?u.106156
E : Type ?u.106159
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
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]