no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.863799
B' : Type ?u.863802
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.864015
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ ↑φ p = eval₂ (algebraMap R A) (↑φ X) p
rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]