R : Type u_2
A : Type u_4
B : Type u_3
σ : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R B) (↑(algebraMap A B) ∘ x)) p =
    ↑(eval₂Hom (algebraMap R B) fun i => ↑(algebraMap A B) (x i)) p
R : Type u_2
A : Type u_4
B : Type u_3
σ : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = ↑(algebraMap A B) (↑(aeval x) p)
rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
  IsScalarTower.algebraMap_eq]
no goals
R : Type u_2
A : Type u_4
B : Type u_3
σ : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R B) (↑(algebraMap A B) ∘ x)) p =
    ↑(eval₂Hom (algebraMap R B) fun i => ↑(algebraMap A B) (x i)) p
simp only [Function.comp]