no goals
F : Type ?u.83442
α : Type u_1
β : Type ?u.83448
𝕜 : Type ?u.83451
E : Type ?u.83454
inst✝ : CancelCommMonoid α
s : Set α
a : α
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]