no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
inst✝ : CommSemiring k
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
  Polynomial.eval₂_mul, hf, hg, MulZeroClass.zero_mul, MulZeroClass.zero_mul, zero_add]