no goals
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ↑(toFunLinear R A) (↑(algebraMap R A) r ⊗ₜ[R] 1) = ↑(algebraMap R A[X]) r
rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, algebraMap_smul,
  Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one]