R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable (∏ i in s, (X - ↑C (f i)))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable (∏ i in s, (X - ↑C (f i)))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y
by_contra hxy
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : Separable ((X - ↑C (f y)) ^ 2 * ∏ x in Finset.erase (Finset.erase s x) y, (X - ↑C (f x)))
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable (∏ i in s, (X - ↑C (f i)))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
rw [← insert_erase hx, prod_insert (not_mem_erase _ _), ←
  insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (not_mem_erase _ _), ←
  mul_assoc, hfxy, ← sq] at hfs
no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : Separable ((X - ↑C (f y)) ^ 2 * ∏ x in Finset.erase (Finset.erase s x) y, (X - ↑C (f x)))
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2