no goals
R : Type u
S₁ : Type v
S₂✝ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f✝ : R →+* S₁
g✝ : σ → S₁
S₂ : Type u_1
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ↑k (eval₂ f g p) = eval₂ (RingHom.comp k f) (↑k ∘ g) p
apply MvPolynomial.induction_on p <;>
  simp (config := { contextual := true }) [eval₂_add, k.map_add, eval₂_mul, k.map_mul]