no goals
F : Type ?u.103189
α : Type u_1
β : Type ?u.103195
𝕜 : Type ?u.103198
E : Type ?u.103201
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
b c d : α
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
h : b * c = d * d
⊢ a * b * (a * c) = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
rw [mul_mul_mul_comm, h, mul_mul_mul_comm]