using `aeval_C`

Stream: new members

[Vasily Ilin]

I have an algebra map comult from $K[X]$ to $K[X] \otimes K[X]$. I want to show that comult takes $1$ to $1\otimes 1$. My attempt below does not work for some reason. It seems that Lean does not understand that $1$ is the constant polynomial.

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

universe u
variables (K : Type u) [comm_semiring K]

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

lemma comul_1 : comul K (1 : K[X]) = 1 ⊗ₜ 1 :=
begin
  unfold comul, -- ⊢ ⇑(aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X)) 1 = 1 ⊗ₜ[K] 1
  rw @aeval_C K (K[X] ⊗[K] K[X]) _ _ _ ((X ⊗ₜ[K] 1) + (1 ⊗ₜ[K] X)) 1, -- did not find instance of the pattern in the target expression ⇑(aeval (X ⊗ₜ[K] 1 + 1 ⊗ₜ[K] X)) (⇑C 1)
end