congr
σ : 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 ∈ p.support, (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e) =
    ∑ m ∈ p.support, (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e
case e_f
σ : 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
⊢ (fun x => (algebraMap R B) (coeff x p) * f (x.prod fun n e => a n ^ e)) = fun m =>
    (algebraMap R B) (coeff m p) * m.prod fun n e => (⇑f ∘ a) n ^ e