simp only [map_prod, aeval_X_pow, Polynomial.aeval_X, aeval_one, Polynomial.aeval_C,
  AlgHom.map_sub] at this
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this :
  (Polynomial.aeval (MvPolynomial.X 0)) (Polynomial.X ^ n - 1) =
    (Polynomial.aeval (MvPolynomial.X 0)) (∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ))
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
x y : K
this✝ : Polynomial.X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n K, (Polynomial.X - Polynomial.C ζ)
this :
  MvPolynomial.X 0 ^ n - 1 = ∏ x ∈ nthRootsFinset n K, (MvPolynomial.X 0 - (algebraMap K (MvPolynomial (Fin 2) K)) x)
⊢ MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n =
    ∏ ζ ∈ nthRootsFinset n K, (MvPolynomial.X 0 - MvPolynomial.C ζ * MvPolynomial.X 1)