congr
case e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    (algebraMap R B) (coeff x p) * x.prod fun n e => (⇑f ∘ a) n ^ e
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ f (x.prod fun n e => a n ^ e) = x.prod fun n e => (⇑f ∘ a) n ^ e