case intro.intro.intro.intro.intro.intro
F : Type ?u.99156
α : Type u_1
β : Type ?u.99162
𝕜 : Type ?u.99165
E : Type ?u.99168
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => x * a) b * (fun x => x * a) c = (fun x => x * a) d * (fun x => x * a) d
⊢ (fun x => x * a) b = (fun x => x * a) c
F : Type ?u.99156
α : Type u_1
β : Type ?u.99162
𝕜 : Type ?u.99165
E : Type ?u.99168
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
⊢ MulSalemSpencer ((fun x => x * a) '' s)
rintro _ _ _ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩ h
case intro.intro.intro.intro.intro.intro
F : Type ?u.99156
α : Type u_1
β : Type ?u.99162
𝕜 : Type ?u.99165
E : Type ?u.99168
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * c * (a * a) = d * d * (a * a)
⊢ (fun x => x * a) b = (fun x => x * a) c
case intro.intro.intro.intro.intro.intro
F : Type ?u.99156
α : Type u_1
β : Type ?u.99162
𝕜 : Type ?u.99165
E : Type ?u.99168
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => x * a) b * (fun x => x * a) c = (fun x => x * a) d * (fun x => x * a) d
⊢ (fun x => x * a) b = (fun x => x * a) c
rw [mul_mul_mul_comm, mul_mul_mul_comm d] at h
no goals
case intro.intro.intro.intro.intro.intro
F : Type ?u.99156
α : Type u_1
β : Type ?u.99162
𝕜 : Type ?u.99165
E : Type ?u.99168
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * c * (a * a) = d * d * (a * a)
⊢ (fun x => x * a) b = (fun x => x * a) c
rw [hs hb hc hd (mul_right_cancel₀ (mul_ne_zero ha ha) h)]