case intro.intro.intro.intro.intro.intro
F : Type ?u.77288
α : Type u_1
β : Type ?u.77294
𝕜 : Type ?u.77297
E : Type ?u.77300
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x x_1 => x * x_1) a b * (fun x x_1 => x * x_1) a c = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
F : Type ?u.77288
α : Type u_1
β : Type ?u.77294
𝕜 : Type ?u.77297
E : Type ?u.77300
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
⊢ MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
rintro _ _ _ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩ h
case intro.intro.intro.intro.intro.intro
F : Type ?u.77288
α : Type u_1
β : Type ?u.77294
𝕜 : Type ?u.77297
E : Type ?u.77300
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : a * a * (b * c) = a * a * (d * d)
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
case intro.intro.intro.intro.intro.intro
F : Type ?u.77288
α : Type u_1
β : Type ?u.77294
𝕜 : Type ?u.77297
E : Type ?u.77300
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x x_1 => x * x_1) a b * (fun x x_1 => x * x_1) a c = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
rw [mul_mul_mul_comm, mul_mul_mul_comm a d] at h
no goals
case intro.intro.intro.intro.intro.intro
F : Type ?u.77288
α : Type u_1
β : Type ?u.77294
𝕜 : Type ?u.77297
E : Type ?u.77300
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : a * a * (b * c) = a * a * (d * d)
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
rw [hs hb hc hd (mul_left_cancel h)]